retro(GB-8q): record three formal implementation chains

docs/retro/GB-8q.formal-implementation-links-20261023.json

@@ -0,0 +1,227 @@
+{
+  "chains": [
+    {
+      "declared_targets": [
+        "ResearchFormalCoreR1.p02_lm009_moment40_tail_finite",
+        "ResearchFormalCoreR1.p02_lm009_moment40_tail_of_finite",
+        "ResearchFormalCoreR1.p02_lm009_moment40_family_r3_interval",
+        "ResearchFormalCoreR1.p02_lm009_moment40_family_r3_of_interval"
+      ],
+      "document": {
+        "bytes": 5503,
+        "commit": "9f3fb6918b28e6378c034ebc19e76d432f5391cb",
+        "git_blob": "b7cdbe5a3d5b5e4ca0c6aee21c7319b8961d1322",
+        "path": "formal/MOMENT_GENERALITY.md",
+        "repository": "d6g8k5htny-coder/Math-",
+        "sha256": "5386c763f95ecd0946e0f23a22d1ba90e7956ff1a1bfcada0d454d1b5ace0cf2"
+      },
+      "edge_status": "CANDIDATE_DEPENDENCY_EDGE",
+      "edges": [
+        {
+          "relation": "declared_formalization_source",
+          "source_role": "document",
+          "target_role": "lean_source"
+        },
+        {
+          "relation": "checks_declarations_and_finite_models",
+          "source_role": "source_wiring_test",
+          "target_role": "lean_source"
+        },
+        {
+          "relation": "checks_manifest_source_identity",
+          "source_role": "source_wiring_test",
+          "target_role": "document"
+        }
+      ],
+      "lean_source": {
+        "bytes": 4543,
+        "commit": "9f3fb6918b28e6378c034ebc19e76d432f5391cb",
+        "git_blob": "2398c6b0e7920ed01cac8d4738ba4f829a9fb0f1",
+        "path": "formal/ResearchFormalCoreR1/MomentGenerality.lean",
+        "repository": "d6g8k5htny-coder/Math-",
+        "sha256": "fdec55f1602938cd8fdb5b71535962e76a9671bf230dea53868b14147fb3b509"
+      },
+      "manifest_target_range": {
+        "end_exclusive": 40,
+        "start_inclusive": 36
+      },
+      "root_import": "import ResearchFormalCoreR1.MomentGenerality",
+      "source_wiring_test": {
+        "bytes": 6432,
+        "commit": "9f3fb6918b28e6378c034ebc19e76d432f5391cb",
+        "git_blob": "22672d3df43d92dac10a61122ed149a93a827d63",
+        "path": "formal/tests/test_moment_generality.py",
+        "repository": "d6g8k5htny-coder/Math-",
+        "sha256": "c6bdd3a3952358a14e2a211f8f6369367ab80703e8eb5196ec9c9f3a97878c8d"
+      }
+    },
+    {
+      "declared_targets": [
+        "ResearchFormalCoreR1.p02_lm009_markov_event",
+        "ResearchFormalCoreR1.p02_lm009_badJet_measurable",
+        "ResearchFormalCoreR1.p02_lm009_badJet_subset",
+        "ResearchFormalCoreR1.p02_lm009_moment40_tail",
+        "ResearchFormalCoreR1.p02_lm009_moment40_weighted_r4",
+        "ResearchFormalCoreR1.p02_lm009_moment40_weighted_r3",
+        "ResearchFormalCoreR1.p02_lm009_moment40_family_r3"
+      ],
+      "document": {
+        "bytes": 5676,
+        "commit": "9f3fb6918b28e6378c034ebc19e76d432f5391cb",
+        "git_blob": "d45f5259114fcfdc935da54d152577904e963a54",
+        "path": "formal/MOMENT_TAIL.md",
+        "repository": "d6g8k5htny-coder/Math-",
+        "sha256": "20ecddcd830c41935dc4b366882db4d0432240932af6632d025b981f90e044bd"
+      },
+      "edge_status": "CANDIDATE_DEPENDENCY_EDGE",
+      "edges": [
+        {
+          "relation": "declared_formalization_source",
+          "source_role": "document",
+          "target_role": "lean_source"
+        },
+        {
+          "relation": "checks_declarations_and_finite_models",
+          "source_role": "source_wiring_test",
+          "target_role": "lean_source"
+        },
+        {
+          "relation": "checks_manifest_source_identity",
+          "source_role": "source_wiring_test",
+          "target_role": "document"
+        }
+      ],
+      "lean_source": {
+        "bytes": 7197,
+        "commit": "9f3fb6918b28e6378c034ebc19e76d432f5391cb",
+        "git_blob": "c8282f297ac22c25d68e94a5e432c2633bac0bab",
+        "path": "formal/ResearchFormalCoreR1/MomentTail.lean",
+        "repository": "d6g8k5htny-coder/Math-",
+        "sha256": "87fe3ee90afc52d8c2652881f1ae195d1b0b15a2ffc18c84d6166d1a4d0de2aa"
+      },
+      "manifest_target_range": {
+        "end_exclusive": 36,
+        "start_inclusive": 29
+      },
+      "root_import": "import ResearchFormalCoreR1.MomentTail",
+      "source_wiring_test": {
+        "bytes": 5481,
+        "commit": "9f3fb6918b28e6378c034ebc19e76d432f5391cb",
+        "git_blob": "d0c0869f3d449b48a808dbc434b5c66b5a60388d",
+        "path": "formal/tests/test_moment_tail.py",
+        "repository": "d6g8k5htny-coder/Math-",
+        "sha256": "4aa8ef5b1646f4cbef837a5b024da18fd75bf9d5dcb1489835482874d8cb48df"
+      }
+    },
+    {
+      "declared_targets": [
+        "ResearchFormalCoreR1.weightPerturbation_integral",
+        "ResearchFormalCoreR1.weightPerturbation_setIntegral",
+        "ResearchFormalCoreR1.weightPerturbation_normalizer_lower",
+        "ResearchFormalCoreR1.weightPerturbation_event_integral_bounds",
+        "ResearchFormalCoreR1.weightPerturbation_quotient_bound",
+        "ResearchFormalCoreR1.weightedLaw_event_perturbation",
+        "ResearchFormalCoreR1.weightedLaw_event_perturbation_r2"
+      ],
+      "document": {
+        "bytes": 6508,
+        "commit": "9f3fb6918b28e6378c034ebc19e76d432f5391cb",
+        "git_blob": "dbd204fbfbb4b00165326b9132ca636955d71c9e",
+        "path": "formal/WEIGHT_PERTURBATION.md",
+        "repository": "d6g8k5htny-coder/Math-",
+        "sha256": "0ac969b86f5b2cc4e84b4bb61790c7497164b923dc5f3fc5be99195b75b1b212"
+      },
+      "edge_status": "CANDIDATE_DEPENDENCY_EDGE",
+      "edges": [
+        {
+          "relation": "declared_formalization_source",
+          "source_role": "document",
+          "target_role": "lean_source"
+        },
+        {
+          "relation": "checks_declarations_and_finite_models",
+          "source_role": "source_wiring_test",
+          "target_role": "lean_source"
+        },
+        {
+          "relation": "checks_manifest_source_identity",
+          "source_role": "source_wiring_test",
+          "target_role": "document"
+        }
+      ],
+      "lean_source": {
+        "bytes": 6728,
+        "commit": "9f3fb6918b28e6378c034ebc19e76d432f5391cb",
+        "git_blob": "8dfd693265fda16fc4f7d82f493ce964013d81e2",
+        "path": "formal/ResearchFormalCoreR1/WeightPerturbation.lean",
+        "repository": "d6g8k5htny-coder/Math-",
+        "sha256": "50ce15709a133da12a0b4333cc653d26c5fd8a412976c975a7c2f3b25ed5c00f"
+      },
+      "manifest_target_range": {
+        "end_exclusive": 47,
+        "start_inclusive": 40
+      },
+      "root_import": "import ResearchFormalCoreR1.WeightPerturbation",
+      "source_wiring_test": {
+        "bytes": 8218,
+        "commit": "9f3fb6918b28e6378c034ebc19e76d432f5391cb",
+        "git_blob": "ce462f979166273e088493c16072a5af7a6bd72c",
+        "path": "formal/tests/test_weight_perturbation.py",
+        "repository": "d6g8k5htny-coder/Math-",
+        "sha256": "0a978f8b56faceb3be6c91dea62b8837e06874ef4fcad3356842aa475d339854"
+      }
+    }
+  ],
+  "controls": {
+    "manifest": {
+      "bytes": 8630,
+      "commit": "9f3fb6918b28e6378c034ebc19e76d432f5391cb",
+      "git_blob": "444642fb4d4987d50201c5e962fc421aab00b9eb",
+      "path": "formal/manifest.json",
+      "repository": "d6g8k5htny-coder/Math-",
+      "sha256": "7149915669414e22f593ce2c6540c5e10d922eb758c7464794fc64764e679778"
+    },
+    "root_imports": {
+      "bytes": 339,
+      "commit": "9f3fb6918b28e6378c034ebc19e76d432f5391cb",
+      "git_blob": "7e484d7d5037812fba329ba3e4c9b8eed8e4de76",
+      "path": "formal/ResearchFormalCoreR1.lean",
+      "repository": "d6g8k5htny-coder/Math-",
+      "sha256": "c55cc116ff3ffbffdb692226e215450a5d2e85b60d27b1b04d529b87bdef38f8"
+    }
+  },
+  "limits": [
+    "Source-availability and declared-dependency evidence only; no scientific acceptance or independent semantic alignment.",
+    "This appendix adds no adopted graph node, graph input or v2 binding and grants no status authority.",
+    "Historical NO IMPLEMENTATION FOUND rows remain dated heuristic search observations, not verified absence of these external Lean/test carriers.",
+    "The nine source files and two control files are pinned at one immutable Math commit; no current-tip tracking or silent repinning.",
+    "Existing GB-8q subject records, source files, mathematical statements and prior reviews remain unchanged.",
+    "The separate MeasureBridge, WeightedLaw and D2Schur subjects are outside this appendix."
+  ],
+  "record_kind": "source_witness_appendix",
+  "rollout": "RETRO-MATH-BIND-01 / GB-8q",
+  "schema_version": 1,
+  "scientific_effect": "NONE",
+  "scientific_status_authority": false,
+  "source_records": {
+    "author_pickup": "https://github.com/d6g8k5htny-coder/main/pull/553#issuecomment-6373981006",
+    "discovery": "https://github.com/d6g8k5htny-coder/main/pull/553#issuecomment-6373679175",
+    "handoff": "https://github.com/d6g8k5htny-coder/main/issues/539#issuecomment-6373697997"
+  },
+  "source_reported_status": {
+    "alignment_status": "PENDING_INDEPENDENT_REVIEW",
+    "formalization_status": "proved",
+    "scientific_effect": "NONE"
+  },
+  "verification": {
+    "declared_target_name_matches": 18,
+    "kernel_verification": "NOT_CLAIMED",
+    "kind": "byte_identity_and_static_source_wiring",
+    "lean_execution": "NOT_RUN",
+    "manifest_sha256_matches": 9,
+    "root_import_matches": 3,
+    "semantic_alignment": "PENDING_INDEPENDENT_REVIEW",
+    "source_files": 9,
+    "source_test_execution": "NOT_RUN"
+  }
+}