feat: import BSD program lane v0.1 skeleton; declare Heller-Godel dependency

.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

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.

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
-```
+```

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-merge-sha>]
+```
+
+This skeleton is citable as a structural scaffold only, not as the full Drive PDF import.

docs/workstream-a/README.md

@@ -0,0 +1,29 @@
+# Workstream A — Foundational Typing
+
+Spec citation: `[BSD-LANE-V0.1-SKELETON @ <merge-sha>]`  
+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.

docs/workstream-b/README.md

@@ -0,0 +1,29 @@
+# Workstream B — Mordell-Weil and Tate-Shafarevich Structure
+
+Spec citation: `[BSD-LANE-V0.1-SKELETON @ <merge-sha>]`  
+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.

docs/workstream-c/README.md

@@ -0,0 +1,33 @@
+# Workstream C — Tunnell-Checkable Cases
+
+Spec citation: `[BSD-LANE-V0.1-SKELETON @ <merge-sha>]`  
+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.