From afa067cd1a6f5937694a2b30cb740f5c70bea36b Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Fri, 23 Oct 2026 15:25:55 -0500 Subject: [PATCH] Record three existing formal document implementation chains --- ....formal-implementation-links-20261023.json | 227 ++++++++++++++++++ 1 file changed, 227 insertions(+) create mode 100644 docs/retro/GB-8q.formal-implementation-links-20261023.json diff --git a/docs/retro/GB-8q.formal-implementation-links-20261023.json b/docs/retro/GB-8q.formal-implementation-links-20261023.json new file mode 100644 index 000000000..6e32e6260 --- /dev/null +++ b/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" + } +}