diff --git a/docs/retro/OPEN_MATH_PR_CANDIDATES_20261023.json b/docs/retro/OPEN_MATH_PR_CANDIDATES_20261023.json new file mode 100644 index 000000000..26f16dfc0 --- /dev/null +++ b/docs/retro/OPEN_MATH_PR_CANDIDATES_20261023.json @@ -0,0 +1,382 @@ +{ + "schema_version": 1, + "object": "RETRO-MATH-OPEN-PR-SOURCE-OVERLAY-20261023", + "purpose": "Candidate-only complement to default-Math 313-unit inventory; no mathematical acceptance or graph-node admission.", + "scientific_effect": "NONE", + "scientific_status_authority": false, + "authority_to_accept_theorems": false, + "math_repository": "d6g8k5htny-coder/Math-", + "frozen_math_main": "9f3fb6918b28e6378c034ebc19e76d432f5391cb", + "open_pr_snapshot": { + "count": 33, + "source": "https://github.com/d6g8k5htny-coder/Math-/pulls", + "file_list_method": "Complete native paginated PR changed-file collections; PR491: 100+84; PR477: 100+100+49", + "limits": "Not a full checkout or hidden branch/artifact inventory." + }, + "landed_inventory_pointer": { + "main_pr": 527, + "source_report": "https://github.com/d6g8k5htny-coder/main/pull/527#issuecomment-6370536039", + "main_unit_count": 313, + "relation": "EXCLUDED_FROM_DEFAULT_MAIN_DENOMINATOR" + }, + "counts": { + "distinct_candidate_units": 17, + "cutoff_revision_units": 7, + "protocol_only_units": 2, + "source_manifest_payload_instances_independently_rehashed": 22 + }, + "verified_sources": { + "c293_pr": 482, + "c294_pr": 487, + "c299_pr": 491, + "c293_manifest_git_blob": "6974112f1e9b4bed7baa0af87af8ec093f939764", + "c294_manifest_git_blob": "1482e902afe1b2c49283861062f114598d5d171b", + "c299_manifest_git_blob": "18d2570643e45e2de06e89ab1a96e9332b0f6064", + "shared_c293_c294_lean_git_blobs": { + "Lifetime.lean": "f2508f7f2e3fd42f22f5aa52bc5ead5ff9e73b9a", + "TorusTopology.lean": "ed678ea322fe5315b3aaff44e4e2f06b018399d8", + "MorseFiniteCritical.lean": "989fabc6e8f04b0c4a36dff9b21d33b1299f7b92" + }, + "lm006_pr385_manifest_git_blob": "a6de8d4113cedf548b17c750da406f8aa6705eb4", + "fold_affine_pr389_manifest_git_blob": "242b1bbf9223532ba483d61c2bee7f0a3e644d53", + "check_grade": "22 source instances individually byte/SHA256 and Git blob compared; 12 formal files C293/C294, 4 LM006, 6 fold affine. No Lean build, Python runtime, proof verification or C299 copied-module SHA replay in this stage." + }, + "admission_rule": "On actual reviewed merge, compare new current Math main cut and source/object identities before moving any candidate to the landed inventory. Do not invent math graph nodes or inherit theorem acceptance.", + "candidate_units": [ + { + "unit": "frontiers/critical_ridge_20261020", + "kind": "formal_source", + "status": "PENDING_OPEN_PR", + "on_math_main_at_frozen_cut": false, + "pr_heads": [ + { + "number": 491, + "head": "deccada38a1510fb8330bc205890ba6e98527818", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/491" + }, + { + "number": 496, + "head": "91811388ef2e20cc30a1c418e866b185a253a186", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/496" + }, + { + "number": 497, + "head": "5b3cc75d1585a00ee1420a556af5b77748c418fa", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/497" + } + ], + "representative_paths": [ + "frontiers/critical_ridge_20261020/execution/author/PROOF.md", + "frontiers/critical_ridge_20261020/project/CriticalRidge.lean", + "frontiers/critical_ridge_20261020/c299_hosted_verify.py", + "frontiers/critical_ridge_20261020/test_c299_hosted_verify.py", + "frontiers/critical_ridge_20261020/HOSTED_SOURCE_MANIFEST.json" + ], + "note": "Three stacked PRs, separate heads; files in the stacked PRs are modified relative to their own unmerged bases." + }, + { + "unit": "frontiers/regular_point_chart_20261020", + "kind": "formal_source", + "status": "PENDING_OPEN_PR", + "on_math_main_at_frozen_cut": false, + "pr_heads": [ + { + "number": 488, + "head": "762a6f30e7131b7b2cc02ad2d80113de9263bd4c", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/488" + } + ], + "representative_paths": [ + "frontiers/regular_point_chart_20261020/RegularPointChart.lean", + "frontiers/regular_point_chart_20261020/RegularPointChartAxiomAudit.lean", + "frontiers/regular_point_chart_20261020/SOURCE_SHA256SUMS" + ], + "note": "Stacked on unmerged C294 branch." + }, + { + "unit": "frontiers/critical_level_attainment_20261020", + "kind": "formal_source", + "status": "PENDING_OPEN_PR", + "on_math_main_at_frozen_cut": false, + "pr_heads": [ + { + "number": 487, + "head": "7af365e8c8db1ae0275d4efe08a70a678f153ca2", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/487" + } + ], + "representative_paths": [ + "frontiers/critical_level_attainment_20261020/final-project/CriticalLevelAttainment.lean", + "frontiers/critical_level_attainment_20261020/final-project/CriticalLevelAxiomAudit.lean", + "frontiers/critical_level_attainment_20261020/FINAL_SOURCE_INVENTORY.json" + ], + "note": "Closed-superlevel local path connectivity premise remains explicit and open; seven declared Lean sources byte-verified." + }, + { + "unit": "frontiers/morse_finite_critical_20261018", + "kind": "formal_source", + "status": "PENDING_OPEN_PR", + "on_math_main_at_frozen_cut": false, + "pr_heads": [ + { + "number": 482, + "head": "35a7d76869aad52d7508d58bc589eeb0ddc18bbb", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/482" + } + ], + "representative_paths": [ + "frontiers/morse_finite_critical_20261018/final-project/MorseFiniteCritical.lean", + "frontiers/morse_finite_critical_20261018/final-project/MorseFiniteControls.lean", + "frontiers/morse_finite_critical_20261018/final-project/MorseFiniteAxiomAudit.lean", + "frontiers/morse_finite_critical_20261018/FINAL_SOURCE_INVENTORY.json" + ], + "note": "Five declared Lean sources byte-verified." + }, + { + "unit": "frontiers/source_lifetime_realization_20261017", + "kind": "formal_source", + "status": "PENDING_OPEN_PR", + "on_math_main_at_frozen_cut": false, + "pr_heads": [ + { + "number": 477, + "head": "db43694c9f9dbff2987e2e3c0a1260b5c48310ec", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/477" + } + ], + "representative_paths": [ + "frontiers/source_lifetime_realization_20261017/SourceLifetimeField.lean", + "frontiers/source_lifetime_realization_20261017/SourceLifetimeGeometry.lean", + "frontiers/source_lifetime_realization_20261017/SourceThetaBridge.lean", + "frontiers/source_lifetime_realization_20261017/validate_static.py" + ], + "note": "249 changed paths enumerated across three PR file-list pages; preserved native evidence is not acceptance." + }, + { + "unit": "frontiers/compact_source_cutoff_baseline_20261009", + "kind": "cutoff_revision", + "status": "PENDING_OPEN_PR", + "on_math_main_at_frozen_cut": false, + "pr_heads": [ + { + "number": 414, + "head": "06bac48e476c825323a74efb7e80cdb5ad9e9bb6", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/414" + } + ], + "representative_paths": [ + "frontiers/compact_source_cutoff_baseline_20261009/CompactSourceCutoff.lean", + "frontiers/compact_source_cutoff_baseline_20261009/SOURCE_MANIFEST.json" + ], + "note": "One revision stage in seven-packet cutoff lineage." + }, + { + "unit": "frontiers/compact_source_cutoff_proof_20261010", + "kind": "cutoff_revision", + "status": "PENDING_OPEN_PR", + "on_math_main_at_frozen_cut": false, + "pr_heads": [ + { + "number": 415, + "head": "bb3c92e3226827c9aa1d8746226efaf758e06e2c", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/415" + } + ], + "representative_paths": [ + "frontiers/compact_source_cutoff_proof_20261010/CompactSourceCutoffProof.lean", + "frontiers/compact_source_cutoff_proof_20261010/SOURCE_MANIFEST.json" + ], + "note": "Manifest declares NOT_COMPILED; no scientific promotion." + }, + { + "unit": "frontiers/compact_source_cutoff_proof_repair_20261011", + "kind": "cutoff_revision", + "status": "PENDING_OPEN_PR", + "on_math_main_at_frozen_cut": false, + "pr_heads": [ + { + "number": 424, + "head": "f7832c870cf31d4239a3a7d67b557e69029a1be1", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/424" + } + ], + "representative_paths": [ + "frontiers/compact_source_cutoff_proof_repair_20261011/CompactSourceCutoffProof.lean", + "frontiers/compact_source_cutoff_proof_repair_20261011/SOURCE_MANIFEST.json" + ], + "note": "Successor repair packet; not an independent accepted theorem." + }, + { + "unit": "frontiers/compact_source_cutoff_controls_repair_20261011", + "kind": "cutoff_revision", + "status": "PENDING_OPEN_PR", + "on_math_main_at_frozen_cut": false, + "pr_heads": [ + { + "number": 425, + "head": "128d96fbe39425519a30e48ce2efc7406041a61e", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/425" + } + ], + "representative_paths": [ + "frontiers/compact_source_cutoff_controls_repair_20261011/CompactSourceCutoffProof.lean", + "frontiers/compact_source_cutoff_controls_repair_20261011/SOURCE_MANIFEST.json" + ], + "note": "Successor repair packet; not an independent accepted theorem." + }, + { + "unit": "frontiers/compact_source_cutoff_controls_final_repair_20261011", + "kind": "cutoff_revision", + "status": "PENDING_OPEN_PR", + "on_math_main_at_frozen_cut": false, + "pr_heads": [ + { + "number": 426, + "head": "5fb3a52ebfbdb73a37f743d9ab960560979f3b20", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/426" + } + ], + "representative_paths": [ + "frontiers/compact_source_cutoff_controls_final_repair_20261011/CompactSourceCutoffProof.lean", + "frontiers/compact_source_cutoff_controls_final_repair_20261011/SOURCE_MANIFEST.json" + ], + "note": "Successor repair packet; not an independent accepted theorem." + }, + { + "unit": "frontiers/compact_source_cutoff_proper_partial_control_20261011", + "kind": "cutoff_revision", + "status": "PENDING_OPEN_PR", + "on_math_main_at_frozen_cut": false, + "pr_heads": [ + { + "number": 427, + "head": "25a4b611368063807ac9201aea80461ffe8583d2", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/427" + } + ], + "representative_paths": [ + "frontiers/compact_source_cutoff_proper_partial_control_20261011/CompactSourceCutoffProof.lean", + "frontiers/compact_source_cutoff_proper_partial_control_20261011/SOURCE_MANIFEST.json" + ], + "note": "Successor repair packet; not an independent accepted theorem." + }, + { + "unit": "frontiers/compact_source_cutoff_proper_partial_repair_20261011", + "kind": "cutoff_revision", + "status": "PENDING_OPEN_PR", + "on_math_main_at_frozen_cut": false, + "pr_heads": [ + { + "number": 430, + "head": "1a7fc4be83043f2e313927019db85fff61eeac3f", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/430" + } + ], + "representative_paths": [ + "frontiers/compact_source_cutoff_proper_partial_repair_20261011/CompactSourceCutoffProof.lean", + "frontiers/compact_source_cutoff_proper_partial_repair_20261011/SOURCE_MANIFEST.json" + ], + "note": "Manifest says PREPARED_UNFROZEN_NOT_COMPILED_NOT_PUBLISHED_NOT_ADMITTED." + }, + { + "unit": "companions/fold_affine_bridge_20261006", + "kind": "lean_code_test", + "status": "PENDING_OPEN_PR", + "on_math_main_at_frozen_cut": false, + "pr_heads": [ + { + "number": 389, + "head": "1038336f92a482b60c7d89fe3024c941281663d3", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/389" + } + ], + "representative_paths": [ + "companions/fold_affine_bridge_20261006/Contract.lean", + "companions/fold_affine_bridge_20261006/FoldAffineBridge.lean", + "companions/fold_affine_bridge_20261006/replay.py", + "companions/fold_affine_bridge_20261006/test_contract.py", + "companions/fold_affine_bridge_20261006/SOURCE_FILES.json" + ], + "note": "Six source/implementation/test/workflow/docs payloads byte-verified against manifest." + }, + { + "unit": "coefficients/lm006_wrong_sign_oned_20261006_a62c", + "kind": "coefficient_code_test", + "status": "PENDING_OPEN_PR", + "on_math_main_at_frozen_cut": false, + "pr_heads": [ + { + "number": 380, + "head": "f256bb9181fe9bf660476ce42e8979fbe1cd2f59", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/380" + }, + { + "number": 385, + "head": "089d87ace030e755511a04735c42c1f91911d4c1", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/385" + } + ], + "representative_paths": [ + "coefficients/lm006_wrong_sign_oned_20261006_a62c/NOTE.md", + "coefficients/lm006_wrong_sign_oned_20261006_a62c/oned.py", + "coefficients/lm006_wrong_sign_oned_20261006_a62c/test_oned.py", + "coefficients/lm006_wrong_sign_oned_20261006_a62c/RESULTS.json", + "coefficients/lm006_wrong_sign_oned_20261006_a62c/SOURCES.json" + ], + "note": "Both PRs share this packet name. At PR#385 four manifest-listed payload bytes/hashes matched." + }, + { + "unit": "coefficients/lm006_wrong_sign_refinement_20261006_r22", + "kind": "coefficient_code_test", + "status": "PENDING_OPEN_PR", + "on_math_main_at_frozen_cut": false, + "pr_heads": [ + { + "number": 372, + "head": "497dcca37abd18464a6b33cf32ce2e3263054323", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/372" + } + ], + "representative_paths": [ + "coefficients/lm006_wrong_sign_refinement_20261006_r22/NOTE.md", + "coefficients/lm006_wrong_sign_refinement_20261006_r22/refine.py", + "coefficients/lm006_wrong_sign_refinement_20261006_r22/test_refinement.py", + "coefficients/lm006_wrong_sign_refinement_20261006_r22/RESULTS.json", + "coefficients/lm006_wrong_sign_refinement_20261006_r22/SOURCES.json" + ], + "note": "Distinct proposed refinement, not a current-main source." + }, + { + "unit": "reviews/third_order_protocol_20261006", + "kind": "protocol_test_only", + "status": "PENDING_OPEN_PR", + "on_math_main_at_frozen_cut": false, + "pr_heads": [ + { + "number": 379, + "head": "9b3387bdc1cd4e1afc29916d7d7c3f9d922af722", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/379" + } + ], + "representative_paths": [ + "reviews/third_order_protocol_20261006/test_third_order_rate_workflow.py" + ], + "note": "Test/protocol packet only; not a standalone theorem." + }, + { + "unit": "reviews/soft_fold_protocol_20261006", + "kind": "protocol_test_only", + "status": "PENDING_OPEN_PR", + "on_math_main_at_frozen_cut": false, + "pr_heads": [ + { + "number": 370, + "head": "fedd0056c18093e8862b7f6ac2860dc04f8133b9", + "pr_url": "https://github.com/d6g8k5htny-coder/Math-/pull/370" + } + ], + "representative_paths": [], + "note": "Review protocol file and root workflow/test delta; not a standalone theorem." + } + ] +} diff --git a/docs/retro/OPEN_MATH_PR_CANDIDATES_20261023.md b/docs/retro/OPEN_MATH_PR_CANDIDATES_20261023.md new file mode 100644 index 000000000..469c4968d --- /dev/null +++ b/docs/retro/OPEN_MATH_PR_CANDIDATES_20261023.md @@ -0,0 +1,56 @@ +# Open Math pull-request artifacts: retroactive source overlay (23 October 2026) + +**Candidate inventory only — NOT A MATHEMATICAL RESULT.** Scientific effect: NONE. This file is the human-readable companion to [OPEN_MATH_PR_CANDIDATES_20261023.json](OPEN_MATH_PR_CANDIDATES_20261023.json). + +## Boundary and source identity + +- Frozen baseline: `d6g8k5htny-coder/Math-` default main at **`9f3fb6918b28e6378c034ebc19e76d432f5391cb`** (native complete recursive Git tree: 3,216 entries; `truncated:false`). +- Candidate population: **33 open Math pull requests**, including Draft and stacked branches; each exact-head PR's changed-file list was paginated. **#491 had 184 changed files (100+84)** and **#477 had 249 (100+100+49)**. A first page of 100 was never assumed complete. +- Published complement, not a replacement for the Chief of Staff's [313-unit *landed* Math/main inventory](https://github.com/d6g8k5htny-coder/main/pull/527): [original source-bound 33-PR overlay report](https://github.com/d6g8k5htny-coder/main/pull/527#issuecomment-6370536039), actual [pickup/release](https://github.com/d6g8k5htny-coder/main/issues/475#issuecomment-6370267167). The original 313-unit census, 291 proposed orphan units, graph statuses, GB-8a–x assignments and all mathematics remain with their existing owners. +- Scope: one candidate unit is the second-level directory path under `frontiers/`, `reviews/`, `coefficients/`, `companions/` or other research roots that is not present at the *frozen default cut* but appears in an **open PR delta**. A unit may contain many files, a sequence of revisions or tests. **It is not one theorem or one verified implementation.** + +## Results at this immutable cut + +| Area | Distinct pending units | Representative open PRs | +| --- | ---: | --- | +| Formal C293/C294/C296/C299/source-lifetime packages | 5 | Math-#482, #487, #488, #491 with stacked #496/#497, #477 | +| Compact-source-cutoff revision lineage | 7 | #414, #415, #424, #425, #426, #427, #430 | +| Fold-affine and LM006 coefficient proof/code/test packets | 3 | #389, #372, #380/#385 (one shared packet) | +| Engineering review-protocol/test directories | 2 | #379, #370 | +| **Total** | **17** | **Distinct directories, not 17 mathematical theorems** | + +All 17 candidate directories are absent from the frozen Math-main tree and absent from the 313-unit landed ledger at its source cut. Other open PRs modify *existing* directories (for example elder-cusp parity in #492, and downstream hard-gate objects in #490/#397); they are not ignored, but do not increase this denominator. + +Every proposed unit, open PR number and full head SHA, representative path, verification boundary and status are in the machine-readable JSON. Its baseline status is **`PENDING_OPEN_PR`**, never `accepted` or `landed`. + +## Authenticated source-to-implementation samples + +### C293 to C294 to C299 (formal source provenance, not theorem implication) + +At [Math-#482](https://github.com/d6g8k5htny-coder/Math-/pull/482), the C293 `FINAL_SOURCE_INVENTORY.json` declares five Lean files. All **5/5** whole file bodies were read at its immutable PR head, matching expected UTF-8 byte lengths and SHA-256. + +At [Math-#487](https://github.com/d6g8k5htny-coder/Math-/pull/487), C294 declares seven Lean files. All **7/7** whole file bodies likewise match. Three modules have the same Git blobs in both packages: + +| Shared source module | Identical Git blob | +| --- | --- | +| `Lifetime.lean` | `f2508f7f2e3fd42f22f5aa52bc5ead5ff9e73b9a` | +| `TorusTopology.lean` | `ed678ea322fe5315b3aaff44e4e2f06b018399d8` | +| `MorseFiniteCritical.lean` | `989fabc6e8f04b0c4a36dff9b21d33b1299f7b92` | + +[Math-#491](https://github.com/d6g8k5htny-coder/Math-/pull/491) C299's `HOSTED_SOURCE_MANIFEST.json`, Git blob `18d2570643e45e2de06e89ab1a96e9332b0f6064`, expressly declares those three modules' **origin at C294 head `7af365e8c8db1ae0275d4efe08a70a678f153ca2`**. This is a tangible historical *source byte/reuse* chain. It does **not** show C299's complete proof is accepted, that a build succeeded in this stage or that the three theorems are logically interchangeable. #496/#497 are stacked, different heads of that same prospective C299 packet. + +### Distinct coefficient and fold-affine packets + +At [Math-#385](https://github.com/d6g8k5htny-coder/Math-/pull/385), **4/4** LM006 `SOURCES.json` rows (`NOTE.md`, `oned.py`, `test_oned.py`, `RESULTS.json`) were whole-file byte/SHA-256/Git-blob verified at the proposed head. #380 touches the same unit and must not be counted again. + +At [Math-#389](https://github.com/d6g8k5htny-coder/Math-/pull/389), **6/6** declared `SOURCE_FILES.json` rows, including `Contract.lean`, `FoldAffineBridge.lean`, `replay.py`, `test_contract.py`, README and its workflow, match their full declared identities. Across the C293, C294, LM006 and fold-affine samples, **22/22 manifest-listed instances** were authenticated. Neither their mathematical proofs nor their executable test suites were rerun in this audit. A hash helper that failed its own known-answer test was discarded before using the corrected, self-tested implementation. + +## Fail-closed migration rule for future work + +1. **While an associated PR is open**, keep exact commit/path/blob/declared source links as `PENDING_OPEN_PR`. Report missing bytes as `NOT_VERIFIED`, not as nonexistence or acceptance. +2. **For stacked PRs**, retain their ordered dependency/base relationships. Do not treat modified files from an unmerged parent as newly accepted source. +3. **Only after a protected, reviewed merge**, recheck the new default Math SHA and the exact landed source bytes, and update the existing CoS inventory through its current owner. A merge does not itself satisfy the separate mathematical predicates. +4. **Do not manufacture downstream-graph nodes for all 17 units.** The existing `frontiers/downstream_gate_20260925/GRAPH.json` is a specific proof-obligation graph. The complete artifact inventory and that graph have different semantics. Preserve original failures, theorem/status classifications and open premises. +5. Never infer that a `.py` file implements a proof from naming alone. These representative paths are candidates supported by their existing manifest or changed-file association; formal verification, actual execution, reviewer acceptance and dependency consumption require their own authenticated evidence. + +This packet is documentation and source accounting only. It changes no workflow, hard gate, proof, Artifact Index identity, theorem classification, graph edge, permission or required check. Publication is a Draft proposal with separate review and guarded integration still pending.