docs(retro): account for unmerged Math proof-to-implementation source candidates

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."
+    }
+  ]
+}