diff --git a/.github/workflows/bsd-proof-program-pfk-dependency.yml b/.github/workflows/bsd-proof-program-pfk-dependency.yml new file mode 100644 index 0000000..5ea6e92 --- /dev/null +++ b/.github/workflows/bsd-proof-program-pfk-dependency.yml @@ -0,0 +1,35 @@ +name: bsd-proof-program PFK Dependency Validation + +on: + pull_request: + branches: [main] + push: + branches: [main] + +jobs: + validate-pfk-dependency: + runs-on: ubuntu-latest + steps: + - name: Checkout bsd-proof-program + uses: actions/checkout@v4 + with: + path: bsd-proof-program + + - name: Checkout Heller-Godel at pinned commit + uses: actions/checkout@v4 + with: + repository: SocioProphet/Heller-Godel + ref: 988307215ad38ccb16514311222184a1b757752b + path: Heller-Godel + + - name: Setup Python + uses: actions/setup-python@v5 + with: + python-version: '3.11' + + - name: Validate canonical PFK dependency + env: + HELLER_GODEL_ROOT: ${{ github.workspace }}/Heller-Godel + run: | + cd bsd-proof-program + python -m unittest tests/test_pfk_dependency.py -v diff --git a/DEPENDENCIES.md b/DEPENDENCIES.md new file mode 100644 index 0000000..2445e24 --- /dev/null +++ b/DEPENDENCIES.md @@ -0,0 +1,86 @@ +# Dependencies + +## Upstream + +| Repository | Commit SHA | Cited content | +|---|---|---| +| `SocioProphet/Heller-Godel` | `988307215ad38ccb16514311222184a1b757752b` | Framework objects (`HG-*`) from `docs/framework-core/`; PFK operational substrate from `proof_fabric_kernel/` | + +## Cited objects + +### Framework-grade (HG-*) + +| Identifier | Role | Notes | +|---|---|---| +| `HG-FND-*` | Foundational vocabulary | typing and claim-boundary vocabulary only | +| `HG-MTH-005` | Universal Bridge formal specification | method-grade shared-missing-machinery diagnosis; does not transfer proofs | +| `HG-MTH-009` | Universal Bridge: arithmetic-geometric / BSD domain extension | reserved upstream; not yet drafted | + +### PFK operational substrate + +| Identifier | Role | BSD use | +|---|---|---| +| `PFK-OP-001` | Event ingestion family | future receipt emission | +| `PFK-OP-030` | Calibration operator family | numerical baselines for congruent-number family and rank/check artifacts | +| `PFK-OP-050` | PrimeStatsProtocol family | descriptive-grade empirical surveys, if any | + +### PFK schemas + +| Identifier | Canonical path | BSD use | +|---|---|---| +| `PFK-SCHEMA-001` | `proof_fabric_kernel/schemas/claim_ledger_row.schema.json` | future workstream claim ledgers | +| `PFK-SCHEMA-002` | `proof_fabric_kernel/schemas/event_ir.schema.json` | operator invocation receipts | +| `PFK-SCHEMA-003` | `proof_fabric_kernel/schemas/proof_artifact.schema.json` | proof-step envelopes | +| `PFK-SCHEMA-004` | `proof_fabric_kernel/schemas/calibration_bundle.schema.json` | numerical baseline checks | + +### PFK anti-seed + +| Identifier | Applies because | +|---|---| +| `A-PFK-OP-001` | operator invocation is not evidence; congruent-number calibration is not BSD progress | +| `A-PFK-PROTOCOL-001` | null passage is not theorem-grade | +| `A-PFK-PROTOCOL-002` | window-shopping prevention for rank-distribution or Tunnell-checkable surveys | +| `A-PFK-SCHEMA-001` | schema validity is not content validity | +| `A-PFK-SCHEMA-002` | schema-version drift; pin is not floating | +| `A-PFK-VAL-001` | validator green is not audit completion | + +### Framework anti-seed + +| Identifier | Failure mode | +|---|---| +| `A-MTH-001` | Universal Bridge does not transfer proofs | +| `A-MTH-003` | Catalan / mu2 fixture is not Clay progress | + +## Citation form + +```text +[HG-MTH-005 @ 988307215ad38ccb16514311222184a1b757752b] +[HG-MTH-009 @ 988307215ad38ccb16514311222184a1b757752b] # reserved, not yet drafted +[PFK-SCHEMA-001 @ 988307215ad38ccb16514311222184a1b757752b] +[A-PFK-OP-001 @ 988307215ad38ccb16514311222184a1b757752b] +``` + +## Forbidden edges + +- `bsd-proof-program` -> any other Clay-program repo (no horizontal dependencies). +- `bsd-proof-program` -> Heller-Godel-other-than-pinned-commit (no floating references). +- `bsd-proof-program` -> Universal Bridge material as proof transfer. + +## Scope discipline + +This dependency declaration does not change M6 discipline: + +- no BSD proof claim; +- no rank computation claim; +- no row promotion; +- no parity theorem use for M6 promotion; +- no finite-Sha assumption; +- no use of BSD, parity, or Sha-finiteness for `H-E1-alg` exact-rank promotion. + +The current M6 boundary remains authoritative: exact-rank promotion cannot set `bsd_used = true`, `parity_used = true`, or `sha_finite_assumed = true`. + +## Schema source + +PFK schemas live canonically at `SocioProphet/Heller-Godel/proof_fabric_kernel/schemas/` at the pinned commit. This repository consumes them through `HELLER_GODEL_ROOT` in dependency validation workflows. + +Local schema material, if any, is non-authoritative unless explicitly declared generated/cache-only. It must not shadow canonical PFK schema names. diff --git a/README.md b/README.md index e810b49..e56a60d 100644 --- a/README.md +++ b/README.md @@ -24,12 +24,55 @@ This tranche contains type contracts, runbooks, tests, audit documentation, and --- +## Heller-Godel / PFK dependency + +This repository consumes the canonical Heller-Godel framework and Proof Fabric Kernel at: + +```text +SocioProphet/Heller-Godel @ 988307215ad38ccb16514311222184a1b757752b +``` + +See: + +```text +DEPENDENCIES.md +``` + +PFK schemas and registry docs are canonical in Heller-Godel under: + +```text +proof_fabric_kernel/ +``` + +Local schema material, if any, is non-authoritative unless explicitly declared generated/cache-only. It must not shadow canonical PFK schema names. + +--- + +## BSD Program Lane v0.1 skeleton + +This repository now includes a structural skeleton for `BSD_Program_Lane_v0.1.pdf`: + +```text +docs/program-spec/bsd-program-lane-v0_1.md +docs/workstream-a/README.md +docs/workstream-b/README.md +docs/workstream-c/README.md +docs/workstream-d/README.md +docs/workstream-e/README.md +docs/workstream-f/README.md +``` + +The skeleton records workstream structure and claim boundaries only. It is not a full-text Drive PDF import and does not change M6 promotion discipline. + +--- + ## Status | Tranche | Status | Mathematics added | |---|---|---| | v0.5 inherited | Canonical baseline | existing | | v0.3.2 handoff | M6 pre-execution scaffolding | none — documentation, schema, tests | +| BSD lane v0.1 skeleton | Structural scaffold | none — workstream structure and dependencies only | | v0.6.0 next | M6.0 → M6.8 execution | TBD per outcome | --- @@ -80,11 +123,19 @@ Generated M6.0 outputs are not part of the initial handoff baseline unless expli ├── Makefile ├── requirements.txt ├── pyproject.toml +├── DEPENDENCIES.md ├── .github/workflows/validate.yml ├── data/v0.5/ ├── docs/audit/ +├── docs/program-spec/ ├── docs/runbooks/ ├── docs/specs/ +├── docs/workstream-a/ +├── docs/workstream-b/ +├── docs/workstream-c/ +├── docs/workstream-d/ +├── docs/workstream-e/ +├── docs/workstream-f/ ├── m6/models/ ├── m6/scripts/ ├── reports/v0.5/ @@ -192,4 +243,4 @@ Authoritative import tracker: ```text https://github.com/SocioProphet/bsd-proof-program/issues/1 -``` +``` \ No newline at end of file diff --git a/docs/program-spec/bsd-program-lane-v0_1.md b/docs/program-spec/bsd-program-lane-v0_1.md new file mode 100644 index 0000000..f11e0a9 --- /dev/null +++ b/docs/program-spec/bsd-program-lane-v0_1.md @@ -0,0 +1,94 @@ +# BSD Program Lane v0.1 — Specification Skeleton + +Source reference: `BSD_Program_Lane_v0.1.pdf` (Drive, May 9, 2026). +Status: structural skeleton only; full PDF text not imported by this PR. +Claim level: program specification / no theorem claim. + +## Import discipline + +This file records the BSD Program Lane v0.1 structure known from the program review context. It does not claim to be a byte-faithful or full-text import of the Drive PDF. + +A future source-import PR with Drive/PDF access should replace this skeleton with full extracted markdown, preserving the workstream and claim-boundary structure below. + +## Scope + +The BSD program is scoped to disciplined evidence handling around the Birch and Swinnerton-Dyer program, including congruent-number family fixtures and M6 exact-rank promotion constraints. + +This skeleton does not claim: + +- a BSD proof; +- a rank computation; +- a row promotion; +- finite Sha; +- parity theorem applicability to M6 rows; +- any theorem-grade BSD artifact. + +## Workstreams A-F + +### Workstream A — Foundational typing + +Defines the BSD claim surface, coefficient fields, elliptic-curve object model, and claim-boundary vocabulary. + +### Workstream B — Mordell-Weil and Tate-Shafarevich structure + +Records the structural relationship between Mordell-Weil rank, Selmer groups, descent data, and Tate-Shafarevich obstructions without assuming finite Sha unless explicitly allowed by a theorem. + +### Workstream C — Tunnell-checkable cases + +Controls congruent-number family fixtures, including elliptic curves of the form: + +```text +E_n: y^2 = x^3 - n^2 x +``` + +Fixture-grade work remains fixture-grade unless upgraded by a theorem-grade artifact. + +### Workstream D — p-adic and Iwasawa-theoretic apparatus + +Records p-adic L-function, Iwasawa-theoretic, and related arithmetic apparatus boundaries. No p-adic evidence is theorem-grade without explicit theorem/citation. + +### Workstream E — Empirical surveys + +Controls descriptive-grade surveys such as rank-distribution or Tunnell-checkable computations. Any empirical claim must declare distribution, tranche, nulls, and reporting policy. + +### Workstream F — Promotion gates and audit + +Defines promotion gates, audit requirements, anti-seed cross-references, and rollback discipline. + +## Evidence classes E0-E7 + +The full v0.1 PDF should define the canonical evidence classes. Until full source import, this skeleton only reserves the class range: + +```text +E0, E1, E2, E3, E4, E5, E6, E7 +``` + +No downstream PR should cite the detailed contents of a class until the full v0.1 spec text is imported or the class is independently defined in repo. + +## Promotion gates + +The full v0.1 PDF should define the canonical promotion gates. Until full source import, this skeleton reserves: + +| Gate | Status | +|---|---| +| Gate 0 | workstream specification accepted | +| Gate 1 | workstream apparatus implemented | +| Gate 2 | fixture validated | +| Gate 3 | first descriptive-grade claim | +| Gate 4 | first methodology-grade claim | +| Gate 5 | theorem-grade artifact | + +## Anti-seed cross-references + +- `[A-MTH-001 @ 988307215ad38ccb16514311222184a1b757752b]` — Universal Bridge does not transfer proofs. +- `[A-MTH-003 @ 988307215ad38ccb16514311222184a1b757752b]` — fixture-grade work is not Clay progress. +- `[A-PFK-OP-001 @ 988307215ad38ccb16514311222184a1b757752b]` — operator invocation is not evidence. +- `[A-PFK-SCHEMA-001 @ 988307215ad38ccb16514311222184a1b757752b]` — schema validity is not content validity. + +## Citation form + +```text +[BSD-LANE-V0.1-SKELETON @ ] +``` + +This skeleton is citable as a structural scaffold only, not as the full Drive PDF import. diff --git a/docs/workstream-a/README.md b/docs/workstream-a/README.md new file mode 100644 index 0000000..77b969d --- /dev/null +++ b/docs/workstream-a/README.md @@ -0,0 +1,29 @@ +# Workstream A — Foundational Typing + +Spec citation: `[BSD-LANE-V0.1-SKELETON @ ]` +Framework citation: `[HG-MTH-005 @ 988307215ad38ccb16514311222184a1b757752b]` +PFK citation: `[PFK-SCHEMA-001 @ 988307215ad38ccb16514311222184a1b757752b]` +Boundary anti-seed: `[A-MTH-001 @ 988307215ad38ccb16514311222184a1b757752b]` + +## Status + +Workstream skeleton. No apparatus implemented yet. + +## Purpose + +Define the BSD claim surface, elliptic-curve object model, coefficient fields, evidence grades, and forbidden promotion rules. + +## Promotion gate status + +| Gate | Status | +|---|---| +| Gate 0 — spec accepted | pending PR merge | +| Gate 1 — apparatus implemented | pending | +| Gate 2 — fixture validated | pending | +| Gate 3 — descriptive-grade claim | pending | +| Gate 4 — methodology-grade claim | pending | +| Gate 5 — theorem-grade artifact | pending | + +## Boundary + +This workstream does not claim BSD progress. It defines vocabulary and audit surface only. diff --git a/docs/workstream-b/README.md b/docs/workstream-b/README.md new file mode 100644 index 0000000..6d4c2c2 --- /dev/null +++ b/docs/workstream-b/README.md @@ -0,0 +1,29 @@ +# Workstream B — Mordell-Weil and Tate-Shafarevich Structure + +Spec citation: `[BSD-LANE-V0.1-SKELETON @ ]` +Framework citation: `[HG-MTH-005 @ 988307215ad38ccb16514311222184a1b757752b]` +PFK citation: `[PFK-SCHEMA-003 @ 988307215ad38ccb16514311222184a1b757752b]` +Boundary anti-seed: `[A-PFK-VAL-001 @ 988307215ad38ccb16514311222184a1b757752b]` + +## Status + +Workstream skeleton. No apparatus implemented yet. + +## Purpose + +Record structural relationships among Mordell-Weil rank, Selmer data, descent outputs, and Tate-Shafarevich obstructions without assuming finite Sha unless an explicit theorem permits it. + +## Promotion gate status + +| Gate | Status | +|---|---| +| Gate 0 — spec accepted | pending PR merge | +| Gate 1 — apparatus implemented | pending | +| Gate 2 — fixture validated | pending | +| Gate 3 — descriptive-grade claim | pending | +| Gate 4 — methodology-grade claim | pending | +| Gate 5 — theorem-grade artifact | pending | + +## Boundary + +Root number, Selmer rank, and parity-shaped evidence do not by themselves provide exact rank promotion under M6 H-E1-alg discipline. diff --git a/docs/workstream-c/README.md b/docs/workstream-c/README.md new file mode 100644 index 0000000..40e2cef --- /dev/null +++ b/docs/workstream-c/README.md @@ -0,0 +1,33 @@ +# Workstream C — Tunnell-Checkable Cases + +Spec citation: `[BSD-LANE-V0.1-SKELETON @ ]` +Framework citation: `[HG-MTH-005 @ 988307215ad38ccb16514311222184a1b757752b]` +PFK citation: `[PFK-SCHEMA-004 @ 988307215ad38ccb16514311222184a1b757752b]` +Boundary anti-seed: `[A-PFK-OP-001 @ 988307215ad38ccb16514311222184a1b757752b]` + +## Status + +Workstream skeleton. No apparatus implemented yet. + +## Purpose + +Control congruent-number family fixtures, including curves of the form: + +```text +E_n: y^2 = x^3 - n^2 x +``` + +## Promotion gate status + +| Gate | Status | +|---|---| +| Gate 0 — spec accepted | pending PR merge | +| Gate 1 — apparatus implemented | pending | +| Gate 2 — fixture validated | pending | +| Gate 3 — descriptive-grade claim | pending | +| Gate 4 — methodology-grade claim | pending | +| Gate 5 — theorem-grade artifact | pending | + +## Boundary + +Tunnell-checkable fixture work is not BSD proof. Conditional results must declare all assumptions explicitly. diff --git a/docs/workstream-d/README.md b/docs/workstream-d/README.md new file mode 100644 index 0000000..0fb6ac5 --- /dev/null +++ b/docs/workstream-d/README.md @@ -0,0 +1,29 @@ +# Workstream D — p-adic and Iwasawa-Theoretic Apparatus + +Spec citation: `[BSD-LANE-V0.1-SKELETON @ ]` +Framework citation: `[HG-MTH-005 @ 988307215ad38ccb16514311222184a1b757752b]` +PFK citation: `[PFK-SCHEMA-003 @ 988307215ad38ccb16514311222184a1b757752b]` +Boundary anti-seed: `[A-MTH-001 @ 988307215ad38ccb16514311222184a1b757752b]` + +## Status + +Workstream skeleton. No apparatus implemented yet. + +## Purpose + +Record p-adic L-function, Iwasawa-theoretic, and related arithmetic apparatus boundaries. + +## Promotion gate status + +| Gate | Status | +|---|---| +| Gate 0 — spec accepted | pending PR merge | +| Gate 1 — apparatus implemented | pending | +| Gate 2 — fixture validated | pending | +| Gate 3 — descriptive-grade claim | pending | +| Gate 4 — methodology-grade claim | pending | +| Gate 5 — theorem-grade artifact | pending | + +## Boundary + +p-adic or Iwasawa-theoretic evidence is not theorem-grade unless supported by a precise theorem or cited result in the native arithmetic-geometric setting. diff --git a/docs/workstream-e/README.md b/docs/workstream-e/README.md new file mode 100644 index 0000000..9c9f003 --- /dev/null +++ b/docs/workstream-e/README.md @@ -0,0 +1,29 @@ +# Workstream E — Empirical Surveys + +Spec citation: `[BSD-LANE-V0.1-SKELETON @ ]` +Framework citation: `[HG-MTH-005 @ 988307215ad38ccb16514311222184a1b757752b]` +PFK citation: `[PFK-OP-050 @ 988307215ad38ccb16514311222184a1b757752b]` +Boundary anti-seed: `[A-PFK-PROTOCOL-002 @ 988307215ad38ccb16514311222184a1b757752b]` + +## Status + +Workstream skeleton. No apparatus implemented yet. + +## Purpose + +Control descriptive-grade empirical surveys such as rank-distribution studies or Tunnell-checkable runs. + +## Promotion gate status + +| Gate | Status | +|---|---| +| Gate 0 — spec accepted | pending PR merge | +| Gate 1 — apparatus implemented | pending | +| Gate 2 — fixture validated | pending | +| Gate 3 — descriptive-grade claim | pending | +| Gate 4 — methodology-grade claim | pending | +| Gate 5 — theorem-grade artifact | pending | + +## Boundary + +Empirical surveys must declare distribution, tranche, nulls, and reporting policy. Passing an empirical protocol does not constitute BSD proof. diff --git a/docs/workstream-f/README.md b/docs/workstream-f/README.md new file mode 100644 index 0000000..e9dda34 --- /dev/null +++ b/docs/workstream-f/README.md @@ -0,0 +1,29 @@ +# Workstream F — Promotion Gates and Audit + +Spec citation: `[BSD-LANE-V0.1-SKELETON @ ]` +Framework citation: `[HG-MTH-005 @ 988307215ad38ccb16514311222184a1b757752b]` +PFK citation: `[PFK-SCHEMA-001 @ 988307215ad38ccb16514311222184a1b757752b]` +Boundary anti-seed: `[A-PFK-VAL-001 @ 988307215ad38ccb16514311222184a1b757752b]` + +## Status + +Workstream skeleton. No apparatus implemented yet. + +## Purpose + +Define promotion gates, audit requirements, rollback discipline, and anti-seed cross-references for BSD workstreams. + +## Promotion gate status + +| Gate | Status | +|---|---| +| Gate 0 — spec accepted | pending PR merge | +| Gate 1 — apparatus implemented | pending | +| Gate 2 — fixture validated | pending | +| Gate 3 — descriptive-grade claim | pending | +| Gate 4 — methodology-grade claim | pending | +| Gate 5 — theorem-grade artifact | pending | + +## Boundary + +Validator green status is not audit completion. Gate movement requires explicit review and recorded evidence. diff --git a/tests/conftest.py b/tests/conftest.py new file mode 100644 index 0000000..49c3096 --- /dev/null +++ b/tests/conftest.py @@ -0,0 +1,7 @@ +from pathlib import Path +import sys + +ROOT = Path(__file__).resolve().parents[1] +root_str = str(ROOT) +if root_str not in sys.path: + sys.path.insert(0, root_str) diff --git a/tests/test_pfk_dependency.py b/tests/test_pfk_dependency.py new file mode 100644 index 0000000..614536d --- /dev/null +++ b/tests/test_pfk_dependency.py @@ -0,0 +1,67 @@ +from pathlib import Path +import os +import unittest + + +ROOT = Path(__file__).resolve().parents[1] +PIN = "988307215ad38ccb16514311222184a1b757752b" +REQUIRED_PFK_PATHS = [ + "proof_fabric_kernel/docs/OperatorCatalog_PrimePolicyOperators_v1.md", + "proof_fabric_kernel/docs/SchemaCatalog_v1.md", + "proof_fabric_kernel/docs/anti-seed-pfk.md", + "proof_fabric_kernel/schemas/claim_ledger_row.schema.json", + "proof_fabric_kernel/schemas/event_ir.schema.json", + "proof_fabric_kernel/schemas/proof_artifact.schema.json", + "proof_fabric_kernel/schemas/calibration_bundle.schema.json", +] +CANONICAL_SCHEMA_NAMES = { + "claim_ledger_row.schema.json", + "event_ir.schema.json", + "proof_artifact.schema.json", + "calibration_bundle.schema.json", +} + + +class TestPFKDependency(unittest.TestCase): + def test_dependencies_file_exists_and_pins_commit(self) -> None: + path = ROOT / "DEPENDENCIES.md" + self.assertTrue(path.exists()) + text = path.read_text(encoding="utf-8") + self.assertIn(PIN, text) + self.assertIn("HG-MTH-005", text) + self.assertIn("PFK-SCHEMA-001", text) + self.assertIn("A-PFK-OP-001", text) + + def test_no_local_canonical_schema_shadowing(self) -> None: + local_schemas = ROOT / "schemas" + if not local_schemas.exists(): + return + local_names = {path.name for path in local_schemas.rglob("*.json")} + shadowed = sorted(local_names & CANONICAL_SCHEMA_NAMES) + self.assertFalse(shadowed, f"local schemas shadow canonical PFK schemas: {shadowed}") + + def test_canonical_pfk_schemas_resolve_when_available(self) -> None: + hg_root_value = os.environ.get("HELLER_GODEL_ROOT") + if not hg_root_value: + self.skipTest("HELLER_GODEL_ROOT not set; dependency-resolution check runs in dedicated workflow") + hg_root = Path(hg_root_value) + missing = [path for path in REQUIRED_PFK_PATHS if not (hg_root / path).exists()] + self.assertFalse(missing, f"Missing canonical Heller-Godel PFK paths: {missing}") + + def test_workstream_skeletons_exist(self) -> None: + expected = {f"workstream-{letter}" for letter in "abcdef"} + docs = ROOT / "docs" + found = {d.name for d in docs.iterdir() if d.is_dir() and d.name.startswith("workstream-")} + self.assertTrue(expected.issubset(found), f"Missing workstream skeletons: {expected - found}") + + def test_program_spec_skeleton_exists(self) -> None: + spec_path = ROOT / "docs" / "program-spec" / "bsd-program-lane-v0_1.md" + self.assertTrue(spec_path.exists()) + content = spec_path.read_text(encoding="utf-8") + for letter in "ABCDEF": + self.assertIn(f"Workstream {letter}", content) + self.assertIn("full PDF text not imported", content) + + +if __name__ == "__main__": + unittest.main()