Formal gate: reject hidden/unregistered Lean declarations

formal/DECLARATION_ADMISSION.md

@@ -0,0 +1,13 @@
+# Package declaration admission hardening
+
+Scientific effect: **NONE**. Engineering successor for RF-GATE-01 (Math- issue #310), implemented by OpenAI / GPT-5.6 Sol in `round11-gate-hardening-20261005`. The #309 mathematical declarations are preserved.
+
+The predecessor used a column-zero theorem/lemma regex. Lean accepts declarations outside it, so declarations could compile outside manifest and axiom coverage. This successor intentionally enforces a conservative grammar rather than claiming to parse arbitrary Lean: one `namespace ResearchFormalCoreR1`; column-zero `theorem`, `lemma`, `def`, or `noncomputable def`; declaration-bearing alternatives and nested namespaces fail closed after comments and strings are removed.
+
+The manifest records all package declarations, not just theorem targets. Execute-time transitive-axiom auditing covers definitions as well as theorems; the historical target-only `axioms` receipt field is retained and `declaration_axioms` is additive. Lean4.34.1, dependency pins, leanchecker and all five existing negative controls are unchanged.
+
+Test-first predecessor `82f4de13f0e41253740d880f26fdc63fda772323` / run37394891831 failed with nine intended regression failures before Lean installation. A successor must pass those regressions, complete Python suites in both modes, source identity and the actual pinned Lean/leanchecker/axiom/type workflow. This is engineering evidence, not independent mathematical alignment or reviewer authentication.
+
+## Incorporated successor status
+
+The source-scanner design above is retained as historical test-first context. The incorporated production gate is the reviewed RF-GATE-01 compiled-environment inventory described in [`GATE_HARDENING.md`](GATE_HARDENING.md): the conservative source grammar remains a fail-closed pre-check, while admission completeness and package-wide axiom closure are decided from Lean's compiled environment. `gate_helper.py` preserves that reviewed implementation byte-for-byte; `gate.py` is the bound compatibility entrypoint that additionally retains current-main's exact Lean-release and clean-dependency observations. Neither layer changes mathematical statements or supplies independent alignment.

formal/LINEAGE_VALIDATION.md

@@ -72,5 +72,5 @@ python3 formal/gate.py --execute
 
 Only the focused suite was run in the implementer's partial staging checkout at
 publication. Full-suite, exact-source and Lean execution claims require their
-actual complete-checkout results; the expected main-based suite is 97 tests.
+actual complete-checkout results; the complete suite size is not a protocol constant; use the actual current-run count.
 Local focused tests are not a Lean kernel replay or independent review.

formal/manifest.json

@@ -94,45 +94,102 @@
     "ResearchFormalCoreR1.d2_gaussian_control",
     "ResearchFormalCoreR1.d2_degenerate_control"
   ],
