Prove exact P02-LM-002 endpoint determinant moment bound

frontiers/determinant_moment_20261025/.gitignore

@@ -0,0 +1,2 @@
+.lake/
+__pycache__/

frontiers/determinant_moment_20261025/COMPATIBILITY.md

@@ -0,0 +1,22 @@
+# GP-FOR-192 compiler-compatible successors
+
+Scientific effect NONE. These changes concern this newly introduced execution project, not an accepted parent proof or a historical scientific register.
+
+The actual first hosted run, 36351673121, on Math- commit 9cc0fff64b5e48b48b1ebc5a1bd6ef6b4ae754c7 installed Lean 4.34.1/mathlib d13f23b723b8a846827a245b89c10fc7d3f11612, passed 30 gate tests in each Python mode and verified source hashes, then FAILED to build. It did not reach the axiom audit or earn kernel-checked status. The failure artifact is 10941934636, archive SHA256 446ade8c0a869d19b93d742f43cbe2b4e784bb1ccb115aa975584fe3c1d9fc42. Its build log is retained here as evidence/initial-build-failure.log.
+
+## Three diagnosed repairs
+
+1. Algebra.lean:8 used `def foldPotential` over noncomputable Real division. The successor uses `noncomputable def foldPotential`. The mathematical expression is identical; no new axiom or hypothesis is introduced by this annotation.
+2. Algebra.lean:49 had a `ring` command after `field_simp [hr]` had already closed the goal. Delete that surplus tactic only.
+3. ProbabilityCompanions.lean:15 similarly had a surplus `ring` after `field_simp [hr, hcZ]`. Delete that surplus tactic only.
+
+Original files are retained verbatim as originals/Algebra.lean.txt (SHA256 4c196820c4db8fafc288dd35642828ba577e3544d60aba7d1d6d24f14ad1e8ae) and originals/ProbabilityCompanions.lean.txt (SHA256 4ace6600a476859982c8851ae9097c89b082d3c96291b3c8330bd4cc00bae65d). The newly introduced, unmerged execution copies were replaced by explicitly named AlgebraV2.lean and ProbabilityCompanionsV2.lean; no original carrier was modified. Namespace and all thirteen theorem statements remain unchanged. Tests compare each successor to exactly the documented transformation of its original, including whitespace and all other proof text.
+
+Unused-variable warnings for hcW/hq are retained, not suppressed or removed by broadening a statement. The successor needs its own actual successful build/audit/negative-control run; the existence of this note does not establish success. Statement preservation and kernel evidence remain distinct from independent alignment review.
+
+## DM2 packet import-only successor (25 October 2026)
+
+See SOURCE_MAP.md's observed 16GiB OOM and exact narrow-import successor. All
+13 scalar theorem types and proof bodies remain as above; only their import
+headers change. The two preservation tests bind the exact chosen replacement
+headers and compare every remaining byte. No core formal/ file is edited.

frontiers/determinant_moment_20261025/GLOSSARY.md

@@ -0,0 +1,7 @@
+# Exact object mapping
+
+Jet indices 0..8: q,a,w,z,c40,c31,c22,c13,c04. R=1+sum of all nine absolute values.
+HM and HS: source section 2 endpoint Hessians. Negative: strictly negative quadratic
+form on every nonzero two-vector. W: absolute determinant product restricted to
+HM negative definite and det HS<0. M8: supplied integral upper bound for R^8.
+Base measure in dm2_moment is arbitrary and common to every premise/conclusion.

frontiers/determinant_moment_20261025/LINEAGE_VALIDATION.md