+  "compiled_inventory": [
+    ["def", "user", "ResearchFormalCoreR1.AlgebraV2", "ResearchFormalCoreR1.foldPotential"],
+    ["theorem", "aux", "ResearchFormalCoreR1.AlgebraV2", "ResearchFormalCoreR1.foldPotential._proof_1"],
+    ["def", "user", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Alpha"],
+    ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Alpha._proof_1"],
+    ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Alpha._proof_2"],
+    ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Alpha.eq_1"],
+    ["def", "user", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Delta"],
+    ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Delta.eq_1"],
+    ["def", "user", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2DetV"],
+    ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2DetV.eq_1"],
+    ["def", "user", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Gamma"],
+    ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Gamma.eq_1"],
+    ["def", "user", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Numerator"],
+    ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Numerator.eq_1"],
+    ["def", "user", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Schur"],
+    ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Schur._proof_1"],
+    ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Schur.eq_1"],
+    ["def", "user", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Tau"],
+    ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Tau._proof_1"],
+    ["theorem", "aux", "ResearchFormalCoreR1.D2Schur", "ResearchFormalCoreR1.d2Tau.eq_1"],
+    ["theorem", "aux", "ResearchFormalCoreR1.MeasureBridge", "ResearchFormalCoreR1.p02_lm008_integral_cs._simp_1_1"],
+    ["theorem", "aux", "ResearchFormalCoreR1.MomentGenerality", "ResearchFormalCoreR1.p02_lm009_moment40_tail_finite._simp_1_1"],
+    ["theorem", "aux", "ResearchFormalCoreR1.MomentGenerality", "ResearchFormalCoreR1.p02_lm009_moment40_tail_finite._simp_1_2"],
+    ["theorem", "aux", "ResearchFormalCoreR1.MomentGenerality", "ResearchFormalCoreR1.p02_lm009_moment40_tail_finite._simp_1_3"],
+    ["theorem", "aux", "ResearchFormalCoreR1.MomentGenerality", "ResearchFormalCoreR1.p02_lm009_moment40_tail_finite._simp_1_4"],
+    ["theorem", "aux", "ResearchFormalCoreR1.MomentGenerality", "ResearchFormalCoreR1.p02_lm009_moment40_tail_finite._simp_1_5"],
+    ["theorem", "aux", "ResearchFormalCoreR1.MomentGenerality", "ResearchFormalCoreR1.p02_lm009_moment40_tail_finite._simp_1_6"],
+    ["theorem", "aux", "ResearchFormalCoreR1.MomentGenerality", "ResearchFormalCoreR1.p02_lm009_moment40_tail_finite._simp_1_7"],
+    ["def", "user", "ResearchFormalCoreR1.MomentTail", "ResearchFormalCoreR1.badJetEvent"],
+    ["theorem", "aux", "ResearchFormalCoreR1.MomentTail", "ResearchFormalCoreR1.p02_lm009_moment40_tail._simp_1_1"],
+    ["theorem", "aux", "ResearchFormalCoreR1.MomentTail", "ResearchFormalCoreR1.p02_lm009_moment40_tail._simp_1_2"],
+    ["theorem", "aux", "ResearchFormalCoreR1.MomentTail", "ResearchFormalCoreR1.p02_lm009_moment40_tail._simp_1_3"],
+    ["theorem", "aux", "ResearchFormalCoreR1.MomentTail", "ResearchFormalCoreR1.p02_lm009_moment40_tail._simp_1_4"],
+    ["theorem", "aux", "ResearchFormalCoreR1.MomentTail", "ResearchFormalCoreR1.p02_lm009_moment40_tail._simp_1_5"],
+    ["theorem", "aux", "ResearchFormalCoreR1.MomentTail", "ResearchFormalCoreR1.p02_lm009_moment40_tail._simp_1_6"],
+    ["theorem", "aux", "ResearchFormalCoreR1.MomentTail", "ResearchFormalCoreR1.p02_lm009_moment40_tail._simp_1_7"],
+    ["theorem", "aux", "ResearchFormalCoreR1.ProbabilityCompanionsV2", "ResearchFormalCoreR1.p02_lm008_r2_cancel._simp_1_1"],
+    ["theorem", "aux", "ResearchFormalCoreR1.ProbabilityCompanionsV2", "ResearchFormalCoreR1.p02_lm008_r2_cancel._simp_1_2"],
+    ["theorem", "aux", "ResearchFormalCoreR1.ProbabilityCompanionsV2", "ResearchFormalCoreR1.p02_lm008_r2_cancel._simp_1_3"],
+    ["theorem", "aux", "ResearchFormalCoreR1.ProbabilityCompanionsV2", "ResearchFormalCoreR1.p02_lm008_r2_cancel._simp_1_4"],
+    ["theorem", "aux", "ResearchFormalCoreR1.ProbabilityCompanionsV2", "ResearchFormalCoreR1.p02_lm008_r2_cancel._simp_1_5"],
+    ["theorem", "aux", "ResearchFormalCoreR1.ProbabilityCompanionsV2", "ResearchFormalCoreR1.p02_lm008_r2_cancel._simp_1_6"],
+    ["theorem", "aux", "ResearchFormalCoreR1.ProbabilityCompanionsV2", "ResearchFormalCoreR1.p02_lm008_r2_cancel._simp_1_7"],
+    ["theorem", "aux", "ResearchFormalCoreR1.WeightPerturbation", "ResearchFormalCoreR1.weightedLaw_event_perturbation_r2._simp_1_1"],
+    ["theorem", "aux", "ResearchFormalCoreR1.WeightPerturbation", "ResearchFormalCoreR1.weightedLaw_event_perturbation_r2._simp_1_2"],
+    ["theorem", "aux", "ResearchFormalCoreR1.WeightPerturbation", "ResearchFormalCoreR1.weightedLaw_event_perturbation_r2._simp_1_3"],
+    ["theorem", "aux", "ResearchFormalCoreR1.WeightPerturbation", "ResearchFormalCoreR1.weightedLaw_event_perturbation_r2._simp_1_4"],
+    ["theorem", "aux", "ResearchFormalCoreR1.WeightPerturbation", "ResearchFormalCoreR1.weightedLaw_event_perturbation_r2._simp_1_5"],
+    ["theorem", "aux", "ResearchFormalCoreR1.WeightPerturbation", "ResearchFormalCoreR1.weightedLaw_event_perturbation_r2._simp_1_6"],
+    ["theorem", "aux", "ResearchFormalCoreR1.WeightPerturbation", "ResearchFormalCoreR1.weightedLaw_event_perturbation_r2._simp_1_7"],
+    ["def", "user", "ResearchFormalCoreR1.WeightedLaw", "ResearchFormalCoreR1.weightedLaw"],
+    ["theorem", "aux", "ResearchFormalCoreR1.WeightedLaw", "ResearchFormalCoreR1.weightedLaw._proof_1"],
+    ["theorem", "aux", "ResearchFormalCoreR1.WeightedLaw", "ResearchFormalCoreR1.weightedLaw.eq_1"]
+  ],
   "files": {
     ".gitignore": "b34af236d1df9e39ed4f98fca51702530ce76bdee4e1a69512f6caed933c3374",
     "COMPATIBILITY.md": "33721aad32f82131a6956a06b58c5bc41f5d28f26efe840a99a4d51ad60cf247",
     "GLOSSARY.md": "6bdda2ce054915efc26e8db462dbe8fd9d0c1db30e02328857bebc6568e05ce9",
-    "README.md": "52c4829c23c5caa8142b4c8d7152766b92cb966b1cb8213ff5210e6fa4ef080e",
+    "README.md": "00fa04b316e1a208a38b80c726c5763aea09605df4da6f36e0a7dee195c71417",
     "ResearchFormalCoreR1/AlgebraV2.lean": "4480708263c40a2f7f03f12ef7e15f0eb4f8193c2dccbb253921a7ec251863c3",
     "ResearchFormalCoreR1/ProbabilityCompanionsV2.lean": "338452a0c2ba24d016059354d543cc995b8cb29c9d4a41d98bb93499f5f8cb8f",
     "ResearchFormalCoreR1.lean": "c55cc116ff3ffbffdb692226e215450a5d2e85b60d27b1b04d529b87bdef38f8",
     "SCOPE.md": "8fa7e879e23742aba77df8687659ca9dcfd13a19e0add6192229c2f80629b3cb",
     "blueprint/src/content.tex": "0c976e8e4a5e69a443e93796c8f6cbf91bf73c224448c4256de72a041e04161f",
     "evidence/initial-build-failure.log": "43393d2e2b3148a2453e3092a1ff04e257dbd4a6dc97eb2853a8bc0451002591",
-    "gate.py": "25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a",
+    "gate.py": "ff8a5374597772b2d37054fd722c2243c4b552a63802c69f7c605519832be6c4",
     "lake-manifest.json": "d63753befccc21923783a5085148e3ff028d97134ea52f5a08bd87ecf1b0b043",
     "lakefile.toml": "d629891716c169404d1f0d76492441c8dd66f1e790b1b8b0819e51c8d5059255",
     "lean-toolchain": "d5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b",
     "originals/Algebra.lean.txt": "4c196820c4db8fafc288dd35642828ba577e3544d60aba7d1d6d24f14ad1e8ae",
     "originals/ProbabilityCompanions.lean.txt": "4ace6600a476859982c8851ae9097c89b082d3c96291b3c8330bd4cc00bae65d",
-    "tests/test_gate.py": "e279e5b1e8c14f913728a18fa345dd1060d856799369fc4c9dce4a5f6dfb7574",
+    "tests/test_gate.py": "5df769901bbf53a7a434c2794c8685242ecfdc32f15d72fae8c2030dff7a9aa2",
     "ResearchFormalCoreR1/MeasureBridge.lean": "28ac130db490c3c3e2fbfabf3ac5be43c854ab1468bf573bf5a8c0dd2c50955f",
     "MEASURE_BRIDGE.md": "bdb6c06f359f17d493d6057adbed61edb20236b7a3a3ca4880ae0b33d8a7200e",
     "tests/test_measure_bridge.py": "0e54b2ed7c2e197967180993b4c0c1ece1e63576ad34fd74ac232a4d507628a2",
     "ResearchFormalCoreR1/WeightedLaw.lean": "f31dfd2cd048cc0c0446c54c46d89c9cdd5d7bb9d76e9d8d16b7c034f351d736",
     "WEIGHTED_LAW.md": "a530dc957923c4c9111b734d8fcc0f4cd3cdba45b08480cfc2e241ecefc5fba4",
-    "tests/test_weighted_law.py": "46c0f11a7a441f085cd339a9f61aa27d1574691c279ef8b6a7a500d089374d27",
+    "tests/test_weighted_law.py": "acd4da143467fdcfefd1b041f18d48a7be3c3504ff1edd7e3d76df3fa5e917b0",
     "ResearchFormalCoreR1/MomentTail.lean": "87fe3ee90afc52d8c2652881f1ae195d1b0b15a2ffc18c84d6166d1a4d0de2aa",
     "MOMENT_TAIL.md": "20ecddcd830c41935dc4b366882db4d0432240932af6632d025b981f90e044bd",
-    "tests/test_moment_tail.py": "4aa8ef5b1646f4cbef837a5b024da18fd75bf9d5dcb1489835482874d8cb48df",
+    "tests/test_moment_tail.py": "d50c46220ff6c4b95ee1cb42b037738740d314508019161ad6fb478ed3b0f7d5",
     "evidence/moment-tail-initial-build-failure.log": "61bee2d55d0dd548b0bccc4d2e40970f654fca8ab1385af7f371592d45c0ab08",
     "ResearchFormalCoreR1/MomentGenerality.lean": "fdec55f1602938cd8fdb5b71535962e76a9671bf230dea53868b14147fb3b509",
     "MOMENT_GENERALITY.md": "5386c763f95ecd0946e0f23a22d1ba90e7956ff1a1bfcada0d454d1b5ace0cf2",
-    "tests/test_moment_generality.py": "c6bdd3a3952358a14e2a211f8f6369367ab80703e8eb5196ec9c9f3a97878c8d",
+    "tests/test_moment_generality.py": "66a0a3d319cd5816d355c3bfa6100f16fa681bb95a2263426af6e14a9057a05d",
     "tests/test_alignment_lineage.py": "c510c6566d7689bebde76843582e9936dfa9e62e783b816b5e4f63d83434b893",
     "LINEAGE_VALIDATION.md": "bba9d0a859f1ba45670fe122e4e72ae1094a2226de98aa814d838b0baaf61815",
     "ResearchFormalCoreR1/WeightPerturbation.lean": "50ce15709a133da12a0b4333cc653d26c5fd8a412976c975a7c2f3b25ed5c00f",
     "WEIGHT_PERTURBATION.md": "0ac969b86f5b2cc4e84b4bb61790c7497164b923dc5f3fc5be99195b75b1b212",
-    "tests/test_weight_perturbation.py": "0a978f8b56faceb3be6c91dea62b8837e06874ef4fcad3356842aa475d339854",
+    "tests/test_weight_perturbation.py": "115f3e027e29da1ae7e52c364d8ad6367c6f47658c29dcf5c325a796a35f9213",
     "evidence/weight-perturbation-initial-build-failure.log": "2abe4ec4bcfa4de282e7983ffebb225af21308c60b84083a1696bcced31b9c7c",
     "D2_SCHUR.md": "c25f4add4c92479ae0f6dfaac43fc9be7a71766f050a79acbc2c72acf47ef4d3",
     "ResearchFormalCoreR1/D2Schur.lean": "d3fb3ed7b4043227f1d5a06e208de9d94eb413c067e9d0f8802388407c9e15b9",
-    "tests/test_d2_schur.py": "3db66384d7068129346871ca169e602b5bcd2594693090f4ddfc5d5297678f83"
+    "tests/test_d2_schur.py": "89badcfc82490290d7ad3671cd6f40f8980824b82a3945796e87c47712585ed9",
+    "tests/test_inventory_gate.py": "93bb736b73a8c93a0a6c5aa7ce8822d15013b32897cd6864bd97d0b1c9914bdb",
+    "GATE_HARDENING.md": "328addf8aa0946b0d62249305047ecd8e3e74b6efc44dbcf400442e5c98aa735"
   }
 }

formal/manifest.overlay.json

@@ -0,0 +1,13 @@
+{
+  "files": {
+    "DECLARATION_ADMISSION.md": "88bda3e378128ef3b8f4cf4e8842ba4a6f89ee5bcecf810a5a3b583079a0cedb",
+    "LINEAGE_VALIDATION.md": "593f8cbdb0a9261a57eded9c559963a9247a1036d5e501c9d6bbd77efe9b0c3a",
+    "README.md": "52c4829c23c5caa8142b4c8d7152766b92cb966b1cb8213ff5210e6fa4ef080e",
+    "gate.py": "509b6eb3b5ee2dc7e42810a40b07192b0feaf3924c9dbb398db43cb44e16e731",
+    "gate_helper.py": "ff8a5374597772b2d37054fd722c2243c4b552a63802c69f7c605519832be6c4",
+    "tests/test_declaration_admission.py": "6a869f853e886772a825794f06a8399fb62a541fa45e6d881029bb57e4dd7af7",
+    "tests/test_gate.py": "62bd0f6b3c149b30aa4ad2817aba59667b87ed5c80445f3fd64b005814968a9b",
+    "tests/test_gate_compatibility.py": "920811ebad0bf7f5c9d057d4396669ad340aae353e224d2e5dbc32ae94587b57"
+  },
+  "schema_version": 1
+}

formal/tests/test_d2_schur.py

@@ -52,7 +52,7 @@ def test_manifest_exact_extension(self):
         for path in (MODULE, 'D2_SCHUR.md', 'tests/test_d2_schur.py'):
             self.assertEqual(hashlib.sha256((ROOT/path).read_bytes()).hexdigest(), m['files'][path])
         self.assertEqual(m['files']['gate.py'],
-                         '25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a')
+                         'ff8a5374597772b2d37054fd722c2243c4b552a63802c69f7c605519832be6c4')
         self.assertEqual(m['files']['ResearchFormalCoreR1/WeightPerturbation.lean'],
                          '50ce15709a133da12a0b4333cc653d26c5fd8a412976c975a7c2f3b25ed5c00f')