@@ -0,0 +1,76 @@
+# Declared-author lineage validation
+
+Scientific effect: **NONE**. This is an engineering successor to the validator,
+not an alignment acceptance, new proof, or scientific-status authority.
+Implementer: OpenAI / GPT-6 Astra Pro, ChatGPT session
+`github-meaningful-advance-20261005T1610Z`, acting under Dylan Roy's delegation.
+Pickup: main#229 comment 5998762623.
+
+## Observed gap and bounded repair
+
+The previous `check_alignment` compared only `author` and `reviewer`. It ignored
+`proposal_authors` even when a record expressly named an unknown or same-provider
+proposer. It also treated literal UNKNOWN identities as ordinary nonempty strings.
+Thus an ACCEPTED disposition could pass the structural validator despite declared
+lineage contradicting [SCOPE's review contract](SCOPE.md#review-contract).
+This is not evidence that a controller accepted a false review or that a theorem
+passed on an invalid proof. Reviewers withheld the relevant candidate correctly.
+
+The successor validates `provider`, `family`, and `agent` for the main author,
+reviewer, and **every declared proposer**. Values must be nonempty strings.
+Whitespace is collapsed and comparisons are case-insensitive. The following exact
+normalized placeholders are rejected: `unknown`, `unverified`, `unspecified`,
+`tbd`, `n/a`, `none`, `null`, `?`, `not known`, and `not available`.
+Every author's three normalized fields must differ from the reviewer's respective
+fields, preserving the existing single-author distinctness rule.
+
+An absent `proposal_authors` retains the historical single-author record shape.
+An explicit empty list is valid. A present collection must be a list of identity
+objects. Each proposer's optional `targets` must be a nonempty, duplicate-free
+list of names in the reviewed target inventory. Omitting that field does not
+exempt the proposer from the package's identity checks. Contributor `pr` labels
+are descriptive metadata, not authentication.
+
+## Boundaries that remain external
+
+This validator cannot discover undeclared proposers, identify model aliases,
+authenticate a claimed provider/session, or infer a provider from a role or app
+name. It does not prove that all contributors were listed. A controller must still
+read the immutable source, native reviewer evidence and contributor history.
+Unknown lineage must not be replaced by an invented provider to pass the check.
+This change neither authorizes a waiver nor creates a composite-review rule.
+
+Manifest/scope digests, full target coverage, ACCEPTED disposition and immutable
+evidence references remain required. No existing withheld record is edited by
+this change. Old accepted records remain records of their old exact manifests;
+the new manifest must not be substituted into them without a fresh review.
+
+## Source preservation and regression checks
+
+No Lean declaration, target, toolchain, dependency revision, historical proof,
+workflow, axiom audit, build/recheck command or executable negative control is
+changed. `source_check` additionally requires this note and
+`tests/test_alignment_lineage.py` to be hash-bound. The two older Python tests
+that pin the whole gate now pin this separately scoped successor; their proof
+and toolchain pins and all other test logic are unchanged.
+
+The new suite has 23 test methods, including role/field/placeholder subcases,
+malformed identities, matching proposer identities, valid legacy and declared
+proposer records, retained digest/coverage checks and omitted source bindings.
+Against the old gate it reported 132 failing subcases and 8 malformed-party
+errors in each Python mode. After repair all 23 methods passed in both modes.
+The fixtures are synthetic, not fabricated review evidence.
+
+```sh
+python3 -B -S -m unittest discover -s formal/tests -p test_alignment_lineage.py -v
+python3 -B -O -S -m unittest discover -s formal/tests -p test_alignment_lineage.py -v
+python3 -m unittest discover -s formal/tests -v
+python3 -O -m unittest discover -s formal/tests -v
+python3 formal/gate.py
+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.
+Local focused tests are not a Lean kernel replay or independent review.

frontiers/determinant_moment_20261025/README.md

@@ -0,0 +1,39 @@
+# Exact endpoint-Hessian determinant second moment
+
+P02-LM-002: for the source's exact nine-jet endpoint convention and 0<r<=1,
+W²<=16r⁴R⁸; an integrable eighth-radius moment bounded by M8 yields an integrable
+squared weight with expectation<=16M8r⁴. See SOURCE_MAP.md and SCOPE.md.
+
+This supplies a missing formal determinant-moment step for the Palm-tail transfer.
+Concrete Gaussian moments, endpoint identification, normalizer and parent results
+remain open. Author OpenAI/Codex /root; scientific effect NONE.
+
+This isolated additive packet preserves the exact existing formal/gate.py and its
+13 necessary scalar baseline theorem bodies with narrow imports. It does not modify the occupied core gate
+or add a hosted workflow. The dependency lock and Lean/mathlib pins are unchanged.
+Repository-wide CI builds the original core formal package, not this packet.
+
+From this directory, with Lean v4.34.1 on PATH:
+
+```sh
+lake exe cache get
+python -B -S -m unittest discover -s tests -v
+python -B -O -S -m unittest discover -s tests -v
+python -B -S gate.py
+python -B -S gate.py --execute
+```
+
+The gate's local exact-commit receipt and complete logs are produced under
+.lake/formal-evidence/. Successful local execution is distinct from trusted hosted
+execution and independent statement alignment. Both require their own evidence.
+A nonauthor same-provider source review is recorded separately and does not satisfy
+the unchanged provider-distinct alignment validator. No accepted alignment record
+or parent acceptance is claimed. Controls and actual run evidence are delivered
+separately; no old result is rebound to this new source.
+
+## Import-only memory repair
+
+The original full-Mathlib build passed but kernel replay exceeded 16GiB.
+SOURCE_MAP.md records that failure and the narrow-import successor. Every
+scalar statement/proof body, gate.py, pin and rejection control is preserved;
+only imports and their exact preservation-test expectations changed.

frontiers/determinant_moment_20261025/ResearchFormalCoreR1.lean

@@ -0,0 +1,3 @@
+import ResearchFormalCoreR1.AlgebraV2
+import ResearchFormalCoreR1.ProbabilityCompanionsV2
+import ResearchFormalCoreR1.DeterminantMoment

frontiers/determinant_moment_20261025/ResearchFormalCoreR1/AlgebraV2.lean

@@ -0,0 +1,53 @@
+import Mathlib.Basic.Real.Basic
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Ring
+import Mathlib.Tactic.NormNum
+
+namespace ResearchFormalCoreR1
+
+set_option autoImplicit false
+
+/-- Canonical A₂ normal-form potential, parameterized by `s` with λ = s². -/
+noncomputable def foldPotential (s x : ℝ) : ℝ := -(x ^ 3) / 3 + (s ^ 2) * x
+
+/-- EC-005: exact canonical fold-gap identity in the normalized coordinate. -/
+theorem ec005_fold_gap (s : ℝ) :
+    foldPotential s s - foldPotential s (-s) = (2 * s) ^ 3 / 6 := by
+  unfold foldPotential
+  ring
+
+/-- EC-008: scalar polynomial companion for the planar collision-Gram determinant.
+    This is not the matrix-construction theorem. -/
+theorem ec008_factor_expansion (c s : ℝ) :
+    2 * s ^ 2 *
+        ((s ^ 2 * (3 * c ^ 4 + 3 * c ^ 2 * s ^ 2 + s ^ 4) / 24) *
+            (s ^ 2 * (4 * c ^ 2 + s ^ 2) / 2) -
+          (-c * s ^ 2 * (2 * c ^ 2 + s ^ 2) / 4) ^ 2) =
+      s ^ 8 * (c ^ 2 + s ^ 2) * (3 * c ^ 2 + s ^ 2) / 24 := by
+  ring
+
+/-- EC-010, generic chart: declared convex-combination polynomial identity. -/
+theorem ec010_generic (α K c η : ℝ) :
+    (K + 8 * α * c * η) ^ 2 + 64 * α * (1 - α) * c ^ 2 * η ^ 2 =
+      (1 - α) * K ^ 2 + α * (K + 8 * c * η) ^ 2 := by
+  ring
+
+/-- EC-010, transverse chart: declared convex-combination polynomial identity. -/
+theorem ec010_transverse (α a η : ℝ) :
+    (a + (1 - 2 * α) * η) ^ 2 + 4 * α * (1 - α) * η ^ 2 =
+      (1 - α) * (a + η) ^ 2 + α * (a - η) ^ 2 := by
+  ring
+
+/-- EC-011: scalar cancellation companion to the adjoint-orbit calculation.
+    It does not formalize the ODE, Hessian symmetry, or section normalization. -/
+theorem ec011_scalar_cancellation (h w g : ℝ) :
+    (-h * w) * g + w * (h * g) = 0 := by
+  ring
+
+/-- EC-014: exact contact-power scalar identity for nonzero separation.
+    It does not formalize the six-pin matrix determinant or density transform. -/
+theorem ec014_contact_power (r : ℝ) (hr : r ≠ 0) :
+    (r ^ 3 / 6) * (1 / r ^ 5) * r ^ 2 = (1 / 6 : ℝ) := by
+  field_simp [hr]
+
+end ResearchFormalCoreR1