diff --git a/frontiers/determinant_moment_20261025/.gitignore b/frontiers/determinant_moment_20261025/.gitignore
new file mode 100644
index 000000000..ae7367994
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/.gitignore
@@ -0,0 +1,2 @@
+.lake/
+__pycache__/
diff --git a/frontiers/determinant_moment_20261025/COMPATIBILITY.md b/frontiers/determinant_moment_20261025/COMPATIBILITY.md
new file mode 100644
index 000000000..629825c5e
--- /dev/null
+++ b/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.
diff --git a/frontiers/determinant_moment_20261025/GLOSSARY.md b/frontiers/determinant_moment_20261025/GLOSSARY.md
new file mode 100644
index 000000000..eb828fef7
--- /dev/null
+++ b/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.
diff --git a/frontiers/determinant_moment_20261025/LINEAGE_VALIDATION.md b/frontiers/determinant_moment_20261025/LINEAGE_VALIDATION.md
new file mode 100644
index 000000000..5a0c5d20e
--- /dev/null
+++ b/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.
diff --git a/frontiers/determinant_moment_20261025/README.md b/frontiers/determinant_moment_20261025/README.md
new file mode 100644
index 000000000..0b9eae248
--- /dev/null
+++ b/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.
diff --git a/frontiers/determinant_moment_20261025/ResearchFormalCoreR1.lean b/frontiers/determinant_moment_20261025/ResearchFormalCoreR1.lean
new file mode 100644
index 000000000..dfe972cb6
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/ResearchFormalCoreR1.lean
@@ -0,0 +1,3 @@
+import ResearchFormalCoreR1.AlgebraV2
+import ResearchFormalCoreR1.ProbabilityCompanionsV2
+import ResearchFormalCoreR1.DeterminantMoment
diff --git a/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/AlgebraV2.lean b/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/AlgebraV2.lean
new file mode 100644
index 000000000..768d0bab9
--- /dev/null
+++ b/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
diff --git a/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/DeterminantMoment.lean b/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/DeterminantMoment.lean
new file mode 100644
index 000000000..93e296ca1
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/DeterminantMoment.lean
@@ -0,0 +1,218 @@
+import Mathlib.MeasureTheory.Integral.Bochner.Basic
+import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
+import Mathlib.Topology.Instances.Matrix
+import Mathlib.MeasureTheory.Order.Group.Lattice
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Ring
+import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.FunProp
+import Mathlib.Tactic.Push
+
+namespace ResearchFormalCoreR1
+
+set_option autoImplicit false
+
+open MeasureTheory
+open scoped BigOperators
+
+abbrev DM2Jet := Fin 9 → ℝ
+
+def dm2Radius (j : DM2Jet) : ℝ := 1 + ∑ i, |j i|
+
+noncomputable def dm2HM (r : ℝ) (j : DM2Jet) : Matrix (Fin 2) (Fin 2) ℝ :=
+  !![-r + r^2*j 4/12, -j 1*r/2 + r^2*j 5/12;
+     -j 1*r/2 + r^2*j 5/12, j 0-r*j 2/2+r^2*j 6/8]
+
+noncomputable def dm2HS (r : ℝ) (j : DM2Jet) : Matrix (Fin 2) (Fin 2) ℝ :=
+  !![r + r^2*j 4/12, j 1*r/2 + r^2*j 5/12;
+     j 1*r/2 + r^2*j 5/12, j 0+r*j 2/2+r^2*j 6/8]
+
+/-- The source's negative-definite condition, stated as the quadratic form. -/
+def dm2Negative (H : Matrix (Fin 2) (Fin 2) ℝ) : Prop :=
+  ∀ v : Fin 2 → ℝ, v ≠ 0 → ∑ i, ∑ k, v i * H i k * v k < 0
+
+noncomputable def dm2Weight (r : ℝ) (j : DM2Jet) : ℝ := by
+  classical
+  exact if dm2Negative (dm2HM r j) ∧ (dm2HS r j).det < 0 then
+    |(dm2HM r j).det * (dm2HS r j).det| else 0
+
+private lemma dm2_scale (r x : ℝ) (hr : 0 ≤ r) (hr1 : r ≤ 1) :
+    |r*x| ≤ |x| := by
+  rw [abs_mul, abs_of_nonneg hr]
+  nlinarith [abs_nonneg x]
+
+private lemma dm2_factors (r A B C R : ℝ) (hr : 0 ≤ r) (hr1 : r ≤ 1)
+    (hR : 0 ≤ R) (hA : |A| ≤ R) (hB : |B| ≤ R) (hC : |C| ≤ R) :
+    |A*C-r*B^2| ≤ 2*R^2 := by
+  have hAC : |A*C| ≤ R^2 := by
+    rw [abs_mul, pow_two]
+    exact mul_le_mul hA hC (abs_nonneg _) hR
+  have hBB : B^2 ≤ R^2 := by nlinarith [sq_abs B, abs_nonneg B]
+  have hrBB : |r*B^2| ≤ R^2 := by
+    rw [abs_of_nonneg (mul_nonneg hr (sq_nonneg B))]
+    nlinarith [sq_nonneg B]
+  exact (abs_sub _ _).trans (by linarith)
+
+/-- Exact untyped determinant domination; no jet-coordinate or type assumptions. -/
+theorem dm2_untyped (r : ℝ) (j : DM2Jet) (hr : 0 < r) (hr1 : r ≤ 1) :
+    ((dm2HM r j).det * (dm2HS r j).det)^2 ≤ 16*r^4*dm2Radius j^8 := by
+  let R := dm2Radius j
+  have hR : 0 ≤ R := by dsimp [R, dm2Radius]; positivity
+  have hsum : (∑ i, |j i|) = |j 0|+|j 1|+|j 2|+|j 3|+|j 4|+|j 5|+|j 6|+|j 7|+|j 8| := by
+    simp [Fin.sum_univ_succ]; ring
+  have hbudget : 1+|j 0|+|j 1|+|j 2|+|j 4|+|j 5|+|j 6| ≤ R := by
+    dsimp [R, dm2Radius]; rw [hsum]
+    linarith [abs_nonneg (j 3), abs_nonneg (j 7), abs_nonneg (j 8)]
+  have hscale (i : Fin 9) : r*|j i| ≤ |j i| := by nlinarith [abs_nonneg (j i)]
+  have hscale2 (i : Fin 9) : r^2*|j i| ≤ |j i| := by
+    exact mul_le_of_le_one_left (abs_nonneg _) (by nlinarith)
+  have haM : |-1+r*j 4/12| ≤ R := by
+    calc
+      _ ≤ 1+|j 4| := by
+        have := abs_add_le (-1 : ℝ) (r*j 4/12)
+        rw [abs_div] at this
+        norm_num [abs_of_pos hr] at this
+        linarith [hscale 4, abs_nonneg (j 4)]
+      _ ≤ R := by linarith [abs_nonneg (j 0), abs_nonneg (j 1), abs_nonneg (j 2), abs_nonneg (j 5), abs_nonneg (j 6)]
+  have haS : |1+r*j 4/12| ≤ R := by
+    have := abs_add_le (1 : ℝ) (r*j 4/12)
+    rw [abs_div] at this
+    norm_num [abs_of_pos hr] at this
+    linarith [hscale 4, abs_nonneg (j 0), abs_nonneg (j 1), abs_nonneg (j 2), abs_nonneg (j 4), abs_nonneg (j 5), abs_nonneg (j 6)]
+  have hbM : |-j 1/2+r*j 5/12| ≤ R := by
+    have := abs_add_le (-j 1/2) (r*j 5/12)
+    simp only [abs_div, abs_neg] at this
+    norm_num [abs_of_pos hr] at this
+    linarith [hscale 5, abs_nonneg (j 0), abs_nonneg (j 1), abs_nonneg (j 2), abs_nonneg (j 4), abs_nonneg (j 5), abs_nonneg (j 6)]
+  have hbS : |j 1/2+r*j 5/12| ≤ R := by
+    have := abs_add_le (j 1/2) (r*j 5/12)
+    simp only [abs_div] at this
+    norm_num [abs_of_pos hr] at this
+    linarith [hscale 5, abs_nonneg (j 0), abs_nonneg (j 1), abs_nonneg (j 2), abs_nonneg (j 4), abs_nonneg (j 5), abs_nonneg (j 6)]
+  have hcM : |j 0-r*j 2/2+r^2*j 6/8| ≤ R := by
+    have h1 := abs_sub (j 0) (r*j 2/2)
+    have h2 := abs_add_le (j 0-r*j 2/2) (r^2*j 6/8)
+    simp only [abs_div] at h1 h2
+    norm_num [abs_of_pos hr] at h1 h2
+    linarith [hscale 2, hscale2 6, abs_nonneg (j 1), abs_nonneg (j 2), abs_nonneg (j 4), abs_nonneg (j 5), abs_nonneg (j 6)]
+  have hcS : |j 0+r*j 2/2+r^2*j 6/8| ≤ R := by
+    have h1 := abs_add_le (j 0) (r*j 2/2)
+    have h2 := abs_add_le (j 0+r*j 2/2) (r^2*j 6/8)
+    simp only [abs_div] at h1 h2
+    norm_num [abs_of_pos hr] at h1 h2
+    linarith [hscale 2, hscale2 6, abs_nonneg (j 1), abs_nonneg (j 2), abs_nonneg (j 4), abs_nonneg (j 5), abs_nonneg (j 6)]
+  have hM := dm2_factors r _ _ _ R hr.le hr1 hR haM hbM hcM
+  have hS := dm2_factors r _ _ _ R hr.le hr1 hR haS hbS hcS
+  have hprod : |((-1+r*j 4/12)*(j 0-r*j 2/2+r^2*j 6/8)-r*(-j 1/2+r*j 5/12)^2) *
+      ((1+r*j 4/12)*(j 0+r*j 2/2+r^2*j 6/8)-r*(j 1/2+r*j 5/12)^2)| ≤ (2*R^2)^2 := by
+    rw [abs_mul]
+    calc
+      _ ≤ (2*R^2)*(2*R^2) := mul_le_mul hM hS (abs_nonneg _) (by positivity)
+      _ = (2*R^2)^2 := (pow_two _).symm
+  have hsquare : (((-1+r*j 4/12)*(j 0-r*j 2/2+r^2*j 6/8)-r*(-j 1/2+r*j 5/12)^2) *
+      ((1+r*j 4/12)*(j 0+r*j 2/2+r^2*j 6/8)-r*(j 1/2+r*j 5/12)^2))^2 ≤ ((2*R^2)^2)^2 := by
+    simpa only [sq_abs] using
+      (sq_le_sq₀ (abs_nonneg _) (sq_nonneg (2*R^2))).2 hprod
+  have hid : ((dm2HM r j).det*(dm2HS r j).det)^2 = r^4 *
+      (((-1+r*j 4/12)*(j 0-r*j 2/2+r^2*j 6/8)-r*(-j 1/2+r*j 5/12)^2) *
+      ((1+r*j 4/12)*(j 0+r*j 2/2+r^2*j 6/8)-r*(j 1/2+r*j 5/12)^2))^2 := by
+    simp [dm2HM, dm2HS, Matrix.det_fin_two]; ring
+  rw [hid]
+  calc
+    _ ≤ r^4*((2*R^2)^2)^2 := mul_le_mul_of_nonneg_left hsquare (by positivity)
+    _ = 16*r^4*dm2Radius j^8 := by dsimp [R]; ring
+
+/-- P02-LM-002 section 2, with the literal quadratic-form type indicator. -/
+theorem dm2_pointwise (r : ℝ) (j : DM2Jet) (hr : 0 < r) (hr1 : r ≤ 1) :
+    dm2Weight r j ^ 2 ≤ 16*r^4*dm2Radius j^8 := by
+  classical
+  unfold dm2Weight
+  split_ifs
+  · simpa only [sq_abs] using dm2_untyped r j hr hr1
+  · simpa only [zero_pow (by decide : (2 : ℕ) ≠ 0)] using
+      (show 0 ≤ 16*r^4*dm2Radius j^8 by positivity)
+
+/-- Two-dimensional Sylvester criterion for the literal quadratic-form definition. -/
+theorem dm2_negative_iff (a b c : ℝ) :
+    dm2Negative !![a,b;b,c] ↔ a < 0 ∧ 0 < a*c-b^2 := by
+  constructor
+  · intro h
+    have ha := h ![1,0] (by simp)
+    simp [Fin.sum_univ_two] at ha
+    have hv : (![(-b),a] : Fin 2 → ℝ) ≠ 0 := by
+      intro heq
+      have := congrFun heq 1
+      simp at this
+      linarith
+    have hd := h ![-b,a] hv
+    simp [Fin.sum_univ_two] at hd
+    refine ⟨ha, ?_⟩
+    by_contra hn
+    have hh : 0 ≤ a*(a*c-b^2) := mul_nonneg_of_nonpos_of_nonpos ha.le (le_of_not_gt hn)
+    nlinarith
+  · rintro ⟨ha,hd⟩ v hv
+    have hvxy : v 0 ≠ 0 ∨ v 1 ≠ 0 := by
+      by_contra hn
+      push Not at hn
+      apply hv
+      ext i
+      fin_cases i <;> simp_all
+    have hq : 0 < (a*v 0+b*v 1)^2+(a*c-b^2)*(v 1)^2 := by
+      rcases eq_or_ne (v 1) 0 with hy|hy
+      · have hx : v 0 ≠ 0 := hvxy.resolve_right (not_ne_iff.mpr hy)
+        simpa [hy] using sq_pos_of_ne_zero (mul_ne_zero ha.ne hx)
+      · exact add_pos_of_nonneg_of_pos (sq_nonneg _) (mul_pos hd (sq_pos_of_ne_zero hy))
+    simp [Fin.sum_univ_two]
+    nlinarith
+
+/-- Measurability of the exact typed weight, with no assumed type-null boundary. -/
+theorem dm2_weight_measurable (r : ℝ) : Measurable (dm2Weight r) := by
+  classical
+  have hm : Continuous (fun j : DM2Jet => (dm2HM r j).det) := by
+    simp only [dm2HM, Matrix.det_fin_two]
+    fun_prop
+  have hs : Continuous (fun j : DM2Jet => (dm2HS r j).det) := by
+    simp only [dm2HS, Matrix.det_fin_two]
+    fun_prop
+  have htype : MeasurableSet {j : DM2Jet | dm2Negative (dm2HM r j) ∧ (dm2HS r j).det < 0} := by
+    simp only [dm2HM, dm2_negative_iff]
+    apply MeasurableSet.inter
+    · apply MeasurableSet.inter
+      · have h : Continuous (fun j : DM2Jet => -r+r^2*j 4/12) := by fun_prop
+        exact (isOpen_lt h continuous_const).measurableSet
+      · have h : Continuous (fun j : DM2Jet => (-r+r^2*j 4/12)*(j 0-r*j 2/2+r^2*j 6/8)-(-j 1*r/2+r^2*j 5/12)^2) := by fun_prop
+        exact (isOpen_lt continuous_const h).measurableSet
+    · exact (isOpen_lt hs continuous_const).measurableSet
+  change Measurable (fun j : DM2Jet => if dm2Negative (dm2HM r j) ∧ (dm2HS r j).det < 0 then |(dm2HM r j).det*(dm2HS r j).det| else 0)
+  exact Measurable.ite htype (hm.measurable.mul hs.measurable).abs measurable_const
+
+/-- P02-LM-002's expectation step: eighth-moment control supplies integrability
+and the second moment, rather than presupposing that second moment. -/
+theorem dm2_moment {Ω : Type*} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
+    (J : Ω → DM2Jet) (hJ : Measurable J) (r M8 : ℝ) (hr : 0 < r) (hr1 : r ≤ 1)
+    (h8 : MeasureTheory.Integrable (fun x => dm2Radius (J x)^8) μ)
+    (hM8 : (∫ x, dm2Radius (J x)^8 ∂μ) ≤ M8) :
+    MeasureTheory.Integrable (fun x => dm2Weight r (J x)^2) μ ∧
+      (∫ x, dm2Weight r (J x)^2 ∂μ) ≤ 16*M8*r^4 := by
+  have hmajor : MeasureTheory.Integrable (fun x => 16*r^4*dm2Radius (J x)^8) μ :=
+    h8.const_mul _
+  have hmeas : MeasureTheory.AEStronglyMeasurable (fun x => dm2Weight r (J x)^2) μ :=
+    (((dm2_weight_measurable r).comp hJ).pow_const 2).aestronglyMeasurable
+  have hi : MeasureTheory.Integrable (fun x => dm2Weight r (J x)^2) μ :=
+    hmajor.mono' hmeas (Filter.Eventually.of_forall (fun x => by
+      rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
+      exact dm2_pointwise r (J x) hr hr1))
+  refine ⟨hi, ?_⟩
+  calc
+    _ ≤ ∫ x, 16*r^4*dm2Radius (J x)^8 ∂μ :=
+      MeasureTheory.integral_mono hi hmajor (fun x => dm2_pointwise r (J x) hr hr1)
+    _ = 16*r^4*(∫ x, dm2Radius (J x)^8 ∂μ) := MeasureTheory.integral_const_mul _ _
+    _ ≤ 16*r^4*M8 := mul_le_mul_of_nonneg_left hM8 (by positivity)
+    _ = 16*M8*r^4 := by ring
+
+end ResearchFormalCoreR1
+
+
diff --git a/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/ProbabilityCompanionsV2.lean b/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/ProbabilityCompanionsV2.lean
new file mode 100644
index 000000000..e4073dc21
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/ProbabilityCompanionsV2.lean
@@ -0,0 +1,93 @@
+import Mathlib.Analysis.Real.Sqrt
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Ring
+import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Linarith
+
+namespace ResearchFormalCoreR1
+
+set_option autoImplicit false
+
+/-- P02-LM-008 algebraic companion: exact cancellation of the `r²` factor
+    after the Cauchy–Schwarz numerator bound and the normalizer lower bound
+    have been established in the surrounding probability theorem. -/
+theorem p02_lm008_r2_cancel
+    (r cW cZ q : ℝ) (hr : r ≠ 0) (hcZ : cZ ≠ 0) :
+    (Real.sqrt cW * r ^ 2 * Real.sqrt q) / (cZ * r ^ 2) =
+      (Real.sqrt cW / cZ) * Real.sqrt q := by
+  field_simp [hr, hcZ]
+
+/-- P02-LM-008 cross-multiplied transfer companion.  This theorem starts
+    from an already supplied Cauchy–Schwarz numerator estimate and an exact
+    normalizer lower bound.  It does not formalize the measure-theoretic
+    Cauchy–Schwarz step itself. -/
+theorem p02_lm008_cross_multiplied
+    (n z r cW cZ q : ℝ)
+    (hr : 0 < r) (hcW : 0 ≤ cW) (hcZ : 0 < cZ) (hq : 0 ≤ q)
+    (hz : cZ * r ^ 2 ≤ z)
+    (hn : n ≤ Real.sqrt cW * r ^ 2 * Real.sqrt q) :
+    n * (cZ * r ^ 2) ≤
+      (Real.sqrt cW * r ^ 2 * Real.sqrt q) * z := by
+  have hden : 0 ≤ cZ * r ^ 2 :=
+    mul_nonneg (le_of_lt hcZ) (sq_nonneg r)
+  have hnum : 0 ≤ Real.sqrt cW * r ^ 2 * Real.sqrt q := by
+    positivity
+  calc
+    n * (cZ * r ^ 2) ≤
+        (Real.sqrt cW * r ^ 2 * Real.sqrt q) * (cZ * r ^ 2) := by
+      exact mul_le_mul_of_nonneg_right hn hden
+    _ ≤ (Real.sqrt cW * r ^ 2 * Real.sqrt q) * z := by
+      exact mul_le_mul_of_nonneg_left hz hnum
+
+/-- P02-LM-008 quotient companion.  With positive denominators, the
+    cross-multiplied inequality and exact `r²` cancellation yield the Palm
+    square-root transfer coefficient. -/
+theorem p02_lm008_quotient_bound
+    (n z r cW cZ q : ℝ)
+    (hr : 0 < r) (hcW : 0 ≤ cW) (hcZ : 0 < cZ) (hq : 0 ≤ q)
+    (hzpos : 0 < z) (hz : cZ * r ^ 2 ≤ z)
+    (hn : n ≤ Real.sqrt cW * r ^ 2 * Real.sqrt q) :
+    n / z ≤ (Real.sqrt cW / cZ) * Real.sqrt q := by
+  have hscaled : 0 < cZ * r ^ 2 :=
+    mul_pos hcZ (sq_pos_of_pos hr)
+  have hcross :=
+    p02_lm008_cross_multiplied n z r cW cZ q hr hcW hcZ hq hz hn
+  rw [← p02_lm008_r2_cancel r cW cZ q (ne_of_gt hr) (ne_of_gt hcZ)]
+  exact (div_le_div_iff₀ hzpos hscaled).2 hcross
+
+/-- P02-LM-009 deterministic threshold companion.  Failure of
+    `r * R^5 ≤ ε` implies the fifth-power threshold used before Markov's
+    inequality. -/
+theorem p02_lm009_bad_event_threshold
+    (r R ε : ℝ) (hr : 0 < r) (hbad : ε < r * R ^ 5) :
+    ε / r < R ^ 5 := by
+  exact (div_lt_iff₀ hr).2 (by simpa [mul_comm] using hbad)
+
+/-- The fixed exponent identity used when the 40th moment is selected in
+    the P02-LM-009 application. -/
+theorem p02_lm009_power40_identity (R : ℝ) :
+    (R ^ 5) ^ 8 = R ^ 40 := by
+  ring
+
+/-- In the final P0.2 power ledger, an `O(r^4)` Palm tail is also `O(r^3)`
+    on `0 ≤ r ≤ 1`. -/
+theorem p02_lm009_r4_le_r3
+    (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) :
+    r ^ 4 ≤ r ^ 3 := by
+  have h : 0 ≤ r ^ 3 * (1 - r) :=
+    mul_nonneg (pow_nonneg hr0 3) (sub_nonneg.mpr hr1)
+  nlinarith
+
+/-- Conditional rate companion: once the Palm square-root transfer has
+    produced a uniform `C r^4` bound, the cubic target follows on `r ≤ 1`. -/
+theorem p02_lm009_palm_r4_to_r3
+    (p C r : ℝ) (hC : 0 ≤ C) (hr0 : 0 ≤ r) (hr1 : r ≤ 1)
+    (hp : p ≤ C * r ^ 4) :
+    p ≤ C * r ^ 3 := by
+  calc
+    p ≤ C * r ^ 4 := hp
+    _ ≤ C * r ^ 3 := by
+      exact mul_le_mul_of_nonneg_left (p02_lm009_r4_le_r3 r hr0 hr1) hC
+
+end ResearchFormalCoreR1
diff --git a/frontiers/determinant_moment_20261025/SCOPE.md b/frontiers/determinant_moment_20261025/SCOPE.md
new file mode 100644
index 000000000..0a3e15e04
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/SCOPE.md
@@ -0,0 +1,35 @@
+# Exact DM2 formal scope
+
+Author OpenAI/Codex /root; source-alignment PENDING_INDEPENDENT_REVIEW.
+The complete preimplementation source binding is SOURCE_MAP.md and remains bound.
+
+| Declaration | Source mapping and hypotheses |
+|---|---|
+| dm2_untyped | Section 3: both exact determinant factors; arbitrary nine real jets; 0<r<=1. Proves the stronger bound before type restriction. |
+| dm2_pointwise | Section 2's exact W²<=16r⁴R⁸; no extra type or probability assumptions. |
+| dm2_negative_iff | Auxiliary two-dimensional Sylvester criterion, proved for every symmetric real 2x2 matrix, connecting the literal quadratic-form indicator with measurable polynomial inequalities. |
+| dm2_weight_measurable | Measurability of the actual indicator-weight product for every real r, with no null-boundary premise. |
+| dm2_moment | Sections 2–3: measurable nine-jet map, integrable eighth radius power, integral<=M8, 0<r<=1 yield squared-weight integrability and integral<=16M8r⁴. The arbitrary-measure statement strengthens the source probability-law implication without adding a premise. |
+
+All definitions, matrix entries, signs and coordinate ordering are in the Lean
+source and SOURCE_MAP.md. The retained 13 scalar baseline declarations preserve their statement/proof bodies from formal/ at c4eabc1a; COMPATIBILITY.md documents their historical repairs.
+Their imported historical review is not transferred to the changed package.
+
+The new theorem does not prove a concrete Gaussian moment, jet identification,
+normalizer floor, actual Palm construction, full event tail, GT5, P0.2, lifetime
+or persistence theorem. Scientific effect NONE; no register changes.
+
+The unchanged retained gate builds all 18 registered targets, runs leanchecker,
+audits transitive axioms against propext/Classical.choice/Quot.sound, and executes
+its original five rejection controls. controls/ adds two explicit false DM2
+mutations: r^6 instead of r^4 and omission of q from R. Those separate executions
+are recorded independently. The gate retains its exact provider-distinct alignment
+validator; a same-provider technical source review earns zero organizational
+independence and does not supply a machine ACCEPTED alignment record.
+
+## 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.
diff --git a/frontiers/determinant_moment_20261025/SOURCE_MAP.md b/frontiers/determinant_moment_20261025/SOURCE_MAP.md
new file mode 100644
index 000000000..bf8e1746e
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/SOURCE_MAP.md
@@ -0,0 +1,65 @@
+# DM2 exact source binding and implementation plan
+
+Author: OpenAI/Codex /root, 2026-10-25. Author-side; alignment pending.
+
+Source repository d6g8k5htny-coder/Math-, commit c4eabc1a917ba2c1b96fe4af425cf2a484877c03,
+path imports/hardening_ebedb780/P02-LM-002/proof.md.export.txt,
+Git blob d1fd7eccd5947cb6c5bf8724a77b7ec1c380a29b,
+SHA256 0f8f80922feb603e5b6e530eb885a7819b3a98d90d3c42d60a68259af766f7de.
+This is the preserved closure capsule's complete statement/proof, sections 2–3;
+its claimed historical reviews are source claims, not reviews of this Lean work.
+The uninspected primary GP-DER-071 and CL-AUD-052 are not represented as inspected.
+
+Before proof implementation, freeze the following mathematical contract.
+A jet is nine real coordinates q,a,w,z,c40,c31,c22,c13,c04, in that order.
+R is exactly 1 plus their nine absolute values; unused z,c13,c04 remain included.
+HM and HS are symmetric two-by-two real matrices with the exact entries of section 2:
+HM=(-r+r²c40/12, -ar/2+r²c31/12; same, q-rw/2+r²c22/8),
+HS=( r+r²c40/12,  ar/2+r²c31/12; same, q+rw/2+r²c22/8).
+Negative definite means the quadratic form is strictly negative at every nonzero
+real two-vector. W=|det HM * det HS| on the conjunction of HM negative definite
+and det HS<0, and zero elsewhere. No typing, nonsingularity, Gaussianity or
+independence premise is permitted in the pointwise theorem.
+
+Target `dm2_pointwise`: for every real r and jet j, 0<r and r<=1 imply
+W(r,j)^2 <=16*r^4*R(j)^8. Prove stronger untyped bound first, then indicator restriction.
+Target `dm2_moment`: on any probability space with measurable jet J, an integrable
+R(J)^8 with integral<=M8 implies integrability of W(r,J)^2 and its integral
+<=16*M8*r^4 for 0<r<=1. M8 is a bound, not an assumed target conclusion.
+The theorem at each r yields the source's uniform family corollary by instantiation.
+
+Parent dependency: formal/MOMENT_TAIL.md and MeasureBridge require an actual
+second-moment estimate cW*r^4; this result supplies cW=16*M8 for the exact normalized
+jet convention. Remaining: identify the actual endpoint field jets with this
+convention; prove the concrete uniform eighth moment and normalizer floor;
+construct/identify the same typed Palm law; prove the event tail and good-event
+coverage. P0.2, GT5, exact capture, lifetime and persistence conclusions stay open.
+
+Plan: (1) independent packet using unchanged gate.py, pins, scalar baseline and
+five rejection controls; no edits to occupied core formal paths. (2) prove exact
+factorization, coefficient domination, pointwise and integral results. Check with
+pinned Lean v4.34.1/mathlib d13f23b723b8a846827a245b89c10fc7d3f11612.
+(3) run source checks, gate tests, fresh build, leanchecker, transitive axiom audit,
+and all rejection controls; retain failed executions. (4) freeze exact source
+identities, publish draft PR, request actual nonauthor source/statement review.
+Report real lineage; author replay never supplies independent alignment.
+(5) supply website mapping as candidate evidence, no graph or status promotion.
+
+## Import-only successor after observed memory failure
+
+At proof commit deb28a751f620715ec65d3bd73690905e6fee94d the ordinary fresh build
+passed, but leanchecker exited 137; cgroup memory.max was 17179869184 bytes and
+memory.events recorded one OOM kill. The failed original build/checker/version logs
+remain under evidence/history/umbrella-mathlib-oom/. No successful receipt exists
+for that commit. The compiler proof bodies and theorem types are unchanged.
+
+The successor replaces only each of the three modules' `import Mathlib` headers
+with exact narrow Mathlib imports. The two copied successor-preservation tests
+now require those exact import lists and continue comparing the entire remaining
+baseline bodies with the preserved originals plus their documented historical
+compiler repairs. Their test-first run failed exactly those two tests before the
+import change. Original source bytes remain in formal/ at the base and in the
+preserved originals. Gate.py, pins, allowlist and all five rejection controls are
+unchanged. This is a new dependency/source candidate, requiring its own execution
+and review; neither the previous source review nor successful compilation is
+silently rebound to it.
diff --git a/frontiers/determinant_moment_20261025/WEBSITE_HANDOFF.json b/frontiers/determinant_moment_20261025/WEBSITE_HANDOFF.json
new file mode 100644
index 000000000..607dac1ed
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/WEBSITE_HANDOFF.json
@@ -0,0 +1,131 @@
+{
+  "purpose": "SOURCE_PINNED_WEBSITE_HANDOFF_NOT_A_GRAPH_BINDING",
+  "schema_version": 1,
+  "node_join": "UNBOUND_ARTIFACT_NO_NODE_ID_INVENTED",
+  "existing_model_reference": {
+    "repository": "d6g8k5htny-coder/main",
+    "commit": "3be7a859d4ff05ceaf8b2c8ec748cfd2658c67f5",
+    "path": "docs/plans/2026-10-08-artifact-index-contract.md"
+  },
+  "proof_checked_commit": "dcfc89366f590342b4cd30b141a22c9ae2a562bb",
+  "public_delivery_commit": "144f371fd5a7990f4d53db01ad8f76dbeba45b4a",
+  "scientific_effect": "NONE",
+  "source_alignment": "SAME_PROVIDER_NONAUTHOR_TECHNICAL_REVIEW_ONLY",
+  "machine_alignment": "PENDING_INDEPENDENT_REVIEW",
+  "organizational_independence_credit": 0,
+  "execution": "LOCAL_KERNEL_RECHECK_AXIOM_AUDIT_AND_NEGATIVE_CONTROLS_PASS_NOT_HOSTED",
+  "coverage": [
+    "Exact normalized nine-jet endpoint-Hessian pointwise W^2 <= 16 r^4 R^8, 0 < r <= 1",
+    "Measurable-jet eighth-moment premise gives squared-weight integrability and integral <=16 M8 r^4",
+    "Auxiliary untyped determinant bound, negative-definiteness criterion and weight measurability"
+  ],
+  "not_established": [
+    "concrete Gaussian eighth-moment bound",
+    "actual field/jet convention identification",
+    "positive normalizer lower bound",
+    "actual Palm-law identification",
+    "full event tail and good-event coverage",
+    "GT5, P0.2, lifetime and persistence parents"
+  ],
+  "artifacts": [
+    {
+      "kind": "file",
+      "repository": "d6g8k5htny-coder/Math-",
+      "artifact_path": "imports/hardening_ebedb780/P02-LM-002/proof.md.export.txt",
+      "commit": "c4eabc1a917ba2c1b96fe4af425cf2a484877c03",
+      "blob_sha": "d1fd7eccd5947cb6c5bf8724a77b7ec1c380a29b",
+      "sha256": "0f8f80922feb603e5b6e530eb885a7819b3a98d90d3c42d60a68259af766f7de",
+      "roles": [
+        "source"
+      ]
+    },
+    {
+      "kind": "file",
+      "repository": "d6g8k5htny-coder/Math-",
+      "artifact_path": "frontiers/determinant_moment_20261025/SOURCE_MAP.md",
+      "commit": "dcfc89366f590342b4cd30b141a22c9ae2a562bb",
+      "blob_sha": "bf8e1746ec5026a57e755c0bb5b74968189aa1a4",
+      "sha256": "32b5e48e9d8150927542718e719a71f6d59ef7593b78dd827dd52c18c47681f6",
+      "roles": [
+        "source"
+      ]
+    },
+    {
+      "kind": "file",
+      "repository": "d6g8k5htny-coder/Math-",
+      "artifact_path": "frontiers/determinant_moment_20261025/SCOPE.md",
+      "commit": "dcfc89366f590342b4cd30b141a22c9ae2a562bb",
+      "blob_sha": "0a3e15e045618369730e8aa9c3f967ef2929e59b",
+      "sha256": "c3cb56539a6b1dcb41c6ac378c1797e95ef878ba03276456276e0bb3abfa3ddd",
+      "roles": [
+        "source"
+      ]
+    },
+    {
+      "kind": "file",
+      "repository": "d6g8k5htny-coder/Math-",
+      "artifact_path": "frontiers/determinant_moment_20261025/ResearchFormalCoreR1/DeterminantMoment.lean",
+      "commit": "dcfc89366f590342b4cd30b141a22c9ae2a562bb",
+      "blob_sha": "93e296ca101be5d15a5ed6bfef7c6fe768f514e6",
+      "sha256": "661b73c3f21c6d2529f5e09ce426d89c01939ab27a5cc868db3802c7e66ea82d",
+      "roles": [
+        "kernel"
+      ]
+    },
+    {
+      "kind": "file",
+      "repository": "d6g8k5htny-coder/Math-",
+      "artifact_path": "frontiers/determinant_moment_20261025/manifest.json",
+      "commit": "dcfc89366f590342b4cd30b141a22c9ae2a562bb",
+      "blob_sha": "71a692415138cbd1950a793402fa30d3bf166ef8",
+      "sha256": "cb2b4870debf98cdf3663663797ccfc524e23d5f41f89e1c9ecdba5b6e680811",
+      "roles": [
+        "kernel"
+      ]
+    },
+    {
+      "kind": "file",
+      "repository": "d6g8k5htny-coder/Math-",
+      "artifact_path": "frontiers/determinant_moment_20261025/evidence/final/receipt.json",
+      "commit": "144f371fd5a7990f4d53db01ad8f76dbeba45b4a",
+      "blob_sha": "a2d175bbdc62940e9c1fe522808444e3f57661d7",
+      "sha256": "8fe7ab0f131a8a5c3e459d3bbbd10b4ab2b135438793851c11b25f7bb69f9eeb",
+      "roles": [
+        "kernel"
+      ]
+    },
+    {
+      "kind": "file",
+      "repository": "d6g8k5htny-coder/Math-",
+      "artifact_path": "frontiers/determinant_moment_20261025/evidence/final/EXPORT_IDENTITIES.json",
+      "commit": "144f371fd5a7990f4d53db01ad8f76dbeba45b4a",
+      "blob_sha": "d4499c4303a1e540756a939cb7bb9596ab8afb86",
+      "sha256": "b6e06898b34d526848c4b1ab480a5effced42ea0c1bca761eb2ee5e20a2b5577",
+      "roles": [
+        "kernel"
+      ]
+    },
+    {
+      "kind": "file",
+      "repository": "d6g8k5htny-coder/Math-",
+      "artifact_path": "frontiers/determinant_moment_20261025/evidence/DM2_IMPORT_SUCCESSOR_REVIEW.md",
+      "commit": "144f371fd5a7990f4d53db01ad8f76dbeba45b4a",
+      "blob_sha": "ef8d1426522175b4888823c1d8eca69fd6c7f955",
+      "sha256": "061dd239951933729266c5ee7e71bfd5e216a898191b789159fac22b0cdb5543",
+      "roles": [
+        "review"
+      ]
+    },
+    {
+      "kind": "file",
+      "repository": "d6g8k5htny-coder/Math-",
+      "artifact_path": "frontiers/determinant_moment_20261025/evidence/DELIVERY.md",
+      "commit": "144f371fd5a7990f4d53db01ad8f76dbeba45b4a",
+      "blob_sha": "f6d07999fedd34f9d47d88811f8046e9e797b7c4",
+      "sha256": "5f20ab6ce305fcd444ac04241516ac2537bfc26212dea4f341665db11bfb0182",
+      "roles": [
+        "source"
+      ]
+    }
+  ]
+}
diff --git a/frontiers/determinant_moment_20261025/WEBSITE_HANDOFF.md b/frontiers/determinant_moment_20261025/WEBSITE_HANDOFF.md
new file mode 100644
index 000000000..4695e8e95
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/WEBSITE_HANDOFF.md
@@ -0,0 +1,21 @@
+# Website engineer handoff
+
+WEBSITE_HANDOFF.json gives full commit/blob/SHA256 pins using the existing
+file-reference fields and allowed source/kernel/review roles. It is an artifact
+inventory, not a schema-v2 graph binding: no existing graph node was established
+for this exact new proof, so node_id and artifact_id are not invented. Keep it
+unbound until a separately reviewed node mapping exists. No GRAPH, Artifact Index,
+scientific register or deployed website is changed by this handoff.
+
+Display the result as the exact normalized-jet **conditional determinant second
+moment**, with its explicit 0<r<=1 and eighth-moment hypotheses. Source capsule
+sections 2–3 are the mathematical source; the Lean file is its new implementation.
+The kernel axis has a successful local build/recheck/axiom/negative-control receipt
+at dcfc89366f590342b4cd30b141a22c9ae2a562bb. Hosted execution is not established
+for this packet. The review axis has a source-exposed same-provider nonauthor
+technical review; machine alignment remains pending, independence credit zero.
+Neither axis establishes the concrete Gaussian moment premise or parent theorem.
+
+The formal packet's source manifest is frozen at the checked commit. Later output
+and mapping commits add evidence without rebinding its receipt. Every artifact
+in this handoff names an already existing immutable source/delivery commit.
diff --git a/frontiers/determinant_moment_20261025/blueprint/src/content.tex b/frontiers/determinant_moment_20261025/blueprint/src/content.tex
new file mode 100644
index 000000000..9f25b5571
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/blueprint/src/content.tex
@@ -0,0 +1,5 @@
+\lean{ResearchFormalCoreR1.dm2_untyped}
+\lean{ResearchFormalCoreR1.dm2_pointwise}
+\lean{ResearchFormalCoreR1.dm2_negative_iff}
+\lean{ResearchFormalCoreR1.dm2_weight_measurable}
+\lean{ResearchFormalCoreR1.dm2_moment}
diff --git a/frontiers/determinant_moment_20261025/controls/false_omit_q.lean.txt b/frontiers/determinant_moment_20261025/controls/false_omit_q.lean.txt
new file mode 100644
index 000000000..3b1e86908
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/controls/false_omit_q.lean.txt
@@ -0,0 +1,6 @@
+import ResearchFormalCoreR1
+open ResearchFormalCoreR1
+-- Deliberately false: q removed from the radius.
+example : let j : DM2Jet := ![(-100),0,0,0,0,0,0,0,0]
+    ((dm2HM (1/2) j).det*(dm2HS (1/2) j).det)^2 ≤ 16*((1/2) : ℝ)^4*1^8 := by
+  norm_num [dm2HM, dm2HS, dm2Radius, Matrix.det_fin_two, Fin.sum_univ_succ]
diff --git a/frontiers/determinant_moment_20261025/controls/false_r6.lean.txt b/frontiers/determinant_moment_20261025/controls/false_r6.lean.txt
new file mode 100644
index 000000000..3a4090ef1
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/controls/false_r6.lean.txt
@@ -0,0 +1,6 @@
+import ResearchFormalCoreR1
+open ResearchFormalCoreR1
+-- Deliberately false: r^4 replaced by r^6.
+example : let j : DM2Jet := ![(-1),0,0,0,0,0,0,0,0]
+    ((dm2HM (1/128) j).det*(dm2HS (1/128) j).det)^2 ≤ 16*((1/128) : ℝ)^6*dm2Radius j^8 := by
+  norm_num [dm2HM, dm2HS, dm2Radius, Matrix.det_fin_two, Fin.sum_univ_succ]
diff --git a/frontiers/determinant_moment_20261025/evidence/DELIVERY.md b/frontiers/determinant_moment_20261025/evidence/DELIVERY.md
new file mode 100644
index 000000000..f6d07999f
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/DELIVERY.md
@@ -0,0 +1,102 @@
+# DM2 execution delivery
+
+Delegated AI implementation for Dylan Roy: OpenAI/Codex `/root`.
+Scientific effect NONE. No parent acceptance or status change.
+
+## Result
+
+The exact P02-LM-002 pointwise inequality and its eighth-moment integration
+corollary are supplied and locally kernel-checked, together with a stronger
+untyped determinant inequality, the quadratic-form Sylvester criterion and
+measurability of the literal typed weight. SOURCE_MAP.md and SCOPE.md bind the
+mathematics. No conclusion or type assumption was inserted as a premise.
+
+## Exact executed source
+
+- Checked commit: dcfc89366f590342b4cd30b141a22c9ae2a562bb.
+- Proof manifest SHA256: cb2b4870debf98cdf3663663797ccfc524e23d5f41f89e1c9ecdba5b6e680811.
+- DM2 module SHA256: 661b73c3f21c6d2529f5e09ce426d89c01939ab27a5cc868db3802c7e66ea82d.
+- Original receipt SHA256: 8fe7ab0f131a8a5c3e459d3bbbd10b4ab2b135438793851c11b25f7bb69f9eeb.
+- Lean v4.34.1, release commit 5045d0056413266e57c625dcd7c365b10e377c52.
+- Mathlib d13f23b723b8a846827a245b89c10fc7d3f11612; all nine locked dependency HEADs
+  and clean worktrees observed before and after execution.
+
+The exact local command was `PATH=/home/agent/.elan/bin:$PATH python -B -S
+frontiers/determinant_moment_20261025/gate.py --execute` from the repository root.
+The gate sets every child cwd to the packet root. Parent exit was 0. It removed
+the package build directory and ran a fresh `lake build`, then
+`lake env leanchecker ResearchFormalCoreR1`, the generated axiom/type queries,
+five controls and final runtime/source/dependency observations. All succeeded
+under their declared expected outcomes. leanchecker's successful stdout is empty;
+its process exit 0 and sequence are recorded in gate-terminal.log.
+
+All 18 declarations (13 retained scalar companions plus five new declarations)
+have transitive axiom sets limited to propext, Classical.choice and Quot.sound.
+The five retained controls rejected two false arithmetic proofs via Lean, and
+sorry, imported-custom-axiom and native_decide proofs via their actual transitive
+axiom reports. Their successful elaboration does not mean gate acceptance.
+
+The unchanged gate's 78 tests passed in normal and optimized Python modes on the
+frozen proof/control source. Test logs are included. The nonauthor independently
+ran the same two 78-test modes and reported the results in its own review.
+
+Two additional real Lean false-goal controls were run after the full gate:
+
+- false_r6: r=1/128, q=-1, all other jets zero. Untyped squared product=2^-28,
+  proposed r^6 bound=2^-30. Lean exit1, `unsolved goals`, goal False.
+- false_omit_q: r=1/2, q=-100, all others zero. Squared product=6250000,
+  bound omitting q from R=1. Lean exit1, `unsolved goals`, goal False.
+
+Their fixtures are in controls/*.lean.txt. Replay by copying each fixture to
+`.lake/formal-evidence/dm2_<label>.lean` and running `lake env lean` on that path
+from the packet directory; each must exit1 on the false goal. Their commands,
+exit codes, elapsed times, source/log hashes are in final/dm2_extra_controls.json.
+Both witnesses also satisfy the actual type indicators, as the nonauthor checked.
+
+## Evidence custody and limits
+
+final/receipt.json is an exact copy of the original gate output, without any
+metadata edited. Its 11 original log hashes were verified before copying, and
+final/EXPORT_IDENTITIES.json gives every exported byte count/hash. Generated
+Audit/Types/control Lean queries are preserved with `.lean.txt` suffixes to keep
+output artifacts out of the package module census. No source content is changed
+by that filename projection. Supplemental DM2 logs are outside the original
+receipt's 11-log map and are bound by their own control record and export index.
+Later delivery-only commits do not change or rebind the checked commit.
+
+This was a direct local managed-cloud execution. repository/workflow/run fields
+are honestly null; it is not a trusted hosted workflow receipt. Existing generic
+repository CI runs the original core package, not this standalone packet. No new
+workflow was introduced and no hosted target-package success is claimed.
+
+The earlier umbrella-Mathlib build at deb28a751f620715ec65d3bd73690905e6fee94d
+passed, but leanchecker was OOM-killed at a 16GiB limit. Its failure remains in
+history/umbrella-mathlib-oom/. Only import headers changed in the successor;
+every theorem, hypothesis, definition and proof body is unchanged. Gate, pins,
+allowlist and five controls stayed identical. Preservation tests compare the
+complete baseline bodies with originals and exact replacement imports. The RED
+run used the precursor deprecated Data.Real headers; final canonical headers
+were selected from the compiler's explicit replacement guidance. This is not
+represented as a RED replay of the final literal header strings.
+
+## Actual review and remaining boundary
+
+DM2_NONAUTHOR_REVIEW.md covers deb28a; DM2_IMPORT_SUCCESSOR_REVIEW.md is the fresh
+review of dcfc8936. Actual reviewer OpenAI/GPT-6-Codex family,
+`/root/dm2_statement_review`, separate context, source exposed, no production
+source authorship. Exact underlying model identifier unavailable to reviewer.
+Organizational/blind/human independence 0. No historical primary Drive proof or
+review was inspected or transferred. The source export's historical acceptance
+labels are provenance only.
+
+Same-provider technical statement review exists; a provider-distinct full-target
+alignment record does not. The unchanged validator remains fail-closed and its
+receipt remains PENDING_INDEPENDENT_REVIEW. Public request is on draft Math-#511
+and main#539/6402508582; no eligible provider-distinct pickup is presumed.
+No fake reviewer JSON is supplied. No merge, Ready transition or scientific
+promotion is attempted.
+
+This supplies the exact normalized-jet second-moment interface cW=16*M8. Still
+unproved here: concrete field/jet identification, uniform Gaussian eighth
+moments, normalizer lower bound, actual same-law Palm identification, event-tail
+and good-event coverage, GT5, P0.2, and parent lifetime/persistence conclusions.
diff --git a/frontiers/determinant_moment_20261025/evidence/DM2_IMPORT_SUCCESSOR_REVIEW.md b/frontiers/determinant_moment_20261025/evidence/DM2_IMPORT_SUCCESSOR_REVIEW.md
new file mode 100644
index 000000000..ef8d14265
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/DM2_IMPORT_SUCCESSOR_REVIEW.md
@@ -0,0 +1,104 @@
+# DM2 import successor: nonauthor technical review
+
+Signed 2026-10-25: OpenAI / GPT-6-Codex family / agent
+`/root/dm2_statement_review`; exact underlying model identifier unavailable.
+Author: OpenAI/Codex `/root`. Separate reviewer context, same provider,
+original proof visible. Organizational-independence credit 0; acceptance credit
+0; scientific effect NONE. This is not provider-distinct machine alignment.
+
+## Frozen source
+
+Reviewed repository `d6g8k5htny-coder/Math-`, commit
+`dcfc89366f590342b4cd30b141a22c9ae2a562bb`. Paths below are relative to
+`frontiers/determinant_moment_20261025/`.
+
+| File | SHA256 |
+|---|---|
+| manifest.json | cb2b4870debf98cdf3663663797ccfc524e23d5f41f89e1c9ecdba5b6e680811 |
+| ResearchFormalCoreR1/DeterminantMoment.lean | 661b73c3f21c6d2529f5e09ce426d89c01939ab27a5cc868db3802c7e66ea82d |
+| ResearchFormalCoreR1/AlgebraV2.lean | 71e4327df9f7d6979f1467f7e0d880e0ab0a70ab6d234802d8c7a1624b9ce2d9 |
+| ResearchFormalCoreR1/ProbabilityCompanionsV2.lean | dbc42b17797be688fecec790f32fcfd0004d98ac776cbbe0471c62c3f506aa41 |
+| SOURCE_MAP.md | 32b5e48e9d8150927542718e719a71f6d59ef7593b78dd827dd52c18c47681f6 |
+| SCOPE.md | c3cb56539a6b1dcb41c6ac378c1797e95ef878ba03276456276e0bb3abfa3ddd |
+| tests/test_gate.py | b5fc1b723d5137d0a41ebb67b29e25da727edfad391d62afa6d44c32b5e114c6 |
+
+All manifest-bound files were independently hashed; no mismatches were found.
+The public source identity and exposure remain those explicitly recorded in
+DM2_NONAUTHOR_REVIEW.md: the preserved P02-LM-002 export at base c4eabc1a,
+not inspection of the primary Drive proofs or historical independent audits.
+That original review note remains unchanged and pertains to its original bytes.
+This note supplies the actual new source review rather than rebinding the old one.
+
+## Dependency and preservation findings
+
+No substantive source-alignment regression was found. Direct Git comparison
+with `deb28a751f620715ec65d3bd73690905e6fee94d` shows that the only changes
+to all three Lean modules are their initial import lines. Removing lines that
+begin with `import ` yields identical remaining bytes, including every
+definition, theorem statement, hypothesis, proof and namespace command.
+The stripped-body SHA256 values are:
+
+| Module | Non-import body SHA256 |
+|---|---|
+| AlgebraV2 | 50938dbae8a0d74220d0ae1e69a6bf1be3cda47eec44970d24457c0347d75ff3 |
+| ProbabilityCompanionsV2 | 432ea418452a0ea49fcbb191026edc879981be97adecee0b836a1e41ae5882fe |
+| DeterminantMoment | 843c04288e7943d97e80fc9e434c7ce36d7eda85a840320604af592dc8937fec |
+
+All new direct imports are Mathlib modules under the same pinned dependency.
+Algebra imports real basics and its field/ring/numerical tactics; probability
+companions import real square root and their arithmetic tactics; DM2 imports
+Bochner integration, matrix determinants/topology, ordered measurable groups
+and its existing proof tactics. No local extra axiom or replacement mathematical
+definition is introduced. These import changes alter the dependency closure;
+they still require fresh replay and transitive axiom audit.
+
+Gate.py, toolchain, lake dependency manifest, lake configuration and both false
+DM2 fixtures were byte-compared with deb28a and are unchanged. The two baseline
+preservation tests now require the exact narrow import lists and retain their
+comparison of the entire remaining expected source against preserved originals
+plus the previously documented historical compiler repairs. This is a bounded
+test adjustment, not replacement of full-body preservation with theorem-name
+or partial-text matching. The reviewed fixture witnesses remain mathematically
+false for the reasons in the original signed note.
+
+The exact matrices, all nine radius coordinates, quadratic-form indicator,
+pointwise hypotheses and genuine eighth-moment integrability premises are
+preserved. The arbitrary-measure expectation theorem remains a sound stronger
+version of the public probability-law implication. The source's uniform-family
+corollary still needs one common supplied M8. Concrete Gaussian moments, Palm
+identification, lower normalizer, event coverage and parent results remain open.
+The documentation accurately distinguishes this successor and its changed
+imports from the historical baseline bytes and review. No full thirteen-target
+baseline source alignment is independently certified here.
+
+## Evidence inspected and limitations
+
+This reviewer ran the revised Python test suite in both normal and optimized
+modes: 78 tests passed in each. No competing compiler or checker was run.
+
+The retained RED log reports exactly two failures. A precision caveat: it tests
+precursor headers Mathlib.Data.Real.Basic and Mathlib.Data.Real.Sqrt, whereas
+the final tests pin Mathlib.Basic.Real.Basic and Mathlib.Analysis.Real.Sqrt.
+The retained first narrow-build log records the deprecation guidance for those
+precursor names and an unsuccessful DM2 build; the second log records a
+successful build using the final source. Thus RED is evidence for the initial
+import-preservation change, not a literal replay of the final header strings.
+This does not weaken the exact current-source comparisons or the independently
+rerun passing tests. Future summaries should retain this distinction.
+
+The preserved umbrella-build log and RESULT.txt report a successful original
+build followed by checker exit 137, a 17179869184-byte cgroup limit, and one
+OOM kill. The original checker log is empty. These are retained author-side
+execution records; this reviewer did not independently observe that past cgroup
+state. The successful final narrow-build log was inspected, but compilation
+alone supplies neither full replay success nor alignment acceptance.
+
+The final gate replay was ongoing when this review was requested. This note
+does not claim its outcome, a fresh leanchecker pass, transitive axiom audit,
+negative-control execution success, or hosted-check success. Those require
+their actual separate evidence. The unchanged validator still requires distinct
+provider/family/agent identities and full target coverage. This same-provider
+bounded technical review cannot provide its machine ACCEPTED alignment record.
+
+Only this new evidence note was written by this reviewer; production sources
+and the original signed review were not edited.
diff --git a/frontiers/determinant_moment_20261025/evidence/DM2_NONAUTHOR_REVIEW.md b/frontiers/determinant_moment_20261025/evidence/DM2_NONAUTHOR_REVIEW.md
new file mode 100644
index 000000000..8f341dfc2
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/DM2_NONAUTHOR_REVIEW.md
@@ -0,0 +1,117 @@
+# DM2 nonauthor source and statement review
+
+Signed: OpenAI / GPT-6-Codex family / agent `/root/dm2_statement_review`,
+2026-10-25. Exact underlying model identifier is unavailable to this reviewer.
+Author reviewed: OpenAI/Codex `/root`. This is a separate reviewer context,
+same provider, original proof visible. Organizational-independence credit 0;
+acceptance credit 0; scientific effect NONE. No machine ACCEPTED alignment
+record is supplied.
+
+## Exact reviewed identity
+
+Repository `d6g8k5htny-coder/Math-`, frozen commit
+`deb28a751f620715ec65d3bd73690905e6fee94d`.
+All paths below are relative to `frontiers/determinant_moment_20261025/`.
+
+| File | SHA256 |
+|---|---|
+| ResearchFormalCoreR1/DeterminantMoment.lean | c12731c88cd7c7dee32b2cb59b3a4eb5016f2b59a96e3cda4b523632a0bf61c4 |
+| SOURCE_MAP.md | 1d21d9d283047a2bbaceec402e2af0009b2b53e3eb3c4fa47654b73bc748460e |
+| SCOPE.md | 7d8c3205bf1d382cb069aec38b7754a44af540e411762507e889eb61239ead4e |
+| manifest.json | fb0aac53dac710c4f03ae599aabc4b0955395e4a4bad047bd126595cc956d436 |
+| controls/false_omit_q.lean.txt | cbcd846199ff2f48099bc33518188ddfcd3667f9e7a9ef932a2627e69b540a46 |
+| controls/false_r6.lean.txt | c0ce4598ff5e188475e0ec9d0eeb3c3465169583a457baec90625d7b0f3a8439 |
+
+The actual public source inspected is
+`imports/hardening_ebedb780/P02-LM-002/proof.md.export.txt` at base
+`c4eabc1a917ba2c1b96fe4af425cf2a484877c03`, Git blob
+`d1fd7eccd5947cb6c5bf8724a77b7ec1c380a29b`, SHA256
+`0f8f80922feb603e5b6e530eb885a7819b3a98d90d3c42d60a68259af766f7de`.
+Both the base blob and working source hash were checked. Its claims about
+historical reviews remain source claims. GP-DER-071 and CL-AUD-052 themselves
+were not inspected. The original public proof and proposed implementation
+were visible; this is source-aware review, not clean-room reconstruction.
+
+## Findings
+
+No substantive mathematical source mismatch was found in the five new DM2
+declarations and their definitions. The final source was reread after the
+compiler repairs; their noncomputable annotations, classical decidability,
+algebra normalization and explicit measurable-set arguments preserve the
+mathematical contract reviewed initially.
+
+`DM2Jet` has nine real coordinates in the declared order. `dm2Radius` includes
+all nine absolute values plus one, including the unused z,c13,c04 coordinates.
+Both Hessians match section 2 exactly: the +/-r and +/-ar/2 signs, the
+rw/2 signs, and the 12 and 8 denominators all agree.
+
+`dm2Negative` is strict quadratic-form negativity at every nonzero real
+two-vector. Applied to the symmetric HM it is the source condition. The
+conjunction with strict det HS < 0 implements both indicators; singular and
+type-boundary cases need no exclusion or null-set assumption.
+
+`dm2_untyped` proves the stronger determinant-product square estimate before
+indicator restriction. Its factorization and coefficient bounds follow the
+source algebra. `dm2_pointwise` has exactly arbitrary real jets and 0 < r <= 1,
+with no Gaussianity, independence, type, or nonsingularity premise.
+
+`dm2_negative_iff` is the correct symmetric two-dimensional Sylvester
+criterion. Its forward direction tests (1,0) and (-b,a); the converse uses
+a times the quadratic form as the sum of the two displayed nonnegative
+squares, with strict positivity for a nonzero vector. The measurable-weight
+proof uses continuous polynomial strict inequalities and works for every
+real r, without a type-boundary measure premise.
+
+`dm2_moment` assumes a measurable jet map, actual integrability of R^8 and
+its integral bounded by M8. It derives squared-weight integrability and
+integral <= 16 M8 r^4 by domination. It does not assume its desired second
+moment. The arbitrary-measure generality is sound and stronger than the
+source probability-law implication. No explicit M8 >= 0 premise is needed:
+it follows from the nonnegative integrand and the supplied integral bound.
+The source uniform-family statement follows by applying this theorem to each
+law with the same M8; a concrete uniform M8 is not established here.
+
+The final declaration-level SCOPE accurately states these boundaries and
+resolves the initial short-scope documentation limitation. The source map's
+parent exclusions agree with formal/MOMENT_TAIL.md and MeasureBridge's
+remaining premises. Concrete field-jet identification, uniform moment bounds,
+normalizer floor, same typed Palm identification, full good-event coverage,
+GT5, P0.2, lifetime and persistence remain open. No full parent composition
+or baseline-target alignment is certified by this review.
+
+## False mutation checks
+
+Both fixtures state genuinely false inequalities, established here by exact
+hand substitution, independently of any compiler-failure report.
+
+For false_omit_q, r=1/2 and q=-100 with other coordinates zero give
+det HM=50, det HS=-50, and LHS=6,250,000. The mutated RHS is 1. The actual
+radius is 101. Thus omission of q destroys the proposed bound.
+
+For false_r6, r=1/128 and q=-1 with other coordinates zero give R=2,
+det HM=r and det HS=-r. The LHS is r^4=2^-28 and mutated RHS
+16 r^6 2^8=2^-30, so the LHS is four times the RHS. In both controls HM is
+negative definite and det HS is negative; the same witnesses also refute
+the corresponding typed-weight mutations. These fixtures directly state
+counterexample inequalities rather than universal mutated theorem statements.
+
+## Gate and review boundary
+
+The retained gate SHA256 is
+`25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a`,
+equal to formal/gate.py at the cited base. Its provider-distinct alignment
+validator remains unchanged. OpenAI author and OpenAI reviewer fail that
+identity condition, regardless of separate agent contexts. The later owner
+loosening allows truthful same-provider review labels; it does not make this
+review pass the unchanged executable validator. The review is limited to the
+five new DM2 declarations, source mapping, explicit scope and two mutations;
+it is not full 18-target baseline alignment.
+
+Compiler success was reported by the author during the final revalidation
+request. This reviewer did not execute or audit the build, leanchecker,
+transitive axiom inventory, rejection-control runs or hosted checks. Their
+actual execution evidence must be assessed separately. No execution success
+or independent acceptance is inferred from source inspection or hashes.
+
+Read-only review of production files; this evidence note is the reviewer's
+only authored repository addition.
diff --git a/frontiers/determinant_moment_20261025/evidence/final/Audit.lean.txt b/frontiers/determinant_moment_20261025/evidence/final/Audit.lean.txt
new file mode 100644
index 000000000..7e8e0a58c
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/Audit.lean.txt
@@ -0,0 +1,19 @@
+import ResearchFormalCoreR1
+#print axioms ResearchFormalCoreR1.ec005_fold_gap
+#print axioms ResearchFormalCoreR1.ec008_factor_expansion
+#print axioms ResearchFormalCoreR1.ec010_generic
+#print axioms ResearchFormalCoreR1.ec010_transverse
+#print axioms ResearchFormalCoreR1.ec011_scalar_cancellation
+#print axioms ResearchFormalCoreR1.ec014_contact_power
+#print axioms ResearchFormalCoreR1.p02_lm008_r2_cancel
+#print axioms ResearchFormalCoreR1.p02_lm008_cross_multiplied
+#print axioms ResearchFormalCoreR1.p02_lm008_quotient_bound
+#print axioms ResearchFormalCoreR1.p02_lm009_bad_event_threshold
+#print axioms ResearchFormalCoreR1.p02_lm009_power40_identity
+#print axioms ResearchFormalCoreR1.p02_lm009_r4_le_r3
+#print axioms ResearchFormalCoreR1.p02_lm009_palm_r4_to_r3
+#print axioms ResearchFormalCoreR1.dm2_untyped
+#print axioms ResearchFormalCoreR1.dm2_pointwise
+#print axioms ResearchFormalCoreR1.dm2_negative_iff
+#print axioms ResearchFormalCoreR1.dm2_weight_measurable
+#print axioms ResearchFormalCoreR1.dm2_moment
diff --git a/frontiers/determinant_moment_20261025/evidence/final/EXPORT_IDENTITIES.json b/frontiers/determinant_moment_20261025/evidence/final/EXPORT_IDENTITIES.json
new file mode 100644
index 000000000..d4499c430
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/EXPORT_IDENTITIES.json
@@ -0,0 +1,116 @@
+{
+  "checked_commit": "dcfc89366f590342b4cd30b141a22c9ae2a562bb",
+  "proof_manifest_sha256": "cb2b4870debf98cdf3663663797ccfc524e23d5f41f89e1c9ecdba5b6e680811",
+  "evidence_kind": "LOCAL_EXECUTION_NOT_HOSTED",
+  "receipt_sha256": "8fe7ab0f131a8a5c3e459d3bbbd10b4ab2b135438793851c11b25f7bb69f9eeb",
+  "files": {
+    "Audit.lean.txt": {
+      "bytes": 1021,
+      "sha256": "d4290700db5b7633cbb98b7a5b9cd2a9ed9c2f93e00425ea4eeba871859ea587"
+    },
+    "Types.lean.txt": {
+      "bytes": 923,
+      "sha256": "84f2580641d1dbf7efbff27f6cc011046d810d9ec1745bf69f7d71241f1d665b"
+    },
+    "axioms.log": {
+      "bytes": 1839,
+      "sha256": "0fd7b72c24a218f67e7782091006440c909718fff19ca0bc112dd66bf66d91c6"
+    },
+    "build.log": {
+      "bytes": 1010,
+      "sha256": "08961056e6112175d291708c2b3e99c13ff75fb1511e7d702a99a1552b625859"
+    },
+    "custom_imported.lean.txt": {
+      "bytes": 154,
+      "sha256": "2fa48cd0eb38fba402d75291e3861db0aa2875bea8bb397085bba6fc8b155e87"
+    },
+    "custom_imported.log": {
+      "bytes": 46,
+      "sha256": "6e7f917c7fe2fdc3efe1943dcc327c56acadd0b0ca96507a4327073fdfd2f083"
+    },
+    "dm2_extra_controls.json": {
+      "bytes": 996,
+      "sha256": "728b7833be50bb164b02b90d6702c6076fdb159605493064ab5845c31a1fdd18"
+    },
+    "dm2_false_omit_q.lean.txt": {
+      "bytes": 315,
+      "sha256": "cbcd846199ff2f48099bc33518188ddfcd3667f9e7a9ef932a2627e69b540a46"
+    },
+    "dm2_false_omit_q.log": {
+      "bytes": 137,
+      "sha256": "a1d9cc2f68628e6bb7d11f91265fadc8ab1f6f34b277cfcfe785d46d92f40a67"
+    },
+    "dm2_false_r6.lean.txt": {
+      "bytes": 323,
+      "sha256": "c0ce4598ff5e188475e0ec9d0eeb3c3465169583a457baec90625d7b0f3a8439"
+    },
+    "dm2_false_r6.log": {
+      "bytes": 133,
+      "sha256": "8c2a173f0db626faad2b7d100cafbcc1d2b2c13ff691de6523621a457454f03f"
+    },
+    "elaborated-types.log": {
+      "bytes": 32201,
+      "sha256": "f5b78a40cf0261ee5af6a9b18906c1c30d185fd186362d11cd13e87ee60e0a7f"
+    },
+    "false_fold.lean.txt": {
+      "bytes": 194,
+      "sha256": "728491968589862a526a1e5fdd3950029cd894f62d2f3795bd83d8ffba45856b"
+    },
+    "false_fold.log": {
+      "bytes": 132,
+      "sha256": "0c0d91c62fbbdeed9ac1f8b968f9d73b701b8079089bd90c07c0af6fcf9ce686"
+    },
+    "false_power.lean.txt": {
+      "bytes": 84,
+      "sha256": "63b53a6959e01168b5b05c97d4c86cb5e08ac61928656c1de19e81f27ea088ae"
+    },
+    "false_power.log": {
+      "bytes": 132,
+      "sha256": "eccbb6ccf7bded2d8ba23f1c2b78b146564a467b848e2c431a76d1dabd053a9c"
+    },
+    "gate-terminal.log": {
+      "bytes": 6565,
+      "sha256": "07309bbdedefa38de42b102bc02eeb1e6f0a7aea26d9b40c834cb70d7a4f1ce8"
+    },
+    "leanchecker.log": {
+      "bytes": 0,
+      "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    "native.lean.txt": {
+      "bytes": 108,
+      "sha256": "12e4f50be5dd78e753cde71e469efab6b79d6ff1b496aa463cf6f7a7c2f8418f"
+    },
+    "native.log": {
+      "bytes": 70,
+      "sha256": "8a0b9f79f3265724af58b27461627f9d532535f8a23681361da731c9ea37c101"
+    },
+    "receipt.json": {
+      "bytes": 6357,
+      "sha256": "8fe7ab0f131a8a5c3e459d3bbbd10b4ab2b135438793851c11b25f7bb69f9eeb"
+    },
+    "sorry.lean.txt": {
+      "bytes": 88,
+      "sha256": "684559bcb801f79ac1bba8890a2a6a9f5455d0279dd15be42d8edcdd5cd7b2cb"
+    },
+    "sorry.log": {
+      "bytes": 167,
+      "sha256": "afc2bcbd48dbe1be41b06656bc3cbb8eb5b2fae535b72bca51dacfe3071fb469"
+    },
+    "tests-normal.log": {
+      "bytes": 8400,
+      "sha256": "c84676c7036c22c56394678b2b38d229573121339a7225bdfd4ad84682980300"
+    },
+    "tests-optimized.log": {
+      "bytes": 8400,
+      "sha256": "2db3a6f23190e12f605ab5c855d6bbb279fb764612202d915ccd88d4f2ad3367"
+    },
+    "version-preflight.log": {
+      "bytes": 106,
+      "sha256": "355a9a028f81641782d75d6e6b58dec70f29d2f61238a9e271690259d9bf5680"
+    },
+    "version.log": {
+      "bytes": 106,
+      "sha256": "355a9a028f81641782d75d6e6b58dec70f29d2f61238a9e271690259d9bf5680"
+    }
+  }
+}
diff --git a/frontiers/determinant_moment_20261025/evidence/final/Types.lean.txt b/frontiers/determinant_moment_20261025/evidence/final/Types.lean.txt
new file mode 100644
index 000000000..1ace387b0
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/Types.lean.txt
@@ -0,0 +1,20 @@
+import ResearchFormalCoreR1
+set_option pp.explicit true
+#check ResearchFormalCoreR1.ec005_fold_gap
+#check ResearchFormalCoreR1.ec008_factor_expansion
+#check ResearchFormalCoreR1.ec010_generic
+#check ResearchFormalCoreR1.ec010_transverse
+#check ResearchFormalCoreR1.ec011_scalar_cancellation
+#check ResearchFormalCoreR1.ec014_contact_power
+#check ResearchFormalCoreR1.p02_lm008_r2_cancel
+#check ResearchFormalCoreR1.p02_lm008_cross_multiplied
+#check ResearchFormalCoreR1.p02_lm008_quotient_bound
+#check ResearchFormalCoreR1.p02_lm009_bad_event_threshold
+#check ResearchFormalCoreR1.p02_lm009_power40_identity
+#check ResearchFormalCoreR1.p02_lm009_r4_le_r3
+#check ResearchFormalCoreR1.p02_lm009_palm_r4_to_r3
+#check ResearchFormalCoreR1.dm2_untyped
+#check ResearchFormalCoreR1.dm2_pointwise
+#check ResearchFormalCoreR1.dm2_negative_iff
+#check ResearchFormalCoreR1.dm2_weight_measurable
+#check ResearchFormalCoreR1.dm2_moment
diff --git a/frontiers/determinant_moment_20261025/evidence/final/axioms.log b/frontiers/determinant_moment_20261025/evidence/final/axioms.log
new file mode 100644
index 000000000..6b8d96789
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/axioms.log
@@ -0,0 +1,18 @@
+'ResearchFormalCoreR1.ec005_fold_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ResearchFormalCoreR1.ec008_factor_expansion' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ResearchFormalCoreR1.ec010_generic' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ResearchFormalCoreR1.ec010_transverse' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ResearchFormalCoreR1.ec011_scalar_cancellation' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ResearchFormalCoreR1.ec014_contact_power' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ResearchFormalCoreR1.p02_lm008_r2_cancel' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ResearchFormalCoreR1.p02_lm008_cross_multiplied' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ResearchFormalCoreR1.p02_lm008_quotient_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ResearchFormalCoreR1.p02_lm009_bad_event_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ResearchFormalCoreR1.p02_lm009_power40_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ResearchFormalCoreR1.p02_lm009_r4_le_r3' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ResearchFormalCoreR1.p02_lm009_palm_r4_to_r3' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ResearchFormalCoreR1.dm2_untyped' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ResearchFormalCoreR1.dm2_pointwise' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ResearchFormalCoreR1.dm2_negative_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ResearchFormalCoreR1.dm2_weight_measurable' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ResearchFormalCoreR1.dm2_moment' depends on axioms: [propext, Classical.choice, Quot.sound]
diff --git a/frontiers/determinant_moment_20261025/evidence/final/build.log b/frontiers/determinant_moment_20261025/evidence/final/build.log
new file mode 100644
index 000000000..ff5d11459
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/build.log
@@ -0,0 +1,17 @@
+✔ [2557/2561] Built ResearchFormalCoreR1.AlgebraV2 (2.1s)
+⚠ [2558/2561] Built ResearchFormalCoreR1.ProbabilityCompanionsV2 (1.9s)
+warning: ResearchFormalCoreR1/ProbabilityCompanionsV2.lean:27:18: Variable name `hcW` is not explicitly referenced.
+
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _hcW
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
+warning: ResearchFormalCoreR1/ProbabilityCompanionsV2.lean:27:48: Variable name `hq` is not explicitly referenced.
+
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _hq
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
+✔ [2559/2561] Built ResearchFormalCoreR1.DeterminantMoment (7.2s)
+✔ [2560/2561] Built ResearchFormalCoreR1 (1.6s)
+Build completed successfully (2561 jobs).
diff --git a/frontiers/determinant_moment_20261025/evidence/final/custom_imported.lean.txt b/frontiers/determinant_moment_20261025/evidence/final/custom_imported.lean.txt
new file mode 100644
index 000000000..365006fe0
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/custom_imported.lean.txt
@@ -0,0 +1,5 @@
+import ResearchFormalCoreR1
+axiom hiddenPremise : False
+theorem middle : False := hiddenPremise
+theorem injected : False := middle
+#print axioms injected
diff --git a/frontiers/determinant_moment_20261025/evidence/final/custom_imported.log b/frontiers/determinant_moment_20261025/evidence/final/custom_imported.log
new file mode 100644
index 000000000..52be5f132
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/custom_imported.log
@@ -0,0 +1 @@
+'injected' depends on axioms: [hiddenPremise]
diff --git a/frontiers/determinant_moment_20261025/evidence/final/dm2_extra_controls.json b/frontiers/determinant_moment_20261025/evidence/final/dm2_extra_controls.json
new file mode 100644
index 000000000..21f64dffc
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/dm2_extra_controls.json
@@ -0,0 +1,30 @@
+[
+  {
+    "label": "false_r6",
+    "argv": [
+      "/home/agent/.elan/bin/lake",
+      "env",
+      "lean",
+      "/workspace/Math-/frontiers/determinant_moment_20261025/.lake/formal-evidence/dm2_false_r6.lean"
+    ],
+    "exit_code": 1,
+    "elapsed_seconds": 2.4222649689999116,
+    "intended_goal_refusal": true,
+    "source_sha256": "c0ce4598ff5e188475e0ec9d0eeb3c3465169583a457baec90625d7b0f3a8439",
+    "log_sha256": "8c2a173f0db626faad2b7d100cafbcc1d2b2c13ff691de6523621a457454f03f"
+  },
+  {
+    "label": "false_omit_q",
+    "argv": [
+      "/home/agent/.elan/bin/lake",
+      "env",
+      "lean",
+      "/workspace/Math-/frontiers/determinant_moment_20261025/.lake/formal-evidence/dm2_false_omit_q.lean"
+    ],
+    "exit_code": 1,
+    "elapsed_seconds": 2.196419590000005,
+    "intended_goal_refusal": true,
+    "source_sha256": "cbcd846199ff2f48099bc33518188ddfcd3667f9e7a9ef932a2627e69b540a46",
+    "log_sha256": "a1d9cc2f68628e6bb7d11f91265fadc8ab1f6f34b277cfcfe785d46d92f40a67"
+  }
+]
diff --git a/frontiers/determinant_moment_20261025/evidence/final/dm2_false_omit_q.lean.txt b/frontiers/determinant_moment_20261025/evidence/final/dm2_false_omit_q.lean.txt
new file mode 100644
index 000000000..3b1e86908
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/dm2_false_omit_q.lean.txt
@@ -0,0 +1,6 @@
+import ResearchFormalCoreR1
+open ResearchFormalCoreR1
+-- Deliberately false: q removed from the radius.
+example : let j : DM2Jet := ![(-100),0,0,0,0,0,0,0,0]
+    ((dm2HM (1/2) j).det*(dm2HS (1/2) j).det)^2 ≤ 16*((1/2) : ℝ)^4*1^8 := by
+  norm_num [dm2HM, dm2HS, dm2Radius, Matrix.det_fin_two, Fin.sum_univ_succ]
diff --git a/frontiers/determinant_moment_20261025/evidence/final/dm2_false_omit_q.log b/frontiers/determinant_moment_20261025/evidence/final/dm2_false_omit_q.log
new file mode 100644
index 000000000..48d572705
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/dm2_false_omit_q.log
@@ -0,0 +1,2 @@
+/workspace/Math-/frontiers/determinant_moment_20261025/.lake/formal-evidence/dm2_false_omit_q.lean:5:74: error: unsolved goals
+⊢ False
diff --git a/frontiers/determinant_moment_20261025/evidence/final/dm2_false_r6.lean.txt b/frontiers/determinant_moment_20261025/evidence/final/dm2_false_r6.lean.txt
new file mode 100644
index 000000000..3a4090ef1
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/dm2_false_r6.lean.txt
@@ -0,0 +1,6 @@
+import ResearchFormalCoreR1
+open ResearchFormalCoreR1
+-- Deliberately false: r^4 replaced by r^6.
+example : let j : DM2Jet := ![(-1),0,0,0,0,0,0,0,0]
+    ((dm2HM (1/128) j).det*(dm2HS (1/128) j).det)^2 ≤ 16*((1/128) : ℝ)^6*dm2Radius j^8 := by
+  norm_num [dm2HM, dm2HS, dm2Radius, Matrix.det_fin_two, Fin.sum_univ_succ]
diff --git a/frontiers/determinant_moment_20261025/evidence/final/dm2_false_r6.log b/frontiers/determinant_moment_20261025/evidence/final/dm2_false_r6.log
new file mode 100644
index 000000000..8d9391494
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/dm2_false_r6.log
@@ -0,0 +1,2 @@
+/workspace/Math-/frontiers/determinant_moment_20261025/.lake/formal-evidence/dm2_false_r6.lean:5:90: error: unsolved goals
+⊢ False
diff --git a/frontiers/determinant_moment_20261025/evidence/final/elaborated-types.log b/frontiers/determinant_moment_20261025/evidence/final/elaborated-types.log
new file mode 100644
index 000000000..4292e2764
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/elaborated-types.log
@@ -0,0 +1,432 @@
+ResearchFormalCoreR1.ec005_fold_gap (s : Real) :
+  @Eq Real
+    (@HSub.hSub Real Real Real (@instHSub Real Real.instSub) (ResearchFormalCoreR1.foldPotential s s)
+      (ResearchFormalCoreR1.foldPotential s (@Neg.neg Real Real.instNeg s)))
+    (@HDiv.hDiv Real Real Real (@instHDiv Real (@DivInvMonoid.toDiv Real Real.instDivInvMonoid))
+      (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+        (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+          (@OfNat.ofNat Real (nat_lit 2) (@instOfNatAtLeastTwo Real (nat_lit 2) Real.instNatCast ⋯)) s)
+        (@OfNat.ofNat Nat (nat_lit 3) (instOfNatNat (nat_lit 3))))
+      (@OfNat.ofNat Real (nat_lit 6) (@instOfNatAtLeastTwo Real (nat_lit 6) Real.instNatCast ⋯)))
+ResearchFormalCoreR1.ec008_factor_expansion (c s : Real) :
+  @Eq Real
+    (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+        (@OfNat.ofNat Real (nat_lit 2) (@instOfNatAtLeastTwo Real (nat_lit 2) Real.instNatCast ⋯))
+        (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) s
+          (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))))
+      (@HSub.hSub Real Real Real (@instHSub Real Real.instSub)
+        (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+          (@HDiv.hDiv Real Real Real (@instHDiv Real (@DivInvMonoid.toDiv Real Real.instDivInvMonoid))
+            (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+              (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) s
+                (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+              (@HAdd.hAdd Real Real Real (@instHAdd Real Real.instAdd)
+                (@HAdd.hAdd Real Real Real (@instHAdd Real Real.instAdd)
+                  (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+                    (@OfNat.ofNat Real (nat_lit 3) (@instOfNatAtLeastTwo Real (nat_lit 3) Real.instNatCast ⋯))
+                    (@HPow.hPow Real Nat Real
+                      (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) c
+                      (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))))
+                  (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+                    (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+                      (@OfNat.ofNat Real (nat_lit 3) (@instOfNatAtLeastTwo Real (nat_lit 3) Real.instNatCast ⋯))
+                      (@HPow.hPow Real Nat Real
+                        (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) c
+                        (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))))
+                    (@HPow.hPow Real Nat Real
+                      (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) s
+                      (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))))
+                (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+                  s (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))))))
+            (@OfNat.ofNat Real (nat_lit 24) (@instOfNatAtLeastTwo Real (nat_lit 24) Real.instNatCast ⋯)))
+          (@HDiv.hDiv Real Real Real (@instHDiv Real (@DivInvMonoid.toDiv Real Real.instDivInvMonoid))
+            (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+              (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) s
+                (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+              (@HAdd.hAdd Real Real Real (@instHAdd Real Real.instAdd)
+                (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+                  (@OfNat.ofNat Real (nat_lit 4) (@instOfNatAtLeastTwo Real (nat_lit 4) Real.instNatCast ⋯))
+                  (@HPow.hPow Real Nat Real
+                    (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) c
+                    (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))))
+                (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+                  s (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))))
+            (@OfNat.ofNat Real (nat_lit 2) (@instOfNatAtLeastTwo Real (nat_lit 2) Real.instNatCast ⋯))))
+        (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+          (@HDiv.hDiv Real Real Real (@instHDiv Real (@DivInvMonoid.toDiv Real Real.instDivInvMonoid))
+            (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+              (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) (@Neg.neg Real Real.instNeg c)
+                (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+                  s (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))))
+              (@HAdd.hAdd Real Real Real (@instHAdd Real Real.instAdd)
+                (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+                  (@OfNat.ofNat Real (nat_lit 2) (@instOfNatAtLeastTwo Real (nat_lit 2) Real.instNatCast ⋯))
+                  (@HPow.hPow Real Nat Real
+                    (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) c
+                    (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))))
+                (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+                  s (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))))
+            (@OfNat.ofNat Real (nat_lit 4) (@instOfNatAtLeastTwo Real (nat_lit 4) Real.instNatCast ⋯)))
+          (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))))
+    (@HDiv.hDiv Real Real Real (@instHDiv Real (@DivInvMonoid.toDiv Real Real.instDivInvMonoid))
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+        (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+          (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) s
+            (@OfNat.ofNat Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
+          (@HAdd.hAdd Real Real Real (@instHAdd Real Real.instAdd)
+            (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) c
+              (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+            (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) s
+              (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))))
+        (@HAdd.hAdd Real Real Real (@instHAdd Real Real.instAdd)
+          (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+            (@OfNat.ofNat Real (nat_lit 3) (@instOfNatAtLeastTwo Real (nat_lit 3) Real.instNatCast ⋯))
+            (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) c
+              (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))))
+          (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) s
+            (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))))
+      (@OfNat.ofNat Real (nat_lit 24) (@instOfNatAtLeastTwo Real (nat_lit 24) Real.instNatCast ⋯)))
+ResearchFormalCoreR1.ec010_generic (α K c η : Real) :
+  @Eq Real
+    (@HAdd.hAdd Real Real Real (@instHAdd Real Real.instAdd)
+      (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+        (@HAdd.hAdd Real Real Real (@instHAdd Real Real.instAdd) K
+          (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+            (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+              (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+                (@OfNat.ofNat Real (nat_lit 8) (@instOfNatAtLeastTwo Real (nat_lit 8) Real.instNatCast ⋯)) α)
+              c)
+            η))
+        (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+        (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+          (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+            (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+              (@OfNat.ofNat Real (nat_lit 64) (@instOfNatAtLeastTwo Real (nat_lit 64) Real.instNatCast ⋯)) α)
+            (@HSub.hSub Real Real Real (@instHSub Real Real.instSub)
+              (@OfNat.ofNat Real (nat_lit 1) (@One.toOfNat1 Real Real.instOne)) α))
+          (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) c
+            (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))))
+        (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) η
+          (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))))
+    (@HAdd.hAdd Real Real Real (@instHAdd Real Real.instAdd)
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+        (@HSub.hSub Real Real Real (@instHSub Real Real.instSub)
+          (@OfNat.ofNat Real (nat_lit 1) (@One.toOfNat1 Real Real.instOne)) α)
+        (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) K
+          (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))))
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) α
+        (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+          (@HAdd.hAdd Real Real Real (@instHAdd Real Real.instAdd) K
+            (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+              (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+                (@OfNat.ofNat Real (nat_lit 8) (@instOfNatAtLeastTwo Real (nat_lit 8) Real.instNatCast ⋯)) c)
+              η))
+          (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))))
+ResearchFormalCoreR1.ec010_transverse (α a η : Real) :
+  @Eq Real
+    (@HAdd.hAdd Real Real Real (@instHAdd Real Real.instAdd)
+      (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+        (@HAdd.hAdd Real Real Real (@instHAdd Real Real.instAdd) a
+          (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+            (@HSub.hSub Real Real Real (@instHSub Real Real.instSub)
+              (@OfNat.ofNat Real (nat_lit 1) (@One.toOfNat1 Real Real.instOne))
+              (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+                (@OfNat.ofNat Real (nat_lit 2) (@instOfNatAtLeastTwo Real (nat_lit 2) Real.instNatCast ⋯)) α))
+            η))
+        (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+        (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+          (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+            (@OfNat.ofNat Real (nat_lit 4) (@instOfNatAtLeastTwo Real (nat_lit 4) Real.instNatCast ⋯)) α)
+          (@HSub.hSub Real Real Real (@instHSub Real Real.instSub)
+            (@OfNat.ofNat Real (nat_lit 1) (@One.toOfNat1 Real Real.instOne)) α))
+        (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) η
+          (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))))
+    (@HAdd.hAdd Real Real Real (@instHAdd Real Real.instAdd)
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+        (@HSub.hSub Real Real Real (@instHSub Real Real.instSub)
+          (@OfNat.ofNat Real (nat_lit 1) (@One.toOfNat1 Real Real.instOne)) α)
+        (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+          (@HAdd.hAdd Real Real Real (@instHAdd Real Real.instAdd) a η)
+          (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))))
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) α
+        (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+          (@HSub.hSub Real Real Real (@instHSub Real Real.instSub) a η)
+          (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))))
+ResearchFormalCoreR1.ec011_scalar_cancellation (h w g : Real) :
+  @Eq Real
+    (@HAdd.hAdd Real Real Real (@instHAdd Real Real.instAdd)
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+        (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) (@Neg.neg Real Real.instNeg h) w) g)
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) w
+        (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) h g)))
+    (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero))
+ResearchFormalCoreR1.ec014_contact_power (r : Real)
+  (hr : @Ne Real r (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero))) :
+  @Eq Real
+    (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+        (@HDiv.hDiv Real Real Real (@instHDiv Real (@DivInvMonoid.toDiv Real Real.instDivInvMonoid))
+          (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+            (@OfNat.ofNat Nat (nat_lit 3) (instOfNatNat (nat_lit 3))))
+          (@OfNat.ofNat Real (nat_lit 6) (@instOfNatAtLeastTwo Real (nat_lit 6) Real.instNatCast ⋯)))
+        (@HDiv.hDiv Real Real Real (@instHDiv Real (@DivInvMonoid.toDiv Real Real.instDivInvMonoid))
+          (@OfNat.ofNat Real (nat_lit 1) (@One.toOfNat1 Real Real.instOne))
+          (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+            (@OfNat.ofNat Nat (nat_lit 5) (instOfNatNat (nat_lit 5))))))
+      (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+        (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))))
+    (@HDiv.hDiv Real Real Real (@instHDiv Real (@DivInvMonoid.toDiv Real Real.instDivInvMonoid))
+      (@OfNat.ofNat Real (nat_lit 1) (@One.toOfNat1 Real Real.instOne))
+      (@OfNat.ofNat Real (nat_lit 6) (@instOfNatAtLeastTwo Real (nat_lit 6) Real.instNatCast ⋯)))
+ResearchFormalCoreR1.p02_lm008_r2_cancel (r cW cZ q : Real)
+  (hr : @Ne Real r (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)))
+  (hcZ : @Ne Real cZ (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero))) :
+  @Eq Real
+    (@HDiv.hDiv Real Real Real (@instHDiv Real (@DivInvMonoid.toDiv Real Real.instDivInvMonoid))
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+        (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) cW.sqrt
+          (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+            (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))))
+        q.sqrt)
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) cZ
+        (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+          (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))))
+    (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+      (@HDiv.hDiv Real Real Real (@instHDiv Real (@DivInvMonoid.toDiv Real Real.instDivInvMonoid)) cW.sqrt cZ) q.sqrt)
+ResearchFormalCoreR1.p02_lm008_cross_multiplied (n z r cW cZ q : Real)
+  (hr : @LT.lt Real Real.instLT (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)) r)
+  (hcW : @LE.le Real Real.instLE (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)) cW)
+  (hcZ : @LT.lt Real Real.instLT (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)) cZ)
+  (hq : @LE.le Real Real.instLE (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)) q)
+  (hz :
+    @LE.le Real Real.instLE
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) cZ
+        (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+          (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))))
+      z)
+  (hn :
+    @LE.le Real Real.instLE n
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+        (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) cW.sqrt
+          (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+            (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))))
+        q.sqrt)) :
+  @LE.le Real Real.instLE
+    (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) n
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) cZ
+        (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+          (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))))
+    (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+        (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) cW.sqrt
+          (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+            (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))))
+        q.sqrt)
+      z)
+ResearchFormalCoreR1.p02_lm008_quotient_bound (n z r cW cZ q : Real)
+  (hr : @LT.lt Real Real.instLT (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)) r)
+  (hcW : @LE.le Real Real.instLE (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)) cW)
+  (hcZ : @LT.lt Real Real.instLT (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)) cZ)
+  (hq : @LE.le Real Real.instLE (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)) q)
+  (hzpos : @LT.lt Real Real.instLT (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)) z)
+  (hz :
+    @LE.le Real Real.instLE
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) cZ
+        (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+          (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))))
+      z)
+  (hn :
+    @LE.le Real Real.instLE n
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+        (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) cW.sqrt
+          (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+            (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))))
+        q.sqrt)) :
+  @LE.le Real Real.instLE
+    (@HDiv.hDiv Real Real Real (@instHDiv Real (@DivInvMonoid.toDiv Real Real.instDivInvMonoid)) n z)
+    (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+      (@HDiv.hDiv Real Real Real (@instHDiv Real (@DivInvMonoid.toDiv Real Real.instDivInvMonoid)) cW.sqrt cZ) q.sqrt)
+ResearchFormalCoreR1.p02_lm009_bad_event_threshold (r R ε : Real)
+  (hr : @LT.lt Real Real.instLT (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)) r)
+  (hbad :
+    @LT.lt Real Real.instLT ε
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) r
+        (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) R
+          (@OfNat.ofNat Nat (nat_lit 5) (instOfNatNat (nat_lit 5)))))) :
+  @LT.lt Real Real.instLT
+    (@HDiv.hDiv Real Real Real (@instHDiv Real (@DivInvMonoid.toDiv Real Real.instDivInvMonoid)) ε r)
+    (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) R
+      (@OfNat.ofNat Nat (nat_lit 5) (instOfNatNat (nat_lit 5))))
+ResearchFormalCoreR1.p02_lm009_power40_identity (R : Real) :
+  @Eq Real
+    (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+      (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) R
+        (@OfNat.ofNat Nat (nat_lit 5) (instOfNatNat (nat_lit 5))))
+      (@OfNat.ofNat Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
+    (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) R
+      (@OfNat.ofNat Nat (nat_lit 40) (instOfNatNat (nat_lit 40))))
+ResearchFormalCoreR1.p02_lm009_r4_le_r3 (r : Real)
+  (hr0 : @LE.le Real Real.instLE (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)) r)
+  (hr1 : @LE.le Real Real.instLE r (@OfNat.ofNat Real (nat_lit 1) (@One.toOfNat1 Real Real.instOne))) :
+  @LE.le Real Real.instLE
+    (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+      (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))))
+    (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+      (@OfNat.ofNat Nat (nat_lit 3) (instOfNatNat (nat_lit 3))))
+ResearchFormalCoreR1.p02_lm009_palm_r4_to_r3 (p C r : Real)
+  (hC : @LE.le Real Real.instLE (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)) C)
+  (hr0 : @LE.le Real Real.instLE (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)) r)
+  (hr1 : @LE.le Real Real.instLE r (@OfNat.ofNat Real (nat_lit 1) (@One.toOfNat1 Real Real.instOne)))
+  (hp :
+    @LE.le Real Real.instLE p
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) C
+        (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+          (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))))) :
+  @LE.le Real Real.instLE p
+    (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) C
+      (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+        (@OfNat.ofNat Nat (nat_lit 3) (instOfNatNat (nat_lit 3)))))
+ResearchFormalCoreR1.dm2_untyped (r : Real) (j : ResearchFormalCoreR1.DM2Jet)
+  (hr : @LT.lt Real Real.instLT (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)) r)
+  (hr1 : @LE.le Real Real.instLE r (@OfNat.ofNat Real (nat_lit 1) (@One.toOfNat1 Real Real.instOne))) :
+  @LE.le Real Real.instLE
+    (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+        (@Matrix.det (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+          (instDecidableEqFin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+          (Fin.fintype (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))) Real Real.commRing
+          (ResearchFormalCoreR1.dm2HM r j))
+        (@Matrix.det (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+          (instDecidableEqFin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+          (Fin.fintype (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))) Real Real.commRing
+          (ResearchFormalCoreR1.dm2HS r j)))
+      (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+    (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+        (@OfNat.ofNat Real (nat_lit 16) (@instOfNatAtLeastTwo Real (nat_lit 16) Real.instNatCast ⋯))
+        (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+          (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))))
+      (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+        (ResearchFormalCoreR1.dm2Radius j) (@OfNat.ofNat Nat (nat_lit 8) (instOfNatNat (nat_lit 8)))))
+ResearchFormalCoreR1.dm2_pointwise (r : Real) (j : ResearchFormalCoreR1.DM2Jet)
+  (hr : @LT.lt Real Real.instLT (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)) r)
+  (hr1 : @LE.le Real Real.instLE r (@OfNat.ofNat Real (nat_lit 1) (@One.toOfNat1 Real Real.instOne))) :
+  @LE.le Real Real.instLE
+    (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+      (ResearchFormalCoreR1.dm2Weight r j) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+    (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+        (@OfNat.ofNat Real (nat_lit 16) (@instOfNatAtLeastTwo Real (nat_lit 16) Real.instNatCast ⋯))
+        (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+          (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))))
+      (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+        (ResearchFormalCoreR1.dm2Radius j) (@OfNat.ofNat Nat (nat_lit 8) (instOfNatNat (nat_lit 8)))))
+ResearchFormalCoreR1.dm2_negative_iff (a b c : Real) :
+  Iff
+    (ResearchFormalCoreR1.dm2Negative
+      (@DFunLike.coe
+        (Equiv
+          (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) →
+            Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) → Real)
+          (Matrix (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+            (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))) Real))
+        (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) →
+          Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) → Real)
+        (fun x =>
+          Matrix (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+            (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))) Real)
+        (@EquivLike.toFunLike
+          (Equiv
+            (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) →
+              Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) → Real)
+            (Matrix (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+              (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))) Real))
+          (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) →
+            Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) → Real)
+          (Matrix (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+            (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))) Real)
+          (@Equiv.instEquivLike
+            (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) →
+              Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) → Real)
+            (Matrix (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+              (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))) Real)))
+        (@Matrix.of (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+          (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))) Real)
+        (@Matrix.vecCons (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) → Real)
+          (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))
+          (@Matrix.vecCons Real (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))) a
+            (@Matrix.vecCons Real (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) b (@Matrix.vecEmpty Real)))
+          (@Matrix.vecCons (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) → Real)
+            (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))
+            (@Matrix.vecCons Real (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))) b
+              (@Matrix.vecCons Real (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) c
+                (@Matrix.vecEmpty Real)))
+            (@Matrix.vecEmpty (Fin (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) → Real))))))
+    (And (@LT.lt Real Real.instLT a (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)))
+      (@LT.lt Real Real.instLT (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero))
+        (@HSub.hSub Real Real Real (@instHSub Real Real.instSub)
+          (@HMul.hMul Real Real Real (@instHMul Real Real.instMul) a c)
+          (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) b
+            (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))))))
+ResearchFormalCoreR1.dm2_weight_measurable (r : Real) :
+  @Measurable ResearchFormalCoreR1.DM2Jet Real
+    (@MeasurableSpace.pi (Fin (@OfNat.ofNat Nat (nat_lit 9) (instOfNatNat (nat_lit 9)))) (fun a => Real) fun a =>
+      Real.measurableSpace)
+    Real.measurableSpace (ResearchFormalCoreR1.dm2Weight r)
+ResearchFormalCoreR1.dm2_moment.{u_1} {Ω : Type u_1} [MeasurableSpace Ω] (μ : @MeasureTheory.Measure Ω inst✝)
+  (J : Ω → ResearchFormalCoreR1.DM2Jet)
+  (hJ :
+    @Measurable Ω ResearchFormalCoreR1.DM2Jet inst✝
+      (@MeasurableSpace.pi (Fin (@OfNat.ofNat Nat (nat_lit 9) (instOfNatNat (nat_lit 9)))) (fun a => Real) fun a =>
+        Real.measurableSpace)
+      J)
+  (r M8 : Real) (hr : @LT.lt Real Real.instLT (@OfNat.ofNat Real (nat_lit 0) (@Zero.toOfNat0 Real Real.instZero)) r)
+  (hr1 : @LE.le Real Real.instLE r (@OfNat.ofNat Real (nat_lit 1) (@One.toOfNat1 Real Real.instOne)))
+  (h8 :
+    @MeasureTheory.Integrable Real
+      (@UniformSpace.toTopologicalSpace Real (@PseudoMetricSpace.toUniformSpace Real Real.pseudoMetricSpace))
+      (@SeminormedAddGroup.toContinuousENorm Real
+        (@SeminormedAddCommGroup.toSeminormedAddGroup Real
+          (@NonUnitalSeminormedRing.toSeminormedAddCommGroup Real
+            (@NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing Real
+              (@SeminormedCommRing.toNonUnitalSeminormedCommRing Real
+                (@NormedCommRing.toSeminormedCommRing Real Real.normedCommRing))))))
+      Ω inst✝
+      (fun x =>
+        @HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+          (ResearchFormalCoreR1.dm2Radius (J x)) (@OfNat.ofNat Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
+      μ)
+  (hM8 :
+    @LE.le Real Real.instLE
+      (@MeasureTheory.integral Ω Real Real.normedAddCommGroup (@NormedField.toNormedSpace Real Real.normedField) inst✝ μ
+        fun x =>
+        @HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+          (ResearchFormalCoreR1.dm2Radius (J x)) (@OfNat.ofNat Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
+      M8) :
+  And
+    (@MeasureTheory.Integrable Real
+      (@UniformSpace.toTopologicalSpace Real (@PseudoMetricSpace.toUniformSpace Real Real.pseudoMetricSpace))
+      (@SeminormedAddGroup.toContinuousENorm Real
+        (@SeminormedAddCommGroup.toSeminormedAddGroup Real
+          (@NonUnitalSeminormedRing.toSeminormedAddCommGroup Real
+            (@NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing Real
+              (@SeminormedCommRing.toNonUnitalSeminormedCommRing Real
+                (@NormedCommRing.toSeminormedCommRing Real Real.normedCommRing))))))
+      Ω inst✝
+      (fun x =>
+        @HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+          (ResearchFormalCoreR1.dm2Weight r (J x)) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+      μ)
+    (@LE.le Real Real.instLE
+      (@MeasureTheory.integral Ω Real Real.normedAddCommGroup (@NormedField.toNormedSpace Real Real.normedField) inst✝ μ
+        fun x =>
+        @HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid)))
+          (ResearchFormalCoreR1.dm2Weight r (J x)) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+      (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+        (@HMul.hMul Real Real Real (@instHMul Real Real.instMul)
+          (@OfNat.ofNat Real (nat_lit 16) (@instOfNatAtLeastTwo Real (nat_lit 16) Real.instNatCast ⋯)) M8)
+        (@HPow.hPow Real Nat Real (@instHPow Real Nat (@NPow.toPow Real (@Monoid.toNPow Real Real.instMonoid))) r
+          (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))))))
diff --git a/frontiers/determinant_moment_20261025/evidence/final/false_fold.lean.txt b/frontiers/determinant_moment_20261025/evidence/final/false_fold.lean.txt
new file mode 100644
index 000000000..775823dc0
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/false_fold.lean.txt
@@ -0,0 +1,3 @@
+import ResearchFormalCoreR1
+example : ResearchFormalCoreR1.foldPotential 1 1 - ResearchFormalCoreR1.foldPotential 1 (-1) = (2 : Real)^3 / 7 := by
+  norm_num [ResearchFormalCoreR1.foldPotential]
diff --git a/frontiers/determinant_moment_20261025/evidence/final/false_fold.log b/frontiers/determinant_moment_20261025/evidence/final/false_fold.log
new file mode 100644
index 000000000..361f876d9
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/false_fold.log
@@ -0,0 +1,2 @@
+/workspace/Math-/frontiers/determinant_moment_20261025/.lake/formal-evidence/false_fold.lean:2:115: error: unsolved goals
+⊢ False
diff --git a/frontiers/determinant_moment_20261025/evidence/final/false_power.lean.txt b/frontiers/determinant_moment_20261025/evidence/final/false_power.lean.txt
new file mode 100644
index 000000000..b5aa5b89f
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/false_power.lean.txt
@@ -0,0 +1,3 @@
+import ResearchFormalCoreR1
+example : (2 : Real)^4 <= (2 : Real)^3 := by
+  norm_num
diff --git a/frontiers/determinant_moment_20261025/evidence/final/false_power.log b/frontiers/determinant_moment_20261025/evidence/final/false_power.log
new file mode 100644
index 000000000..baa89174a
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/false_power.log
@@ -0,0 +1,2 @@
+/workspace/Math-/frontiers/determinant_moment_20261025/.lake/formal-evidence/false_power.lean:2:42: error: unsolved goals
+⊢ False
diff --git a/frontiers/determinant_moment_20261025/evidence/final/gate-terminal.log b/frontiers/determinant_moment_20261025/evidence/final/gate-terminal.log
new file mode 100644
index 000000000..b136f4f1e
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/gate-terminal.log
@@ -0,0 +1,181 @@
+version-preflight: exit 0
+build: exit 0
+leanchecker: exit 0
+axioms: exit 0
+elaborated-types: exit 0
+false_fold: exit 1
+false_power: exit 1
+sorry: exit 0
+custom_imported: exit 0
+native: exit 0
+version: exit 0
+{
+  "alignment_status": "PENDING_INDEPENDENT_REVIEW",
+  "axioms": {
+    "ResearchFormalCoreR1.dm2_moment": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.dm2_negative_iff": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.dm2_pointwise": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.dm2_untyped": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.dm2_weight_measurable": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.ec005_fold_gap": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.ec008_factor_expansion": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.ec010_generic": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.ec010_transverse": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.ec011_scalar_cancellation": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.ec014_contact_power": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.p02_lm008_cross_multiplied": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.p02_lm008_quotient_bound": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.p02_lm008_r2_cancel": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.p02_lm009_bad_event_threshold": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.p02_lm009_palm_r4_to_r3": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.p02_lm009_power40_identity": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.p02_lm009_r4_le_r3": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ]
+  },
+  "checked_commit": "dcfc89366f590342b4cd30b141a22c9ae2a562bb",
+  "dependency_revisions": {
+    "Cli": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
+    "LeanSearchClient": "ddf04cf3949fa556442341e87d47f9f6e6074707",
+    "Qq": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259",
+    "aesop": "355695d523e41d0554926416cba2a2b3544fbbc9",
+    "batteries": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
+    "importGraph": "e928b72544873815af278d38681b31c0293588e3",
+    "mathlib": "d13f23b723b8a846827a245b89c10fc7d3f11612",
+    "plausible": "118aa17ee84656b8bd727fef7c458ee8c833385c",
+    "proofwidgets": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5"
+  },
+  "dependency_worktrees": "CLEAN",
+  "formalization_status": "kernel-checked",
+  "lean_version": "Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)",
+  "logs": {
+    "axioms.log": "0fd7b72c24a218f67e7782091006440c909718fff19ca0bc112dd66bf66d91c6",
+    "build.log": "08961056e6112175d291708c2b3e99c13ff75fb1511e7d702a99a1552b625859",
+    "custom_imported.log": "6e7f917c7fe2fdc3efe1943dcc327c56acadd0b0ca96507a4327073fdfd2f083",
+    "elaborated-types.log": "f5b78a40cf0261ee5af6a9b18906c1c30d185fd186362d11cd13e87ee60e0a7f",
+    "false_fold.log": "0c0d91c62fbbdeed9ac1f8b968f9d73b701b8079089bd90c07c0af6fcf9ce686",
+    "false_power.log": "eccbb6ccf7bded2d8ba23f1c2b78b146564a467b848e2c431a76d1dabd053a9c",
+    "leanchecker.log": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855",
+    "native.log": "8a0b9f79f3265724af58b27461627f9d532535f8a23681361da731c9ea37c101",
+    "sorry.log": "afc2bcbd48dbe1be41b06656bc3cbb8eb5b2fae535b72bca51dacfe3071fb469",
+    "version-preflight.log": "355a9a028f81641782d75d6e6b58dec70f29d2f61238a9e271690259d9bf5680",
+    "version.log": "355a9a028f81641782d75d6e6b58dec70f29d2f61238a9e271690259d9bf5680"
+  },
+  "manifest_sha256": "cb2b4870debf98cdf3663663797ccfc524e23d5f41f89e1c9ecdba5b6e680811",
+  "negative_controls": {
+    "custom_imported": "REJECTED_BY_AXIOM_GATE",
+    "false_fold": "REJECTED_BY_LEAN",
+    "false_power": "REJECTED_BY_LEAN",
+    "native": "REJECTED_BY_AXIOM_GATE",
+    "sorry": "REJECTED_BY_AXIOM_GATE"
+  },
+  "observations": {
+    "final": {
+      "dependency_revisions": {
+        "Cli": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
+        "LeanSearchClient": "ddf04cf3949fa556442341e87d47f9f6e6074707",
+        "Qq": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259",
+        "aesop": "355695d523e41d0554926416cba2a2b3544fbbc9",
+        "batteries": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
+        "importGraph": "e928b72544873815af278d38681b31c0293588e3",
+        "mathlib": "d13f23b723b8a846827a245b89c10fc7d3f11612",
+        "plausible": "118aa17ee84656b8bd727fef7c458ee8c833385c",
+        "proofwidgets": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5"
+      },
+      "dependency_worktrees": "CLEAN",
+      "lean_version": "Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)",
+      "manifest_sha256": "cb2b4870debf98cdf3663663797ccfc524e23d5f41f89e1c9ecdba5b6e680811"
+    },
+    "preflight": {
+      "dependency_revisions": {
+        "Cli": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
+        "LeanSearchClient": "ddf04cf3949fa556442341e87d47f9f6e6074707",
+        "Qq": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259",
+        "aesop": "355695d523e41d0554926416cba2a2b3544fbbc9",
+        "batteries": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
+        "importGraph": "e928b72544873815af278d38681b31c0293588e3",
+        "mathlib": "d13f23b723b8a846827a245b89c10fc7d3f11612",
+        "plausible": "118aa17ee84656b8bd727fef7c458ee8c833385c",
+        "proofwidgets": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5"
+      },
+      "dependency_worktrees": "CLEAN",
+      "lean_version": "Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)",
+      "manifest_sha256": "cb2b4870debf98cdf3663663797ccfc524e23d5f41f89e1c9ecdba5b6e680811"
+    }
+  },
+  "repository": null,
+  "schema_version": 1,
+  "scientific_effect": "NONE",
+  "workflow_run_attempt": null,
+  "workflow_run_id": null
+}
diff --git a/frontiers/determinant_moment_20261025/evidence/final/leanchecker.log b/frontiers/determinant_moment_20261025/evidence/final/leanchecker.log
new file mode 100644
index 000000000..e69de29bb
diff --git a/frontiers/determinant_moment_20261025/evidence/final/native.lean.txt b/frontiers/determinant_moment_20261025/evidence/final/native.lean.txt
new file mode 100644
index 000000000..65534e2f8
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/native.lean.txt
@@ -0,0 +1,3 @@
+import ResearchFormalCoreR1
+theorem injected : (2 : Nat) + 2 = 4 := by native_decide
+#print axioms injected
diff --git a/frontiers/determinant_moment_20261025/evidence/final/native.log b/frontiers/determinant_moment_20261025/evidence/final/native.log
new file mode 100644
index 000000000..a494e022b
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/native.log
@@ -0,0 +1 @@
+'injected' depends on axioms: [injected._native.native_decide.ax_1_1]
diff --git a/frontiers/determinant_moment_20261025/evidence/final/receipt.json b/frontiers/determinant_moment_20261025/evidence/final/receipt.json
new file mode 100644
index 000000000..a2d175bbd
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/receipt.json
@@ -0,0 +1,170 @@
+{
+  "alignment_status": "PENDING_INDEPENDENT_REVIEW",
+  "axioms": {
+    "ResearchFormalCoreR1.dm2_moment": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.dm2_negative_iff": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.dm2_pointwise": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.dm2_untyped": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.dm2_weight_measurable": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.ec005_fold_gap": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.ec008_factor_expansion": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.ec010_generic": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.ec010_transverse": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.ec011_scalar_cancellation": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.ec014_contact_power": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.p02_lm008_cross_multiplied": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.p02_lm008_quotient_bound": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.p02_lm008_r2_cancel": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.p02_lm009_bad_event_threshold": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.p02_lm009_palm_r4_to_r3": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.p02_lm009_power40_identity": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "ResearchFormalCoreR1.p02_lm009_r4_le_r3": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ]
+  },
+  "checked_commit": "dcfc89366f590342b4cd30b141a22c9ae2a562bb",
+  "dependency_revisions": {
+    "Cli": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
+    "LeanSearchClient": "ddf04cf3949fa556442341e87d47f9f6e6074707",
+    "Qq": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259",
+    "aesop": "355695d523e41d0554926416cba2a2b3544fbbc9",
+    "batteries": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
+    "importGraph": "e928b72544873815af278d38681b31c0293588e3",
+    "mathlib": "d13f23b723b8a846827a245b89c10fc7d3f11612",
+    "plausible": "118aa17ee84656b8bd727fef7c458ee8c833385c",
+    "proofwidgets": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5"
+  },
+  "dependency_worktrees": "CLEAN",
+  "formalization_status": "kernel-checked",
+  "lean_version": "Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)",
+  "logs": {
+    "axioms.log": "0fd7b72c24a218f67e7782091006440c909718fff19ca0bc112dd66bf66d91c6",
+    "build.log": "08961056e6112175d291708c2b3e99c13ff75fb1511e7d702a99a1552b625859",
+    "custom_imported.log": "6e7f917c7fe2fdc3efe1943dcc327c56acadd0b0ca96507a4327073fdfd2f083",
+    "elaborated-types.log": "f5b78a40cf0261ee5af6a9b18906c1c30d185fd186362d11cd13e87ee60e0a7f",
+    "false_fold.log": "0c0d91c62fbbdeed9ac1f8b968f9d73b701b8079089bd90c07c0af6fcf9ce686",
+    "false_power.log": "eccbb6ccf7bded2d8ba23f1c2b78b146564a467b848e2c431a76d1dabd053a9c",
+    "leanchecker.log": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855",
+    "native.log": "8a0b9f79f3265724af58b27461627f9d532535f8a23681361da731c9ea37c101",
+    "sorry.log": "afc2bcbd48dbe1be41b06656bc3cbb8eb5b2fae535b72bca51dacfe3071fb469",
+    "version-preflight.log": "355a9a028f81641782d75d6e6b58dec70f29d2f61238a9e271690259d9bf5680",
+    "version.log": "355a9a028f81641782d75d6e6b58dec70f29d2f61238a9e271690259d9bf5680"
+  },
+  "manifest_sha256": "cb2b4870debf98cdf3663663797ccfc524e23d5f41f89e1c9ecdba5b6e680811",
+  "negative_controls": {
+    "custom_imported": "REJECTED_BY_AXIOM_GATE",
+    "false_fold": "REJECTED_BY_LEAN",
+    "false_power": "REJECTED_BY_LEAN",
+    "native": "REJECTED_BY_AXIOM_GATE",
+    "sorry": "REJECTED_BY_AXIOM_GATE"
+  },
+  "observations": {
+    "final": {
+      "dependency_revisions": {
+        "Cli": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
+        "LeanSearchClient": "ddf04cf3949fa556442341e87d47f9f6e6074707",
+        "Qq": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259",
+        "aesop": "355695d523e41d0554926416cba2a2b3544fbbc9",
+        "batteries": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
+        "importGraph": "e928b72544873815af278d38681b31c0293588e3",
+        "mathlib": "d13f23b723b8a846827a245b89c10fc7d3f11612",
+        "plausible": "118aa17ee84656b8bd727fef7c458ee8c833385c",
+        "proofwidgets": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5"
+      },
+      "dependency_worktrees": "CLEAN",
+      "lean_version": "Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)",
+      "manifest_sha256": "cb2b4870debf98cdf3663663797ccfc524e23d5f41f89e1c9ecdba5b6e680811"
+    },
+    "preflight": {
+      "dependency_revisions": {
+        "Cli": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
+        "LeanSearchClient": "ddf04cf3949fa556442341e87d47f9f6e6074707",
+        "Qq": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259",
+        "aesop": "355695d523e41d0554926416cba2a2b3544fbbc9",
+        "batteries": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
+        "importGraph": "e928b72544873815af278d38681b31c0293588e3",
+        "mathlib": "d13f23b723b8a846827a245b89c10fc7d3f11612",
+        "plausible": "118aa17ee84656b8bd727fef7c458ee8c833385c",
+        "proofwidgets": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5"
+      },
+      "dependency_worktrees": "CLEAN",
+      "lean_version": "Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)",
+      "manifest_sha256": "cb2b4870debf98cdf3663663797ccfc524e23d5f41f89e1c9ecdba5b6e680811"
+    }
+  },
+  "repository": null,
+  "schema_version": 1,
+  "scientific_effect": "NONE",
+  "workflow_run_attempt": null,
+  "workflow_run_id": null
+}
diff --git a/frontiers/determinant_moment_20261025/evidence/final/sorry.lean.txt b/frontiers/determinant_moment_20261025/evidence/final/sorry.lean.txt
new file mode 100644
index 000000000..ace09ca23
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/sorry.lean.txt
@@ -0,0 +1,3 @@
+import ResearchFormalCoreR1
+theorem injected : False := by sorry
+#print axioms injected
diff --git a/frontiers/determinant_moment_20261025/evidence/final/sorry.log b/frontiers/determinant_moment_20261025/evidence/final/sorry.log
new file mode 100644
index 000000000..e34e95e9e
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/sorry.log
@@ -0,0 +1,2 @@
+/workspace/Math-/frontiers/determinant_moment_20261025/.lake/formal-evidence/sorry.lean:2:8: warning: declaration uses `sorry`
+'injected' depends on axioms: [sorryAx]
diff --git a/frontiers/determinant_moment_20261025/evidence/final/tests-normal.log b/frontiers/determinant_moment_20261025/evidence/final/tests-normal.log
new file mode 100644
index 000000000..8ab85e0ff
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/tests-normal.log
@@ -0,0 +1,83 @@
+test_blank_or_nonstring_proposer_identity (test_alignment_lineage.AlignmentLineageTests.test_blank_or_nonstring_proposer_identity) ... ok
+test_disposition_only_edit_cannot_hide_unknown_proposer (test_alignment_lineage.AlignmentLineageTests.test_disposition_only_edit_cannot_hide_unknown_proposer) ... ok
+test_every_declared_proposer_is_checked (test_alignment_lineage.AlignmentLineageTests.test_every_declared_proposer_is_checked) ... ok
+test_existing_digest_scope_and_coverage_checks (test_alignment_lineage.AlignmentLineageTests.test_existing_digest_scope_and_coverage_checks) ... ok
+test_explicit_empty_proposer_list (test_alignment_lineage.AlignmentLineageTests.test_explicit_empty_proposer_list) ... ok
+test_input_not_mutated (test_alignment_lineage.AlignmentLineageTests.test_input_not_mutated) ... ok
+test_invalid_proposer_target_scope (test_alignment_lineage.AlignmentLineageTests.test_invalid_proposer_target_scope) ... ok
+test_known_distinct_proposer (test_alignment_lineage.AlignmentLineageTests.test_known_distinct_proposer) ... ok
+test_legacy_single_author_record (test_alignment_lineage.AlignmentLineageTests.test_legacy_single_author_record) ... ok
+test_lineage_scope_cannot_be_unbound (test_alignment_lineage.AlignmentLineageTests.test_lineage_scope_cannot_be_unbound) ... ok
+test_lineage_tests_cannot_be_unbound (test_alignment_lineage.AlignmentLineageTests.test_lineage_tests_cannot_be_unbound) ... ok
+test_malformed_primary_and_reviewer_objects (test_alignment_lineage.AlignmentLineageTests.test_malformed_primary_and_reviewer_objects) ... ok
+test_malformed_proposer_collection (test_alignment_lineage.AlignmentLineageTests.test_malformed_proposer_collection) ... ok
+test_malformed_proposer_object (test_alignment_lineage.AlignmentLineageTests.test_malformed_proposer_object) ... ok
+test_missing_proposer_identity_field (test_alignment_lineage.AlignmentLineageTests.test_missing_proposer_identity_field) ... ok
+test_placeholder_lineage_in_all_roles (test_alignment_lineage.AlignmentLineageTests.test_placeholder_lineage_in_all_roles) ... ok
+test_primary_identity_normalization (test_alignment_lineage.AlignmentLineageTests.test_primary_identity_normalization) ... ok
+test_proposer_identity_normalization (test_alignment_lineage.AlignmentLineageTests.test_proposer_identity_normalization) ... ok
+test_same_proposer_agent (test_alignment_lineage.AlignmentLineageTests.test_same_proposer_agent) ... ok
+test_same_proposer_family (test_alignment_lineage.AlignmentLineageTests.test_same_proposer_family) ... ok
+test_same_proposer_provider (test_alignment_lineage.AlignmentLineageTests.test_same_proposer_provider) ... ok
+test_unscoped_known_proposer (test_alignment_lineage.AlignmentLineageTests.test_unscoped_known_proposer) ... ok
+test_withheld_record_remains_rejected (test_alignment_lineage.AlignmentLineageTests.test_withheld_record_remains_rejected) ... ok
+test_empty_link (test_gate.BlueprintTests.test_empty_link) ... ok
+test_unsupported_leanok (test_gate.BlueprintTests.test_unsupported_leanok) ... ok
+test_valid_link (test_gate.BlueprintTests.test_valid_link) ... ok
+test_wrong_link (test_gate.BlueprintTests.test_wrong_link) ... ok
+test_axiom_free (test_gate.GateTests.test_axiom_free) ... ok
+test_custom (test_gate.GateTests.test_custom) ... ok
+test_duplicate_target_output (test_gate.GateTests.test_duplicate_target_output) ... ok
+test_duplicate_target_request (test_gate.GateTests.test_duplicate_target_request) ... ok
+test_manifest_absolute (test_gate.GateTests.test_manifest_absolute) ... ok
+test_manifest_content (test_gate.GateTests.test_manifest_content) ... ok
+test_manifest_empty (test_gate.GateTests.test_manifest_empty) ... ok
+test_manifest_escape (test_gate.GateTests.test_manifest_escape) ... ok
+test_manifest_missing (test_gate.GateTests.test_manifest_missing) ... ok
+test_manifest_symlink (test_gate.GateTests.test_manifest_symlink) ... ok
+test_manifest_tamper (test_gate.GateTests.test_manifest_tamper) ... ok
+test_missing_target (test_gate.GateTests.test_missing_target) ... ok
+test_multiline (test_gate.GateTests.test_multiline) ... ok
+test_native (test_gate.GateTests.test_native) ... ok
+test_noise_denied (test_gate.GateTests.test_noise_denied) ... ok
+test_review_bad_disposition (test_gate.GateTests.test_review_bad_disposition) ... ok
+test_review_bad_evidence (test_gate.GateTests.test_review_bad_evidence) ... ok
+test_review_changed_scope (test_gate.GateTests.test_review_changed_scope) ... ok
+test_review_partial (test_gate.GateTests.test_review_partial) ... ok
+test_review_same_provider (test_gate.GateTests.test_review_same_provider) ... ok
+test_review_self (test_gate.GateTests.test_review_self) ... ok
+test_review_stale (test_gate.GateTests.test_review_stale) ... ok
+test_review_valid (test_gate.GateTests.test_review_valid) ... ok
+test_sorry (test_gate.GateTests.test_sorry) ... ok
+test_standard_axioms (test_gate.GateTests.test_standard_axioms) ... ok
+test_unexpected_target (test_gate.GateTests.test_unexpected_target) ... ok
+test_dependency_dirtied_during_execution_refuses_receipt (test_gate.RuntimeGuardTests.test_dependency_dirtied_during_execution_refuses_receipt) ... ok
+test_dependency_moved_during_execution_refuses_receipt (test_gate.RuntimeGuardTests.test_dependency_moved_during_execution_refuses_receipt) ... ok
+test_dirty_dependency_before_execution_refuses_and_preserves_build (test_gate.RuntimeGuardTests.test_dirty_dependency_before_execution_refuses_and_preserves_build) ... ok
+test_receipt_binds_attempt_and_both_equal_observations (test_gate.RuntimeGuardTests.test_receipt_binds_attempt_and_both_equal_observations) ... ok
+test_runtime_changed_between_observations_refuses_receipt (test_gate.RuntimeGuardTests.test_runtime_changed_between_observations_refuses_receipt) ... ok
+test_wrong_dependency_before_execution_refuses_and_preserves_build (test_gate.RuntimeGuardTests.test_wrong_dependency_before_execution_refuses_and_preserves_build) ... ok
+test_complete_pinned_release_record (test_gate.RuntimeVersionTests.test_complete_pinned_release_record) ... ok
+test_installed_dependency_change_still_refuses_receipt (test_gate.RuntimeVersionTests.test_installed_dependency_change_still_refuses_receipt) ... ok
+test_invalid_preflight_preserves_build_and_runs_no_build (test_gate.RuntimeVersionTests.test_invalid_preflight_preserves_build_and_runs_no_build) ... ok
+test_other_commit_after_execution_refuses_receipt (test_gate.RuntimeVersionTests.test_other_commit_after_execution_refuses_receipt) ... ok
+test_other_commit_preflight_preserves_build (test_gate.RuntimeVersionTests.test_other_commit_preflight_preserves_build) ... ok
+test_other_versions_and_incomplete_or_extra_records_refused (test_gate.RuntimeVersionTests.test_other_versions_and_incomplete_or_extra_records_refused) ... ok
+test_preflight_process_failure_preserves_build (test_gate.RuntimeVersionTests.test_preflight_process_failure_preserves_build) ... ok
+test_short_and_other_release_commits_refused (test_gate.RuntimeVersionTests.test_short_and_other_release_commits_refused) ... ok
+test_source_change_during_build_still_refuses_receipt (test_gate.RuntimeVersionTests.test_source_change_during_build_still_refuses_receipt) ... ok
+test_success_checks_before_build_and_after_controls_and_binds_both_logs (test_gate.RuntimeVersionTests.test_success_checks_before_build_and_after_controls_and_binds_both_logs) ... ok
+test_version_change_after_execution_refuses_receipt (test_gate.RuntimeVersionTests.test_version_change_after_execution_refuses_receipt) ... ok
+test_duplicate_json_rejected (test_gate.SourceContractTests.test_duplicate_json_rejected) ... ok
+test_json_object (test_gate.SourceContractTests.test_json_object) ... ok
+test_manifest_cannot_claim_kernel_status (test_gate.SourceContractTests.test_manifest_cannot_claim_kernel_status) ... ok
+test_root_declaration_cannot_evade_audit (test_gate.SourceContractTests.test_root_declaration_cannot_evade_audit) ... ok
+test_source_baseline (test_gate.SourceContractTests.test_source_baseline) ... ok
+test_unbound_gate_refused (test_gate.SourceContractTests.test_unbound_gate_refused) ... ok
+test_only_documented_algebra_repairs (test_gate.SuccessorTests.test_only_documented_algebra_repairs) ... ok
+test_only_documented_probability_repair (test_gate.SuccessorTests.test_only_documented_probability_repair) ... ok
+
+----------------------------------------------------------------------
+Ran 78 tests in 0.195s
+
+OK
diff --git a/frontiers/determinant_moment_20261025/evidence/final/tests-optimized.log b/frontiers/determinant_moment_20261025/evidence/final/tests-optimized.log
new file mode 100644
index 000000000..1feb0c9da
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/tests-optimized.log
@@ -0,0 +1,83 @@
+test_blank_or_nonstring_proposer_identity (test_alignment_lineage.AlignmentLineageTests.test_blank_or_nonstring_proposer_identity) ... ok
+test_disposition_only_edit_cannot_hide_unknown_proposer (test_alignment_lineage.AlignmentLineageTests.test_disposition_only_edit_cannot_hide_unknown_proposer) ... ok
+test_every_declared_proposer_is_checked (test_alignment_lineage.AlignmentLineageTests.test_every_declared_proposer_is_checked) ... ok
+test_existing_digest_scope_and_coverage_checks (test_alignment_lineage.AlignmentLineageTests.test_existing_digest_scope_and_coverage_checks) ... ok
+test_explicit_empty_proposer_list (test_alignment_lineage.AlignmentLineageTests.test_explicit_empty_proposer_list) ... ok
+test_input_not_mutated (test_alignment_lineage.AlignmentLineageTests.test_input_not_mutated) ... ok
+test_invalid_proposer_target_scope (test_alignment_lineage.AlignmentLineageTests.test_invalid_proposer_target_scope) ... ok
+test_known_distinct_proposer (test_alignment_lineage.AlignmentLineageTests.test_known_distinct_proposer) ... ok
+test_legacy_single_author_record (test_alignment_lineage.AlignmentLineageTests.test_legacy_single_author_record) ... ok
+test_lineage_scope_cannot_be_unbound (test_alignment_lineage.AlignmentLineageTests.test_lineage_scope_cannot_be_unbound) ... ok
+test_lineage_tests_cannot_be_unbound (test_alignment_lineage.AlignmentLineageTests.test_lineage_tests_cannot_be_unbound) ... ok
+test_malformed_primary_and_reviewer_objects (test_alignment_lineage.AlignmentLineageTests.test_malformed_primary_and_reviewer_objects) ... ok
+test_malformed_proposer_collection (test_alignment_lineage.AlignmentLineageTests.test_malformed_proposer_collection) ... ok
+test_malformed_proposer_object (test_alignment_lineage.AlignmentLineageTests.test_malformed_proposer_object) ... ok
+test_missing_proposer_identity_field (test_alignment_lineage.AlignmentLineageTests.test_missing_proposer_identity_field) ... ok
+test_placeholder_lineage_in_all_roles (test_alignment_lineage.AlignmentLineageTests.test_placeholder_lineage_in_all_roles) ... ok
+test_primary_identity_normalization (test_alignment_lineage.AlignmentLineageTests.test_primary_identity_normalization) ... ok
+test_proposer_identity_normalization (test_alignment_lineage.AlignmentLineageTests.test_proposer_identity_normalization) ... ok
+test_same_proposer_agent (test_alignment_lineage.AlignmentLineageTests.test_same_proposer_agent) ... ok
+test_same_proposer_family (test_alignment_lineage.AlignmentLineageTests.test_same_proposer_family) ... ok
+test_same_proposer_provider (test_alignment_lineage.AlignmentLineageTests.test_same_proposer_provider) ... ok
+test_unscoped_known_proposer (test_alignment_lineage.AlignmentLineageTests.test_unscoped_known_proposer) ... ok
+test_withheld_record_remains_rejected (test_alignment_lineage.AlignmentLineageTests.test_withheld_record_remains_rejected) ... ok
+test_empty_link (test_gate.BlueprintTests.test_empty_link) ... ok
+test_unsupported_leanok (test_gate.BlueprintTests.test_unsupported_leanok) ... ok
+test_valid_link (test_gate.BlueprintTests.test_valid_link) ... ok
+test_wrong_link (test_gate.BlueprintTests.test_wrong_link) ... ok
+test_axiom_free (test_gate.GateTests.test_axiom_free) ... ok
+test_custom (test_gate.GateTests.test_custom) ... ok
+test_duplicate_target_output (test_gate.GateTests.test_duplicate_target_output) ... ok
+test_duplicate_target_request (test_gate.GateTests.test_duplicate_target_request) ... ok
+test_manifest_absolute (test_gate.GateTests.test_manifest_absolute) ... ok
+test_manifest_content (test_gate.GateTests.test_manifest_content) ... ok
+test_manifest_empty (test_gate.GateTests.test_manifest_empty) ... ok
+test_manifest_escape (test_gate.GateTests.test_manifest_escape) ... ok
+test_manifest_missing (test_gate.GateTests.test_manifest_missing) ... ok
+test_manifest_symlink (test_gate.GateTests.test_manifest_symlink) ... ok
+test_manifest_tamper (test_gate.GateTests.test_manifest_tamper) ... ok
+test_missing_target (test_gate.GateTests.test_missing_target) ... ok
+test_multiline (test_gate.GateTests.test_multiline) ... ok
+test_native (test_gate.GateTests.test_native) ... ok
+test_noise_denied (test_gate.GateTests.test_noise_denied) ... ok
+test_review_bad_disposition (test_gate.GateTests.test_review_bad_disposition) ... ok
+test_review_bad_evidence (test_gate.GateTests.test_review_bad_evidence) ... ok
+test_review_changed_scope (test_gate.GateTests.test_review_changed_scope) ... ok
+test_review_partial (test_gate.GateTests.test_review_partial) ... ok
+test_review_same_provider (test_gate.GateTests.test_review_same_provider) ... ok
+test_review_self (test_gate.GateTests.test_review_self) ... ok
+test_review_stale (test_gate.GateTests.test_review_stale) ... ok
+test_review_valid (test_gate.GateTests.test_review_valid) ... ok
+test_sorry (test_gate.GateTests.test_sorry) ... ok
+test_standard_axioms (test_gate.GateTests.test_standard_axioms) ... ok
+test_unexpected_target (test_gate.GateTests.test_unexpected_target) ... ok
+test_dependency_dirtied_during_execution_refuses_receipt (test_gate.RuntimeGuardTests.test_dependency_dirtied_during_execution_refuses_receipt) ... ok
+test_dependency_moved_during_execution_refuses_receipt (test_gate.RuntimeGuardTests.test_dependency_moved_during_execution_refuses_receipt) ... ok
+test_dirty_dependency_before_execution_refuses_and_preserves_build (test_gate.RuntimeGuardTests.test_dirty_dependency_before_execution_refuses_and_preserves_build) ... ok
+test_receipt_binds_attempt_and_both_equal_observations (test_gate.RuntimeGuardTests.test_receipt_binds_attempt_and_both_equal_observations) ... ok
+test_runtime_changed_between_observations_refuses_receipt (test_gate.RuntimeGuardTests.test_runtime_changed_between_observations_refuses_receipt) ... ok
+test_wrong_dependency_before_execution_refuses_and_preserves_build (test_gate.RuntimeGuardTests.test_wrong_dependency_before_execution_refuses_and_preserves_build) ... ok
+test_complete_pinned_release_record (test_gate.RuntimeVersionTests.test_complete_pinned_release_record) ... ok
+test_installed_dependency_change_still_refuses_receipt (test_gate.RuntimeVersionTests.test_installed_dependency_change_still_refuses_receipt) ... ok
+test_invalid_preflight_preserves_build_and_runs_no_build (test_gate.RuntimeVersionTests.test_invalid_preflight_preserves_build_and_runs_no_build) ... ok
+test_other_commit_after_execution_refuses_receipt (test_gate.RuntimeVersionTests.test_other_commit_after_execution_refuses_receipt) ... ok
+test_other_commit_preflight_preserves_build (test_gate.RuntimeVersionTests.test_other_commit_preflight_preserves_build) ... ok
+test_other_versions_and_incomplete_or_extra_records_refused (test_gate.RuntimeVersionTests.test_other_versions_and_incomplete_or_extra_records_refused) ... ok
+test_preflight_process_failure_preserves_build (test_gate.RuntimeVersionTests.test_preflight_process_failure_preserves_build) ... ok
+test_short_and_other_release_commits_refused (test_gate.RuntimeVersionTests.test_short_and_other_release_commits_refused) ... ok
+test_source_change_during_build_still_refuses_receipt (test_gate.RuntimeVersionTests.test_source_change_during_build_still_refuses_receipt) ... ok
+test_success_checks_before_build_and_after_controls_and_binds_both_logs (test_gate.RuntimeVersionTests.test_success_checks_before_build_and_after_controls_and_binds_both_logs) ... ok
+test_version_change_after_execution_refuses_receipt (test_gate.RuntimeVersionTests.test_version_change_after_execution_refuses_receipt) ... ok
+test_duplicate_json_rejected (test_gate.SourceContractTests.test_duplicate_json_rejected) ... ok
+test_json_object (test_gate.SourceContractTests.test_json_object) ... ok
+test_manifest_cannot_claim_kernel_status (test_gate.SourceContractTests.test_manifest_cannot_claim_kernel_status) ... ok
+test_root_declaration_cannot_evade_audit (test_gate.SourceContractTests.test_root_declaration_cannot_evade_audit) ... ok
+test_source_baseline (test_gate.SourceContractTests.test_source_baseline) ... ok
+test_unbound_gate_refused (test_gate.SourceContractTests.test_unbound_gate_refused) ... ok
+test_only_documented_algebra_repairs (test_gate.SuccessorTests.test_only_documented_algebra_repairs) ... ok
+test_only_documented_probability_repair (test_gate.SuccessorTests.test_only_documented_probability_repair) ... ok
+
+----------------------------------------------------------------------
+Ran 78 tests in 0.186s
+
+OK
diff --git a/frontiers/determinant_moment_20261025/evidence/final/version-preflight.log b/frontiers/determinant_moment_20261025/evidence/final/version-preflight.log
new file mode 100644
index 000000000..3bdff924e
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/version-preflight.log
@@ -0,0 +1 @@
+Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)
diff --git a/frontiers/determinant_moment_20261025/evidence/final/version.log b/frontiers/determinant_moment_20261025/evidence/final/version.log
new file mode 100644
index 000000000..3bdff924e
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/final/version.log
@@ -0,0 +1 @@
+Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)
diff --git a/frontiers/determinant_moment_20261025/evidence/history/dm2-baseline-tests.log b/frontiers/determinant_moment_20261025/evidence/history/dm2-baseline-tests.log
new file mode 100644
index 000000000..5b86c7362
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/history/dm2-baseline-tests.log
@@ -0,0 +1,83 @@
+test_blank_or_nonstring_proposer_identity (test_alignment_lineage.AlignmentLineageTests.test_blank_or_nonstring_proposer_identity) ... ok
+test_disposition_only_edit_cannot_hide_unknown_proposer (test_alignment_lineage.AlignmentLineageTests.test_disposition_only_edit_cannot_hide_unknown_proposer) ... ok
+test_every_declared_proposer_is_checked (test_alignment_lineage.AlignmentLineageTests.test_every_declared_proposer_is_checked) ... ok
+test_existing_digest_scope_and_coverage_checks (test_alignment_lineage.AlignmentLineageTests.test_existing_digest_scope_and_coverage_checks) ... ok
+test_explicit_empty_proposer_list (test_alignment_lineage.AlignmentLineageTests.test_explicit_empty_proposer_list) ... ok
+test_input_not_mutated (test_alignment_lineage.AlignmentLineageTests.test_input_not_mutated) ... ok
+test_invalid_proposer_target_scope (test_alignment_lineage.AlignmentLineageTests.test_invalid_proposer_target_scope) ... ok
+test_known_distinct_proposer (test_alignment_lineage.AlignmentLineageTests.test_known_distinct_proposer) ... ok
+test_legacy_single_author_record (test_alignment_lineage.AlignmentLineageTests.test_legacy_single_author_record) ... ok
+test_lineage_scope_cannot_be_unbound (test_alignment_lineage.AlignmentLineageTests.test_lineage_scope_cannot_be_unbound) ... ok
+test_lineage_tests_cannot_be_unbound (test_alignment_lineage.AlignmentLineageTests.test_lineage_tests_cannot_be_unbound) ... ok
+test_malformed_primary_and_reviewer_objects (test_alignment_lineage.AlignmentLineageTests.test_malformed_primary_and_reviewer_objects) ... ok
+test_malformed_proposer_collection (test_alignment_lineage.AlignmentLineageTests.test_malformed_proposer_collection) ... ok
+test_malformed_proposer_object (test_alignment_lineage.AlignmentLineageTests.test_malformed_proposer_object) ... ok
+test_missing_proposer_identity_field (test_alignment_lineage.AlignmentLineageTests.test_missing_proposer_identity_field) ... ok
+test_placeholder_lineage_in_all_roles (test_alignment_lineage.AlignmentLineageTests.test_placeholder_lineage_in_all_roles) ... ok
+test_primary_identity_normalization (test_alignment_lineage.AlignmentLineageTests.test_primary_identity_normalization) ... ok
+test_proposer_identity_normalization (test_alignment_lineage.AlignmentLineageTests.test_proposer_identity_normalization) ... ok
+test_same_proposer_agent (test_alignment_lineage.AlignmentLineageTests.test_same_proposer_agent) ... ok
+test_same_proposer_family (test_alignment_lineage.AlignmentLineageTests.test_same_proposer_family) ... ok
+test_same_proposer_provider (test_alignment_lineage.AlignmentLineageTests.test_same_proposer_provider) ... ok
+test_unscoped_known_proposer (test_alignment_lineage.AlignmentLineageTests.test_unscoped_known_proposer) ... ok
+test_withheld_record_remains_rejected (test_alignment_lineage.AlignmentLineageTests.test_withheld_record_remains_rejected) ... ok
+test_empty_link (test_gate.BlueprintTests.test_empty_link) ... ok
+test_unsupported_leanok (test_gate.BlueprintTests.test_unsupported_leanok) ... ok
+test_valid_link (test_gate.BlueprintTests.test_valid_link) ... ok
+test_wrong_link (test_gate.BlueprintTests.test_wrong_link) ... ok
+test_axiom_free (test_gate.GateTests.test_axiom_free) ... ok
+test_custom (test_gate.GateTests.test_custom) ... ok
+test_duplicate_target_output (test_gate.GateTests.test_duplicate_target_output) ... ok
+test_duplicate_target_request (test_gate.GateTests.test_duplicate_target_request) ... ok
+test_manifest_absolute (test_gate.GateTests.test_manifest_absolute) ... ok
+test_manifest_content (test_gate.GateTests.test_manifest_content) ... ok
+test_manifest_empty (test_gate.GateTests.test_manifest_empty) ... ok
+test_manifest_escape (test_gate.GateTests.test_manifest_escape) ... ok
+test_manifest_missing (test_gate.GateTests.test_manifest_missing) ... ok
+test_manifest_symlink (test_gate.GateTests.test_manifest_symlink) ... ok
+test_manifest_tamper (test_gate.GateTests.test_manifest_tamper) ... ok
+test_missing_target (test_gate.GateTests.test_missing_target) ... ok
+test_multiline (test_gate.GateTests.test_multiline) ... ok
+test_native (test_gate.GateTests.test_native) ... ok
+test_noise_denied (test_gate.GateTests.test_noise_denied) ... ok
+test_review_bad_disposition (test_gate.GateTests.test_review_bad_disposition) ... ok
+test_review_bad_evidence (test_gate.GateTests.test_review_bad_evidence) ... ok
+test_review_changed_scope (test_gate.GateTests.test_review_changed_scope) ... ok
+test_review_partial (test_gate.GateTests.test_review_partial) ... ok
+test_review_same_provider (test_gate.GateTests.test_review_same_provider) ... ok
+test_review_self (test_gate.GateTests.test_review_self) ... ok
+test_review_stale (test_gate.GateTests.test_review_stale) ... ok
+test_review_valid (test_gate.GateTests.test_review_valid) ... ok
+test_sorry (test_gate.GateTests.test_sorry) ... ok
+test_standard_axioms (test_gate.GateTests.test_standard_axioms) ... ok
+test_unexpected_target (test_gate.GateTests.test_unexpected_target) ... ok
+test_dependency_dirtied_during_execution_refuses_receipt (test_gate.RuntimeGuardTests.test_dependency_dirtied_during_execution_refuses_receipt) ... ok
+test_dependency_moved_during_execution_refuses_receipt (test_gate.RuntimeGuardTests.test_dependency_moved_during_execution_refuses_receipt) ... ok
+test_dirty_dependency_before_execution_refuses_and_preserves_build (test_gate.RuntimeGuardTests.test_dirty_dependency_before_execution_refuses_and_preserves_build) ... ok
+test_receipt_binds_attempt_and_both_equal_observations (test_gate.RuntimeGuardTests.test_receipt_binds_attempt_and_both_equal_observations) ... ok
+test_runtime_changed_between_observations_refuses_receipt (test_gate.RuntimeGuardTests.test_runtime_changed_between_observations_refuses_receipt) ... ok
+test_wrong_dependency_before_execution_refuses_and_preserves_build (test_gate.RuntimeGuardTests.test_wrong_dependency_before_execution_refuses_and_preserves_build) ... ok
+test_complete_pinned_release_record (test_gate.RuntimeVersionTests.test_complete_pinned_release_record) ... ok
+test_installed_dependency_change_still_refuses_receipt (test_gate.RuntimeVersionTests.test_installed_dependency_change_still_refuses_receipt) ... ok
+test_invalid_preflight_preserves_build_and_runs_no_build (test_gate.RuntimeVersionTests.test_invalid_preflight_preserves_build_and_runs_no_build) ... ok
+test_other_commit_after_execution_refuses_receipt (test_gate.RuntimeVersionTests.test_other_commit_after_execution_refuses_receipt) ... ok
+test_other_commit_preflight_preserves_build (test_gate.RuntimeVersionTests.test_other_commit_preflight_preserves_build) ... ok
+test_other_versions_and_incomplete_or_extra_records_refused (test_gate.RuntimeVersionTests.test_other_versions_and_incomplete_or_extra_records_refused) ... ok
+test_preflight_process_failure_preserves_build (test_gate.RuntimeVersionTests.test_preflight_process_failure_preserves_build) ... ok
+test_short_and_other_release_commits_refused (test_gate.RuntimeVersionTests.test_short_and_other_release_commits_refused) ... ok
+test_source_change_during_build_still_refuses_receipt (test_gate.RuntimeVersionTests.test_source_change_during_build_still_refuses_receipt) ... ok
+test_success_checks_before_build_and_after_controls_and_binds_both_logs (test_gate.RuntimeVersionTests.test_success_checks_before_build_and_after_controls_and_binds_both_logs) ... ok
+test_version_change_after_execution_refuses_receipt (test_gate.RuntimeVersionTests.test_version_change_after_execution_refuses_receipt) ... ok
+test_duplicate_json_rejected (test_gate.SourceContractTests.test_duplicate_json_rejected) ... ok
+test_json_object (test_gate.SourceContractTests.test_json_object) ... ok
+test_manifest_cannot_claim_kernel_status (test_gate.SourceContractTests.test_manifest_cannot_claim_kernel_status) ... ok
+test_root_declaration_cannot_evade_audit (test_gate.SourceContractTests.test_root_declaration_cannot_evade_audit) ... ok
+test_source_baseline (test_gate.SourceContractTests.test_source_baseline) ... ok
+test_unbound_gate_refused (test_gate.SourceContractTests.test_unbound_gate_refused) ... ok
+test_only_documented_algebra_repairs (test_gate.SuccessorTests.test_only_documented_algebra_repairs) ... ok
+test_only_documented_probability_repair (test_gate.SuccessorTests.test_only_documented_probability_repair) ... ok
+
+----------------------------------------------------------------------
+Ran 78 tests in 0.142s
+
+OK
diff --git a/frontiers/determinant_moment_20261025/evidence/history/dm2-compile-01.log b/frontiers/determinant_moment_20261025/evidence/history/dm2-compile-01.log
new file mode 100644
index 000000000..67c1077e1
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/history/dm2-compile-01.log
@@ -0,0 +1 @@
+ResearchFormalCoreR1/DeterminantMoment.lean:1:0: error: object file '/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/batteries/.lake/build/lib/lean/Batteries/CodeAction.olean' of module Batteries.CodeAction does not exist
diff --git a/frontiers/determinant_moment_20261025/evidence/history/dm2-compile-02.log b/frontiers/determinant_moment_20261025/evidence/history/dm2-compile-02.log
new file mode 100644
index 000000000..e0c6365f4
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/history/dm2-compile-02.log
@@ -0,0 +1,214 @@
+ResearchFormalCoreR1/DeterminantMoment.lean:14:4: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Real.instDivInvMonoid', which is 'noncomputable'
+ResearchFormalCoreR1/DeterminantMoment.lean:18:4: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Real.instDivInvMonoid', which is 'noncomputable'
+ResearchFormalCoreR1/DeterminantMoment.lean:27:2: error(lean.synthInstanceFailed): failed to synthesize instance of type class
+  Decidable (dm2Negative (dm2HM r j) ∧ (dm2HS r j).det < 0)
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+ResearchFormalCoreR1/DeterminantMoment.lean:66:8: error: linarith failed to find a contradiction
+r : ℝ
+j : DM2Jet
+hr : 0 < r
+hr1 : r ≤ 1
+R : ℝ := dm2Radius j
+hR : 0 ≤ R
+hsum : ∑ i, |j i| = |j 0| + |j 1| + |j 2| + |j 3| + |j 4| + |j 5| + |j 6| + |j 7| + |j 8|
+hbudget : 1 + |j 0| + |j 1| + |j 2| + |j 4| + |j 5| + |j 6| ≤ R
+hscale : ∀ (i : Fin 9), |r * j i| ≤ |j i|
+hscale2 : ∀ (i : Fin 9), |r ^ 2 * j i| ≤ |j i|
+this : |-1 + r * j 4 / 12| ≤ 1 + |r| * |j 4| / 12
+a✝ : 1 + |j 4| < |-1 + r * j 4 / 12|
+⊢ False
+failed
+ResearchFormalCoreR1/DeterminantMoment.lean:72:4: error: linarith failed to find a contradiction
+r : ℝ
+j : DM2Jet
+hr : 0 < r
+hr1 : r ≤ 1
+R : ℝ := dm2Radius j
+hR : 0 ≤ R
+hsum : ∑ i, |j i| = |j 0| + |j 1| + |j 2| + |j 3| + |j 4| + |j 5| + |j 6| + |j 7| + |j 8|
+hbudget : 1 + |j 0| + |j 1| + |j 2| + |j 4| + |j 5| + |j 6| ≤ R
+hscale : ∀ (i : Fin 9), |r * j i| ≤ |j i|
+hscale2 : ∀ (i : Fin 9), |r ^ 2 * j i| ≤ |j i|
+haM : |-1 + r * j 4 / 12| ≤ R
+this : |1 + r * j 4 / 12| ≤ 1 + |r| * |j 4| / 12
+a✝ : R < |1 + r * j 4 / 12|
+⊢ False
+failed
+ResearchFormalCoreR1/DeterminantMoment.lean:77:4: error: linarith failed to find a contradiction
+r : ℝ
+j : DM2Jet
+hr : 0 < r
+hr1 : r ≤ 1
+R : ℝ := dm2Radius j
+hR : 0 ≤ R
+hsum : ∑ i, |j i| = |j 0| + |j 1| + |j 2| + |j 3| + |j 4| + |j 5| + |j 6| + |j 7| + |j 8|
+hbudget : 1 + |j 0| + |j 1| + |j 2| + |j 4| + |j 5| + |j 6| ≤ R
+hscale : ∀ (i : Fin 9), |r * j i| ≤ |j i|
+hscale2 : ∀ (i : Fin 9), |r ^ 2 * j i| ≤ |j i|
+haM : |-1 + r * j 4 / 12| ≤ R
+haS : |1 + r * j 4 / 12| ≤ R
+this : |-j 1 / 2 + r * j 5 / 12| ≤ |j 1| / 2 + |r| * |j 5| / 12
+a✝ : R < |-j 1 / 2 + r * j 5 / 12|
+⊢ False
+failed
+ResearchFormalCoreR1/DeterminantMoment.lean:82:4: error: linarith failed to find a contradiction
+r : ℝ
+j : DM2Jet
+hr : 0 < r
+hr1 : r ≤ 1
+R : ℝ := dm2Radius j
+hR : 0 ≤ R
+hsum : ∑ i, |j i| = |j 0| + |j 1| + |j 2| + |j 3| + |j 4| + |j 5| + |j 6| + |j 7| + |j 8|
+hbudget : 1 + |j 0| + |j 1| + |j 2| + |j 4| + |j 5| + |j 6| ≤ R
+hscale : ∀ (i : Fin 9), |r * j i| ≤ |j i|
+hscale2 : ∀ (i : Fin 9), |r ^ 2 * j i| ≤ |j i|
+haM : |-1 + r * j 4 / 12| ≤ R
+haS : |1 + r * j 4 / 12| ≤ R
+hbM : |-j 1 / 2 + r * j 5 / 12| ≤ R
+this : |j 1 / 2 + r * j 5 / 12| ≤ |j 1| / 2 + |r| * |j 5| / 12
+a✝ : R < |j 1 / 2 + r * j 5 / 12|
+⊢ False
+failed
+ResearchFormalCoreR1/DeterminantMoment.lean:88:4: error: linarith failed to find a contradiction
+r : ℝ
+j : DM2Jet
+hr : 0 < r
+hr1 : r ≤ 1
+R : ℝ := dm2Radius j
+hR : 0 ≤ R
+hsum : ∑ i, |j i| = |j 0| + |j 1| + |j 2| + |j 3| + |j 4| + |j 5| + |j 6| + |j 7| + |j 8|
+hbudget : 1 + |j 0| + |j 1| + |j 2| + |j 4| + |j 5| + |j 6| ≤ R
+hscale : ∀ (i : Fin 9), |r * j i| ≤ |j i|
+hscale2 : ∀ (i : Fin 9), |r ^ 2 * j i| ≤ |j i|
+haM : |-1 + r * j 4 / 12| ≤ R
+haS : |1 + r * j 4 / 12| ≤ R
+hbM : |-j 1 / 2 + r * j 5 / 12| ≤ R
+hbS : |j 1 / 2 + r * j 5 / 12| ≤ R
+h1 : |j 0 - r * j 2 / 2| ≤ |j 0| + |r| * |j 2| / 2
+h2 : |j 0 - r * j 2 / 2 + r ^ 2 * j 6 / 8| ≤ |j 0 - r * j 2 / 2| + r ^ 2 * |j 6| / 8
+a✝ : R < |j 0 - r * j 2 / 2 + r ^ 2 * j 6 / 8|
+⊢ False
+failed
+ResearchFormalCoreR1/DeterminantMoment.lean:94:4: error: linarith failed to find a contradiction
+r : ℝ
+j : DM2Jet
+hr : 0 < r
+hr1 : r ≤ 1
+R : ℝ := dm2Radius j
+hR : 0 ≤ R
+hsum : ∑ i, |j i| = |j 0| + |j 1| + |j 2| + |j 3| + |j 4| + |j 5| + |j 6| + |j 7| + |j 8|
+hbudget : 1 + |j 0| + |j 1| + |j 2| + |j 4| + |j 5| + |j 6| ≤ R
+hscale : ∀ (i : Fin 9), |r * j i| ≤ |j i|
+hscale2 : ∀ (i : Fin 9), |r ^ 2 * j i| ≤ |j i|
+haM : |-1 + r * j 4 / 12| ≤ R
+haS : |1 + r * j 4 / 12| ≤ R
+hbM : |-j 1 / 2 + r * j 5 / 12| ≤ R
+hbS : |j 1 / 2 + r * j 5 / 12| ≤ R
+hcM : |j 0 - r * j 2 / 2 + r ^ 2 * j 6 / 8| ≤ R
+h1 : |j 0 + r * j 2 / 2| ≤ |j 0| + |r| * |j 2| / 2
+h2 : |j 0 + r * j 2 / 2 + r ^ 2 * j 6 / 8| ≤ |j 0 + r * j 2 / 2| + r ^ 2 * |j 6| / 8
+a✝ : R < |j 0 + r * j 2 / 2 + r ^ 2 * j 6 / 8|
+⊢ False
+failed
+ResearchFormalCoreR1/DeterminantMoment.lean:100:21: error: Application type mismatch: The argument
+  hM
+has type
+  |(-1 + r * j 4 / 12) * (j 0 - r * j 2 / 2 + r ^ 2 * j 6 / 8) - r * (-j 1 / 2 + r * j 5 / 12) ^ 2| ≤ 2 * R ^ 2
+but is expected to have type
+  |(-1 + r * j 4 / 12) * (j 0 - r * j 2 / 2 + r * r * j 6 / 8) - r * (-j 1 / 2 + r * j 5 / 12) ^ 2| ≤
+    npowRec 1 (2 * R ^ 2)
+in the application
+  mul_le_mul hM
+ResearchFormalCoreR1/DeterminantMoment.lean:100:46: error: failed to prove positivity/nonnegativity/nonzeroness
+ResearchFormalCoreR1/DeterminantMoment.lean:103:4: error: (deterministic) timeout at `«Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.getTableauImp»`, maximum number of heartbeats (200000) has been reached
+
+Note: Use `set_option maxHeartbeats <num>` to set the limit.
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+ResearchFormalCoreR1/DeterminantMoment.lean:47:0: error: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached
+
+Note: Use `set_option maxHeartbeats <num>` to set the limit.
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+ResearchFormalCoreR1/DeterminantMoment.lean:119:2: error: Tactic `split_ifs` failed: no if-then-else conditions to split
+
+r : ℝ
+j : DM2Jet
+hr : 0 < r
+hr1 : r ≤ 1
+⊢ sorry ^ 2 ≤ 16 * r ^ 4 * dm2Radius j ^ 8
+ResearchFormalCoreR1/DeterminantMoment.lean:144:6: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
+If you'd rather continue using `push_neg` in your project, you can implement it as follows:
+```
+open Lean.Parser.Tactic in
+macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
+  `(tactic| push $cfg:optConfig Not $[$loc]?)
+```
+ResearchFormalCoreR1/DeterminantMoment.lean:168:36: error: Tactic `apply` failed: could not unify the conclusion of `@isOpen_lt`
+  IsOpen {b | ?f b < ?g b}
+with the goal
+  MeasurableSet fun j => Real.lt✝ (-r + r ^ 2 * j 4 / 12) 0
+
+Note: The full type of `@isOpen_lt` is
+  ∀ {α : Type ?u.312} {β : Type ?u.311} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α]
+    [inst_3 : TopologicalSpace β] {f g : β → α}, Continuous f → Continuous g → IsOpen {b | f b < g b}
+
+case h₁.h₁
+r : ℝ
+hm : Continuous fun j => (dm2HM r j).det
+hs : Continuous fun j => (dm2HS r j).det
+⊢ MeasurableSet fun j => Real.lt✝ (-r + r ^ 2 * j 4 / 12) 0
+ResearchFormalCoreR1/DeterminantMoment.lean:168:36: error: Tactic `apply` failed: could not unify the conclusion of `@isOpen_lt`
+  IsOpen {b | ?f b < ?g b}
+with the goal
+  MeasurableSet fun j =>
+    Real.lt✝ 0 ((-r + r ^ 2 * j 4 / 12) * (j 0 - r * j 2 / 2 + r ^ 2 * j 6 / 8) - (-j 1 * r / 2 + r ^ 2 * j 5 / 12) ^ 2)
+
+Note: The full type of `@isOpen_lt` is
+  ∀ {α : Type ?u.312} {β : Type ?u.311} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α]
+    [inst_3 : TopologicalSpace β] {f g : β → α}, Continuous f → Continuous g → IsOpen {b | f b < g b}
+
+case h₁.h₂
+r : ℝ
+hm : Continuous fun j => (dm2HM r j).det
+hs : Continuous fun j => (dm2HS r j).det
+⊢ MeasurableSet fun j =>
+    Real.lt✝ 0 ((-r + r ^ 2 * j 4 / 12) * (j 0 - r * j 2 / 2 + r ^ 2 * j 6 / 8) - (-j 1 * r / 2 + r ^ 2 * j 5 / 12) ^ 2)
+ResearchFormalCoreR1/DeterminantMoment.lean:170:2: error: Type mismatch
+  Measurable.ite htype (Measurable.abs (Measurable.mul (Continuous.measurable hm) (Continuous.measurable hs)))
+    measurable_const
+has type
+  Measurable fun x =>
+    if dm2Negative (dm2HM r x) ∧ (dm2HS r x).det < 0 then |((fun j => (dm2HM r j).det) * fun j => (dm2HS r j).det) x|
+    else ?m.1091
+but is expected to have type
+  Measurable (dm2Weight r)
+ResearchFormalCoreR1/DeterminantMoment.lean:160:42: warning: This simp argument is unused:
+  Matrix.cons_val_zero
+
+Hint: Omit it from the simp argument list.
+  [apply] simp only [dm2HM, Matrix.det_fin_two, Matrix.cons_val_one]
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
+ResearchFormalCoreR1/DeterminantMoment.lean:160:64: warning: This simp argument is unused:
+  Matrix.cons_val_one
+
+Hint: Omit it from the simp argument list.
+  [apply] simp only [dm2HM, Matrix.det_fin_two, Matrix.cons_val_zero]
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
+ResearchFormalCoreR1/DeterminantMoment.lean:163:42: warning: This simp argument is unused:
+  Matrix.cons_val_zero
+
+Hint: Omit it from the simp argument list.
+  [apply] simp only [dm2HS, Matrix.det_fin_two, Matrix.cons_val_one]
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
+ResearchFormalCoreR1/DeterminantMoment.lean:163:64: warning: This simp argument is unused:
+  Matrix.cons_val_one
+
+Hint: Omit it from the simp argument list.
+  [apply] simp only [dm2HS, Matrix.det_fin_two, Matrix.cons_val_zero]
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/frontiers/determinant_moment_20261025/evidence/history/dm2-compile-03.log b/frontiers/determinant_moment_20261025/evidence/history/dm2-compile-03.log
new file mode 100644
index 000000000..1280e9395
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/history/dm2-compile-03.log
@@ -0,0 +1,16 @@
+ResearchFormalCoreR1/DeterminantMoment.lean:124:4: error: not a positivity goal
+ResearchFormalCoreR1/DeterminantMoment.lean:172:29: error: `fun_prop` was unable to prove `Continuous ?m.1032`
+
+Issues:
+ResearchFormalCoreR1/DeterminantMoment.lean:173:46: error: `fun_prop` was unable to prove `Continuous ?m.1052`
+
+Issues:
+ResearchFormalCoreR1/DeterminantMoment.lean:175:2: error: Type mismatch: After simplification, term
+  Measurable.ite htype (Measurable.abs (Measurable.mul (Continuous.measurable hm) (Continuous.measurable hs)))
+    measurable_const
+ has type
+  @Measurable DM2Jet ℝ MeasurableSpace.pi Real.measurableSpace fun x =>
+    if dm2Negative (dm2HM r x) ∧ (dm2HS r x).det < 0 then |((fun j => (dm2HM r j).det) * fun j => (dm2HS r j).det) x|
+    else 0
+but is expected to have type
+  @Measurable DM2Jet ℝ MeasurableSpace.pi Real.measurableSpace (dm2Weight r)
diff --git a/frontiers/determinant_moment_20261025/evidence/history/dm2-compile-04.log b/frontiers/determinant_moment_20261025/evidence/history/dm2-compile-04.log
new file mode 100644
index 000000000..e69de29bb
diff --git a/frontiers/determinant_moment_20261025/evidence/history/dm2-narrow-build-01.log b/frontiers/determinant_moment_20261025/evidence/history/dm2-narrow-build-01.log
new file mode 100644
index 000000000..38b350e78
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/history/dm2-narrow-build-01.log
@@ -0,0 +1,87 @@
+⚠ [2556/2560] Built ResearchFormalCoreR1.AlgebraV2 (4.4s)
+warning: ResearchFormalCoreR1/AlgebraV2.lean:1:0: 'Mathlib.Data.Real.Basic' has been deprecated: please replace this import by
+
+import Mathlib.Basic.Real.Basic
+⚠ [2557/2560] Built ResearchFormalCoreR1.ProbabilityCompanionsV2 (4.3s)
+warning: ResearchFormalCoreR1/ProbabilityCompanionsV2.lean:1:0: 'Mathlib.Data.Real.Sqrt' has been deprecated: please replace this import by
+
+import Mathlib.Analysis.Real.Sqrt
+warning: ResearchFormalCoreR1/ProbabilityCompanionsV2.lean:27:18: Variable name `hcW` is not explicitly referenced.
+
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _hcW
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
+warning: ResearchFormalCoreR1/ProbabilityCompanionsV2.lean:27:48: Variable name `hq` is not explicitly referenced.
+
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _hq
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
+✖ [2558/2560] Building ResearchFormalCoreR1.DeterminantMoment (10s)
+trace: .> LEAN_PATH=/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/Cli/.lake/build/lib/lean:/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/batteries/.lake/build/lib/lean:/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/Qq/.lake/build/lib/lean:/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/aesop/.lake/build/lib/lean:/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/proofwidgets/.lake/build/lib/lean:/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/importGraph/.lake/build/lib/lean:/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/plausible/.lake/build/lib/lean:/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/mathlib/.lake/build/lib/lean:/workspace/Math-/frontiers/determinant_moment_20261025/.lake/build/lib/lean /home/agent/.elan/toolchains/leanprover--lean4---v4.34.1/bin/lean /workspace/Math-/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/DeterminantMoment.lean -o /workspace/Math-/frontiers/determinant_moment_20261025/.lake/build/lib/lean/ResearchFormalCoreR1/DeterminantMoment.olean -i /workspace/Math-/frontiers/determinant_moment_20261025/.lake/build/lib/lean/ResearchFormalCoreR1/DeterminantMoment.ilean -c /workspace/Math-/frontiers/determinant_moment_20261025/.lake/build/ir/ResearchFormalCoreR1/DeterminantMoment.c --setup /workspace/Math-/frontiers/determinant_moment_20261025/.lake/build/ir/ResearchFormalCoreR1/DeterminantMoment.setup.json --json
+error: ResearchFormalCoreR1/DeterminantMoment.lean:174:4: `fun_prop` was unable to prove `Continuous fun j =>
+  !![-r + r ^ 2 * j 4 / 12, -j 1 * r / 2 + r ^ 2 * j 5 / 12;
+          -j 1 * r / 2 + r ^ 2 * j 5 / 12, j 0 - r * j 2 / 2 + r ^ 2 * j 6 / 8]
+        0 0 *
+      !![-r + r ^ 2 * j 4 / 12, -j 1 * r / 2 + r ^ 2 * j 5 / 12;
+          -j 1 * r / 2 + r ^ 2 * j 5 / 12, j 0 - r * j 2 / 2 + r ^ 2 * j 6 / 8]
+        1 1 -
+    !![-r + r ^ 2 * j 4 / 12, -j 1 * r / 2 + r ^ 2 * j 5 / 12;
+          -j 1 * r / 2 + r ^ 2 * j 5 / 12, j 0 - r * j 2 / 2 + r ^ 2 * j 6 / 8]
+        0 1 *
+      !![-r + r ^ 2 * j 4 / 12, -j 1 * r / 2 + r ^ 2 * j 5 / 12;
+          -j 1 * r / 2 + r ^ 2 * j 5 / 12, j 0 - r * j 2 / 2 + r ^ 2 * j 6 / 8]
+        1 0`
+
+Issues:
+  No theorems found for `Matrix.of` in order to prove `Continuous fun x3 => Matrix.of x3 0 0`
+  No theorems found for `Matrix.of` in order to prove `Continuous fun x3 => Matrix.of x3 0`
+  No theorems found for `Matrix.of` in order to prove `Continuous fun x3 => Matrix.of x3`
+  No theorems found for `Matrix.of` in order to prove `Continuous fun x =>
+  !![-r + r ^ 2 * x 4 / 12, -x 1 * r / 2 + r ^ 2 * x 5 / 12;
+    -x 1 * r / 2 + r ^ 2 * x 5 / 12, x 0 - r * x 2 / 2 + r ^ 2 * x 6 / 8]`
+  No theorems found for `Matrix.of` in order to prove `Continuous fun x =>
+  !![-r + r ^ 2 * x 4 / 12, -x 1 * r / 2 + r ^ 2 * x 5 / 12;
+      -x 1 * r / 2 + r ^ 2 * x 5 / 12, x 0 - r * x 2 / 2 + r ^ 2 * x 6 / 8]
+    0`
+  No theorems found for `Matrix.of` in order to prove `Continuous fun x =>
+  !![-r + r ^ 2 * x 4 / 12, -x 1 * r / 2 + r ^ 2 * x 5 / 12;
+      -x 1 * r / 2 + r ^ 2 * x 5 / 12, x 0 - r * x 2 / 2 + r ^ 2 * x 6 / 8]
+    0 0`
+error: ResearchFormalCoreR1/DeterminantMoment.lean:177:4: `fun_prop` was unable to prove `Continuous fun j =>
+  !![r + r ^ 2 * j 4 / 12, j 1 * r / 2 + r ^ 2 * j 5 / 12;
+          j 1 * r / 2 + r ^ 2 * j 5 / 12, j 0 + r * j 2 / 2 + r ^ 2 * j 6 / 8]
+        0 0 *
+      !![r + r ^ 2 * j 4 / 12, j 1 * r / 2 + r ^ 2 * j 5 / 12;
+          j 1 * r / 2 + r ^ 2 * j 5 / 12, j 0 + r * j 2 / 2 + r ^ 2 * j 6 / 8]
+        1 1 -
+    !![r + r ^ 2 * j 4 / 12, j 1 * r / 2 + r ^ 2 * j 5 / 12;
+          j 1 * r / 2 + r ^ 2 * j 5 / 12, j 0 + r * j 2 / 2 + r ^ 2 * j 6 / 8]
+        0 1 *
+      !![r + r ^ 2 * j 4 / 12, j 1 * r / 2 + r ^ 2 * j 5 / 12;
+          j 1 * r / 2 + r ^ 2 * j 5 / 12, j 0 + r * j 2 / 2 + r ^ 2 * j 6 / 8]
+        1 0`
+
+Issues:
+  No theorems found for `Matrix.of` in order to prove `Continuous fun x3 => Matrix.of x3 0 0`
+  No theorems found for `Matrix.of` in order to prove `Continuous fun x3 => Matrix.of x3 0`
+  No theorems found for `Matrix.of` in order to prove `Continuous fun x3 => Matrix.of x3`
+  No theorems found for `Matrix.of` in order to prove `Continuous fun x =>
+  !![r + r ^ 2 * x 4 / 12, x 1 * r / 2 + r ^ 2 * x 5 / 12;
+    x 1 * r / 2 + r ^ 2 * x 5 / 12, x 0 + r * x 2 / 2 + r ^ 2 * x 6 / 8]`
+  No theorems found for `Matrix.of` in order to prove `Continuous fun x =>
+  !![r + r ^ 2 * x 4 / 12, x 1 * r / 2 + r ^ 2 * x 5 / 12;
+      x 1 * r / 2 + r ^ 2 * x 5 / 12, x 0 + r * x 2 / 2 + r ^ 2 * x 6 / 8]
+    0`
+  No theorems found for `Matrix.of` in order to prove `Continuous fun x =>
+  !![r + r ^ 2 * x 4 / 12, x 1 * r / 2 + r ^ 2 * x 5 / 12;
+      x 1 * r / 2 + r ^ 2 * x 5 / 12, x 0 + r * x 2 / 2 + r ^ 2 * x 6 / 8]
+    0 0`
+error: ResearchFormalCoreR1/DeterminantMoment.lean:188:63: Invalid field `abs`: The environment does not contain `Function.abs`, so it is not possible to project the field `abs` from an expression
+  Measurable.mul (Continuous.measurable hm) (Continuous.measurable hs)
+of type
+  ∀ ⦃t : Set ℝ⦄, MeasurableSet t → MeasurableSet (((fun j => (dm2HM r j).det) * fun j => (dm2HS r j).det) ⁻¹' t)
+Some required targets logged failures:
+- ResearchFormalCoreR1.DeterminantMoment
+error: build failed
diff --git a/frontiers/determinant_moment_20261025/evidence/history/dm2-narrow-build-02.log b/frontiers/determinant_moment_20261025/evidence/history/dm2-narrow-build-02.log
new file mode 100644
index 000000000..83110a5ec
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/history/dm2-narrow-build-02.log
@@ -0,0 +1,17 @@
+✔ [2557/2561] Built ResearchFormalCoreR1.AlgebraV2 (1.4s)
+⚠ [2558/2561] Built ResearchFormalCoreR1.ProbabilityCompanionsV2 (2.0s)
+warning: ResearchFormalCoreR1/ProbabilityCompanionsV2.lean:27:18: Variable name `hcW` is not explicitly referenced.
+
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _hcW
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
+warning: ResearchFormalCoreR1/ProbabilityCompanionsV2.lean:27:48: Variable name `hq` is not explicitly referenced.
+
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _hq
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
+✔ [2559/2561] Built ResearchFormalCoreR1.DeterminantMoment (7.5s)
+✔ [2560/2561] Built ResearchFormalCoreR1 (1.7s)
+Build completed successfully (2561 jobs).
diff --git a/frontiers/determinant_moment_20261025/evidence/history/dm2-narrow-red.log b/frontiers/determinant_moment_20261025/evidence/history/dm2-narrow-red.log
new file mode 100644
index 000000000..6f7a2a189
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/history/dm2-narrow-red.log
@@ -0,0 +1,78 @@
+test_empty_link (test_gate.BlueprintTests.test_empty_link) ... ok
+test_unsupported_leanok (test_gate.BlueprintTests.test_unsupported_leanok) ... ok
+test_valid_link (test_gate.BlueprintTests.test_valid_link) ... ok
+test_wrong_link (test_gate.BlueprintTests.test_wrong_link) ... ok
+test_axiom_free (test_gate.GateTests.test_axiom_free) ... ok
+test_custom (test_gate.GateTests.test_custom) ... ok
+test_duplicate_target_output (test_gate.GateTests.test_duplicate_target_output) ... ok
+test_duplicate_target_request (test_gate.GateTests.test_duplicate_target_request) ... ok
+test_manifest_absolute (test_gate.GateTests.test_manifest_absolute) ... ok
+test_manifest_content (test_gate.GateTests.test_manifest_content) ... ok
+test_manifest_empty (test_gate.GateTests.test_manifest_empty) ... ok
+test_manifest_escape (test_gate.GateTests.test_manifest_escape) ... ok
+test_manifest_missing (test_gate.GateTests.test_manifest_missing) ... ok
+test_manifest_symlink (test_gate.GateTests.test_manifest_symlink) ... ok
+test_manifest_tamper (test_gate.GateTests.test_manifest_tamper) ... ok
+test_missing_target (test_gate.GateTests.test_missing_target) ... ok
+test_multiline (test_gate.GateTests.test_multiline) ... ok
+test_native (test_gate.GateTests.test_native) ... ok
+test_noise_denied (test_gate.GateTests.test_noise_denied) ... ok
+test_review_bad_disposition (test_gate.GateTests.test_review_bad_disposition) ... ok
+test_review_bad_evidence (test_gate.GateTests.test_review_bad_evidence) ... ok
+test_review_changed_scope (test_gate.GateTests.test_review_changed_scope) ... ok
+test_review_partial (test_gate.GateTests.test_review_partial) ... ok
+test_review_same_provider (test_gate.GateTests.test_review_same_provider) ... ok
+test_review_self (test_gate.GateTests.test_review_self) ... ok
+test_review_stale (test_gate.GateTests.test_review_stale) ... ok
+test_review_valid (test_gate.GateTests.test_review_valid) ... ok
+test_sorry (test_gate.GateTests.test_sorry) ... ok
+test_standard_axioms (test_gate.GateTests.test_standard_axioms) ... ok
+test_unexpected_target (test_gate.GateTests.test_unexpected_target) ... ok
+test_dependency_dirtied_during_execution_refuses_receipt (test_gate.RuntimeGuardTests.test_dependency_dirtied_during_execution_refuses_receipt) ... ok
+test_dependency_moved_during_execution_refuses_receipt (test_gate.RuntimeGuardTests.test_dependency_moved_during_execution_refuses_receipt) ... ok
+test_dirty_dependency_before_execution_refuses_and_preserves_build (test_gate.RuntimeGuardTests.test_dirty_dependency_before_execution_refuses_and_preserves_build) ... ok
+test_receipt_binds_attempt_and_both_equal_observations (test_gate.RuntimeGuardTests.test_receipt_binds_attempt_and_both_equal_observations) ... ok
+test_runtime_changed_between_observations_refuses_receipt (test_gate.RuntimeGuardTests.test_runtime_changed_between_observations_refuses_receipt) ... ok
+test_wrong_dependency_before_execution_refuses_and_preserves_build (test_gate.RuntimeGuardTests.test_wrong_dependency_before_execution_refuses_and_preserves_build) ... ok
+test_complete_pinned_release_record (test_gate.RuntimeVersionTests.test_complete_pinned_release_record) ... ok
+test_installed_dependency_change_still_refuses_receipt (test_gate.RuntimeVersionTests.test_installed_dependency_change_still_refuses_receipt) ... ok
+test_invalid_preflight_preserves_build_and_runs_no_build (test_gate.RuntimeVersionTests.test_invalid_preflight_preserves_build_and_runs_no_build) ... ok
+test_other_commit_after_execution_refuses_receipt (test_gate.RuntimeVersionTests.test_other_commit_after_execution_refuses_receipt) ... ok
+test_other_commit_preflight_preserves_build (test_gate.RuntimeVersionTests.test_other_commit_preflight_preserves_build) ... ok
+test_other_versions_and_incomplete_or_extra_records_refused (test_gate.RuntimeVersionTests.test_other_versions_and_incomplete_or_extra_records_refused) ... ok
+test_preflight_process_failure_preserves_build (test_gate.RuntimeVersionTests.test_preflight_process_failure_preserves_build) ... ok
+test_short_and_other_release_commits_refused (test_gate.RuntimeVersionTests.test_short_and_other_release_commits_refused) ... ok
+test_source_change_during_build_still_refuses_receipt (test_gate.RuntimeVersionTests.test_source_change_during_build_still_refuses_receipt) ... ok
+test_success_checks_before_build_and_after_controls_and_binds_both_logs (test_gate.RuntimeVersionTests.test_success_checks_before_build_and_after_controls_and_binds_both_logs) ... ok
+test_version_change_after_execution_refuses_receipt (test_gate.RuntimeVersionTests.test_version_change_after_execution_refuses_receipt) ... ok
+test_duplicate_json_rejected (test_gate.SourceContractTests.test_duplicate_json_rejected) ... ok
+test_json_object (test_gate.SourceContractTests.test_json_object) ... ok
+test_manifest_cannot_claim_kernel_status (test_gate.SourceContractTests.test_manifest_cannot_claim_kernel_status) ... ok
+test_root_declaration_cannot_evade_audit (test_gate.SourceContractTests.test_root_declaration_cannot_evade_audit) ... ok
+test_source_baseline (test_gate.SourceContractTests.test_source_baseline) ... ok
+test_unbound_gate_refused (test_gate.SourceContractTests.test_unbound_gate_refused) ... ok
+test_only_documented_algebra_repairs (test_gate.SuccessorTests.test_only_documented_algebra_repairs) ... FAIL
+test_only_documented_probability_repair (test_gate.SuccessorTests.test_only_documented_probability_repair) ... FAIL
+
+======================================================================
+FAIL: test_only_documented_algebra_repairs (test_gate.SuccessorTests.test_only_documented_algebra_repairs)
+----------------------------------------------------------------------
+Traceback (most recent call last):
+  File "/workspace/Math-/frontiers/determinant_moment_20261025/tests/test_gate.py", line 364, in test_only_documented_algebra_repairs
+    self.assertEqual((ROOT/'ResearchFormalCoreR1/AlgebraV2.lean').read_text(), expected.replace("import Mathlib\n", 'import Mathlib.Data.Real.Basic\nimport Mathlib.Tactic.FieldSimp\nimport Mathlib.Tactic.Ring\nimport Mathlib.Tactic.NormNum\n'))
+AssertionError: 'import Mathlib\n\nnamespace ResearchFormalCoreR1\n\nset[1916 chars]R1\n' != 'import Mathlib.Data.Real.Basic\nimport Mathlib.Tactic.F[2024 chars]R1\n'
+Diff is 2154 characters long. Set self.maxDiff to None to see it.
+
+======================================================================
+FAIL: test_only_documented_probability_repair (test_gate.SuccessorTests.test_only_documented_probability_repair)
+----------------------------------------------------------------------
+Traceback (most recent call last):
+  File "/workspace/Math-/frontiers/determinant_moment_20261025/tests/test_gate.py", line 368, in test_only_documented_probability_repair
+    self.assertEqual((ROOT/'ResearchFormalCoreR1/ProbabilityCompanionsV2.lean').read_text(), expected.replace("import Mathlib\n", 'import Mathlib.Data.Real.Sqrt\nimport Mathlib.Tactic.FieldSimp\nimport Mathlib.Tactic.Ring\nimport Mathlib.Tactic.NormNum\nimport Mathlib.Tactic.Positivity\nimport Mathlib.Tactic.Linarith\n'))
+AssertionError: "import Mathlib\n\nnamespace ResearchFormalCoreR1\n\nset[3433 chars]R1\n" != "import Mathlib.Data.Real.Sqrt\nimport Mathlib.Tactic.Fi[3606 chars]R1\n"
+Diff is 3776 characters long. Set self.maxDiff to None to see it.
+
+----------------------------------------------------------------------
+Ran 55 tests in 0.167s
+
+FAILED (failures=2)
diff --git a/frontiers/determinant_moment_20261025/evidence/history/dm2-target-first.log b/frontiers/determinant_moment_20261025/evidence/history/dm2-target-first.log
new file mode 100644
index 000000000..a05999cee
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/history/dm2-target-first.log
@@ -0,0 +1,15 @@
+/workspace/scratch/DM2Target.lean:1:0: error: unknown module prefix 'ResearchFormalCoreR1'
+
+No directory 'ResearchFormalCoreR1' or file 'ResearchFormalCoreR1.olean' in the search path entries:
+/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/Cli/.lake/build/lib/lean
+/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/batteries/.lake/build/lib/lean
+/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/Qq/.lake/build/lib/lean
+/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/aesop/.lake/build/lib/lean
+/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/proofwidgets/.lake/build/lib/lean
+/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/importGraph/.lake/build/lib/lean
+/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/LeanSearchClient/.lake/build/lib/lean
+/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/plausible/.lake/build/lib/lean
+/workspace/Math-/frontiers/determinant_moment_20261025/.lake/packages/mathlib/.lake/build/lib/lean
+/workspace/Math-/frontiers/determinant_moment_20261025/.lake/build/lib/lean
+/home/agent/.elan/toolchains/leanprover--lean4---v4.34.1/lib/lean
+/home/agent/.elan/toolchains/leanprover--lean4---v4.34.1/lib/lean
diff --git a/frontiers/determinant_moment_20261025/evidence/history/umbrella-mathlib-oom/RESULT.txt b/frontiers/determinant_moment_20261025/evidence/history/umbrella-mathlib-oom/RESULT.txt
new file mode 100644
index 000000000..3482a1b8f
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/history/umbrella-mathlib-oom/RESULT.txt
@@ -0,0 +1 @@
+Proof commit deb28a751f620715ec65d3bd73690905e6fee94d. Fresh build exit0; leanchecker exit137. cgroup memory.max=17179869184; memory.events oom=1, oom_kill=1. No successful receipt. Retained unchanged gate will be rerun after import-only source successor.
diff --git a/frontiers/determinant_moment_20261025/evidence/history/umbrella-mathlib-oom/build.log b/frontiers/determinant_moment_20261025/evidence/history/umbrella-mathlib-oom/build.log
new file mode 100644
index 000000000..9184d2066
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/history/umbrella-mathlib-oom/build.log
@@ -0,0 +1,17 @@
+⚠ [8924/8928] Built ResearchFormalCoreR1.ProbabilityCompanionsV2 (5.6s)
+warning: ResearchFormalCoreR1/ProbabilityCompanionsV2.lean:22:18: Variable name `hcW` is not explicitly referenced.
+
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _hcW
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
+warning: ResearchFormalCoreR1/ProbabilityCompanionsV2.lean:22:48: Variable name `hq` is not explicitly referenced.
+
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _hq
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
+✔ [8925/8928] Built ResearchFormalCoreR1.AlgebraV2 (5.8s)
+✔ [8926/8928] Built ResearchFormalCoreR1.DeterminantMoment (10s)
+✔ [8927/8928] Built ResearchFormalCoreR1 (3.6s)
+Build completed successfully (8928 jobs).
diff --git a/frontiers/determinant_moment_20261025/evidence/history/umbrella-mathlib-oom/leanchecker.log b/frontiers/determinant_moment_20261025/evidence/history/umbrella-mathlib-oom/leanchecker.log
new file mode 100644
index 000000000..e69de29bb
diff --git a/frontiers/determinant_moment_20261025/evidence/history/umbrella-mathlib-oom/version-preflight.log b/frontiers/determinant_moment_20261025/evidence/history/umbrella-mathlib-oom/version-preflight.log
new file mode 100644
index 000000000..3bdff924e
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/evidence/history/umbrella-mathlib-oom/version-preflight.log
@@ -0,0 +1 @@
+Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)
diff --git a/frontiers/determinant_moment_20261025/gate.py b/frontiers/determinant_moment_20261025/gate.py
new file mode 100644
index 000000000..e5975f367
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/gate.py
@@ -0,0 +1,262 @@
+#!/usr/bin/env python3
+"""Source-bound Lean evidence, not a scientific acceptance engine (stdlib only)."""
+import argparse
+import hashlib
+import json
+import os
+from pathlib import Path, PurePosixPath
+import re
+import shutil
+import subprocess
+import sys
+
+ALLOWED = frozenset({'propext', 'Classical.choice', 'Quot.sound'})
+NAME = r'[A-Za-z_][A-Za-z0-9_.]*'
+AXIOM = re.compile(r"'(" + NAME + r")' (?:depends on axioms: \[([^\]]*)\]|does not depend on any axioms)")
+SHA256 = re.compile(r'[0-9a-f]{64}')
+COMMIT = re.compile(r'[0-9a-f]{40}')
+ROOT = Path(__file__).resolve().parent
+
+def sha(data):
+    return hashlib.sha256(data).hexdigest()
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+def check_lean_version(text):
+    version = text.strip()
+    require(re.fullmatch(r'Lean \(version 4\.34\.1, [^()\r\n]+, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release\)', version) is not None,
+            'unexpected running Lean version: ' + repr(version))
+    return version
+
+def check_worktree_clean(name, status):
+    """`git status --porcelain` output of a dependency: staged, unstaged or untracked changes fail."""
+    require(status.strip() == '', 'dependency worktree is not clean: ' + name + ': ' + status.strip()[:200])
+
+def dependency_state(m):
+    """Exact locked revision and a clean worktree for every dependency, read from the checkouts."""
+    actual = {}
+    for name in m['dependency_revisions']:
+        repo = str(ROOT / '.lake' / 'packages' / name)
+        actual[name] = subprocess.check_output(['git', '-C', repo, 'rev-parse', 'HEAD'], text=True).strip()
+        check_worktree_clean(name, subprocess.check_output(
+            ['git', '-C', repo, 'status', '--porcelain', '--untracked-files=normal'], text=True))
+    require(actual == m['dependency_revisions'], 'installed dependency HEAD differs from lock')
+    return actual
+
+def observation(version, dependencies, digest):
+    return {'lean_version': version, 'dependency_revisions': dependencies, 'dependency_worktrees': 'CLEAN',
+            'manifest_sha256': digest}
+
+def audit_axioms(text, targets):
+    require(isinstance(targets, list) and targets and len(set(targets)) == len(targets), 'empty or duplicate target list')
+    records = {}
+    for match in AXIOM.finditer(text):
+        name, raw = match.groups()
+        require(name in targets and name not in records, 'unexpected or duplicate axiom target: ' + name)
+        axioms = [] if raw is None or not raw.strip() else [a.strip() for a in raw.split(',')]
+        require(all(re.fullmatch(NAME, a) for a in axioms), 'malformed axiom name')
+        require(set(axioms) <= ALLOWED, 'forbidden transitive axiom: ' + repr(set(axioms) - ALLOWED))
+        records[name] = sorted(set(axioms))
+    require(not AXIOM.sub('', text).strip(), 'unrecognized audit output')
+    require(set(records) == set(targets), 'missing target axiom report')
+    return records
+
+def check_files(root, files):
+    require(isinstance(files, dict) and files, 'empty file manifest')
+    root = root.resolve()
+    for name, digest in files.items():
+        p = PurePosixPath(name)
+        require(not p.is_absolute() and '..' not in p.parts and str(p) == name and '\\' not in name, 'unsafe manifest path')
+        require(isinstance(digest, str) and SHA256.fullmatch(digest), 'invalid source hash')
+        target = root / p
+        require(all(not (root.joinpath(*p.parts[:i])).is_symlink() for i in range(1, len(p.parts) + 1)), 'symlink source')
+        require(target.is_file() and target.resolve().is_relative_to(root), 'missing or escaping source: ' + name)
+        require(sha(target.read_bytes()) == digest, 'source hash mismatch: ' + name)
+
+def check_blueprint(text, targets):
+    links = re.findall(r'\\lean\{([^}]+)\}', text)
+    require(links and all(n in targets for n in links), 'missing or unresolved Blueprint declaration')
+    require('\\leanok' not in text, 'unreviewed Blueprint completion label')
+    return links
+
+def lineage_identity(party, role):
+    """Validate declared identity text, not the truth or completeness of authorship."""
+    require(isinstance(party, dict), 'malformed review lineage: ' + role)
+    placeholders = {'unknown', 'unverified', 'unspecified', 'tbd', 'n/a',
+                    'none', 'null', '?', 'not known', 'not available'}
+    result = {}
+    for key in ('provider', 'family', 'agent'):
+        value = party.get(key)
+        require(isinstance(value, str) and value.strip(), 'missing review lineage: ' + role + '.' + key)
+        normalized = ' '.join(value.split()).casefold()
+        require(normalized not in placeholders, 'ambiguous review lineage: ' + role + '.' + key)
+        result[key] = normalized
+    return result
+
+def check_alignment(review, manifest_digest, targets, scope_digest):
+    require(isinstance(review, dict), 'review must be object')
+    require(review.get('disposition') == 'ACCEPTED', 'alignment not accepted')
+    require(review.get('manifest_sha256') == manifest_digest, 'stale alignment manifest')
+    require(review.get('scope_sha256') == scope_digest, 'stale alignment scope')
+    covered = review.get('targets', [])
+    require(isinstance(covered, list) and len(covered) == len(set(covered)) and set(covered) == set(targets), 'partial or ambiguous review')
+    r = lineage_identity(review.get('reviewer'), 'reviewer')
+    authors = [('author', lineage_identity(review.get('author'), 'author'))]
+    # Absence preserves the historical single-author schema. Declared proposers
+    # are additional authors, never ignored metadata or a substitute for author.
+    proposers = review.get('proposal_authors', [])
+    require(isinstance(proposers, list), 'malformed review lineage: proposal_authors')
+    for index, proposer in enumerate(proposers):
+        role = 'proposal_authors[' + str(index) + ']'
+        identity = lineage_identity(proposer, role)
+        if 'targets' in proposer:
+            scope = proposer['targets']
+            require(isinstance(scope, list) and scope and
+                    all(isinstance(name, str) and name in targets for name in scope) and
+                    len(scope) == len(set(scope)), 'invalid proposal target scope: ' + role)
+        authors.append((role, identity))
+    for role, author in authors:
+        for key in ('provider', 'family', 'agent'):
+            require(author[key] != r[key], 'lineage not independent: ' + role + '.' + key)
+    e = review.get('evidence', {})
+    require(isinstance(e.get('repository'), str) and re.fullmatch(r'[^/\s]+/[^/\s]+', e['repository']), 'missing evidence repo')
+    require(isinstance(e.get('commit'), str) and COMMIT.fullmatch(e['commit']), 'mutable review ref')
+    require(isinstance(e.get('sha256'), str) and SHA256.fullmatch(e['sha256']), 'missing review hash')
+    require(isinstance(e.get('path'), str) and e['path'] and not PurePosixPath(e['path']).is_absolute() and '..' not in PurePosixPath(e['path']).parts, 'missing or unsafe review path')
+    # This checks structure, identity and scope. A controller must retrieve and
+    # authenticate the review evidence; strings do not prove a review happened.
+
+def load_json(text):
+    def unique(pairs):
+        obj = {}
+        for key, value in pairs:
+            require(key not in obj, 'duplicate JSON key: ' + key)
+            obj[key] = value
+        return obj
+    return json.loads(text, object_pairs_hook=unique)
+
+def source_check():
+    raw = (ROOT / 'manifest.json').read_bytes()
+    m = load_json(raw)
+    require(m.get('schema_version') == 1 and m.get('scientific_effect') == 'NONE', 'invalid evidence schema')
+    require(m.get('formalization_status') == 'proved' and m.get('alignment_status') == 'PENDING_INDEPENDENT_REVIEW', 'source metadata cannot self-award execution or review')
+    required = {'gate.py', 'tests/test_gate.py', 'lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'ResearchFormalCoreR1.lean', 'SCOPE.md', 'GLOSSARY.md', 'README.md', 'blueprint/src/content.tex', 'tests/test_alignment_lineage.py', 'LINEAGE_VALIDATION.md'}
+    require(required <= set(m['files']), 'unbound control or scope file')
+    originals = {'originals/Algebra.lean.txt': '4c196820c4db8fafc288dd35642828ba577e3544d60aba7d1d6d24f14ad1e8ae', 'originals/ProbabilityCompanions.lean.txt': '4ace6600a476859982c8851ae9097c89b082d3c96291b3c8330bd4cc00bae65d'}
+    require(all(m['files'].get(path) == value for path, value in originals.items()), 'original source identity changed or omitted')
+    require('COMPATIBILITY.md' in m['files'], 'unbound successor rationale')
+    check_files(ROOT, m['files'])
+    require((ROOT / 'lean-toolchain').read_text().strip() == 'leanprover/lean4:v4.34.1', 'wrong Lean toolchain')
+    lock = load_json((ROOT / 'lake-manifest.json').read_text())
+    packages = lock['packages']
+    require(len(packages) == len({p['name'] for p in packages}), 'duplicate dependency')
+    actual = {p['name']: p['rev'] for p in packages}
+    require(actual == m['dependency_revisions'], 'dependency lock mismatch')
+    require(all(COMMIT.fullmatch(v) for v in actual.values()), 'unpinned dependency')
+    expected_root = ''.join('import ' + path[:-5].replace('/', '.') + '\n' for path in m['source_modules'])
+    require((ROOT / 'ResearchFormalCoreR1.lean').read_text() == expected_root, 'root must only import registered modules')
+    names = []
+    for path in m['source_modules']:
+        require(path in m['files'], 'unbound source module')
+        text = (ROOT / path).read_text()
+        names.extend('ResearchFormalCoreR1.' + n for n in re.findall(r'^(?:theorem|lemma)\s+(' + NAME + ')', text, re.M))
+    require(names == m['targets'], 'target inventory differs from source declarations')
+    check_blueprint((ROOT / 'blueprint/src/content.tex').read_text(), names)
+    lean_files = {p.relative_to(ROOT).as_posix() for p in ROOT.rglob('*.lean') if '.lake' not in p.relative_to(ROOT).parts}
+    require(lean_files == set(m['source_modules']) | {'ResearchFormalCoreR1.lean'}, 'unregistered Lean module')
+    return m, sha(raw)
+
+def run(command, label, out, expect_success=True):
+    result = subprocess.run(command, cwd=ROOT, text=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, timeout=900)
+    (out / (label + '.log')).write_text(result.stdout)
+    print(label + ': exit ' + str(result.returncode), flush=True)
+    require((result.returncode == 0) == expect_success, 'unexpected process outcome: ' + label + '\n' + result.stdout[-6000:])
+    return result.stdout
+
+def execute(m, digest):
+    out = ROOT / '.lake' / 'formal-evidence'
+    out.mkdir(parents=True, exist_ok=True)
+    require(not (ROOT / '.lake').is_symlink() and not (ROOT / '.lake/build').is_symlink(), 'symlink build directory')
+    preflight_version = check_lean_version(run(['lake', 'env', 'lean', '--version'], 'version-preflight', out))
+    preflight = observation(preflight_version, dependency_state(m), digest)
+    if (ROOT / '.lake/build').exists():
+        shutil.rmtree(ROOT / '.lake/build')  # fresh local-package build; dependency cache is untouched
+    run(['lake', 'build'], 'build', out)
+    run(['lake', 'env', 'leanchecker', 'ResearchFormalCoreR1'], 'leanchecker', out)
+    audit = out / 'Audit.lean'
+    audit.write_text('import ResearchFormalCoreR1\n' + '\n'.join('#print axioms ' + n for n in m['targets']) + '\n')
+    text = run(['lake', 'env', 'lean', str(audit)], 'axioms', out)
+    axioms = audit_axioms(text, m['targets'])
+    types = out / 'Types.lean'
+    types.write_text('import ResearchFormalCoreR1\nset_option pp.explicit true\n' + '\n'.join('#check ' + n for n in m['targets']) + '\n')
+    run(['lake', 'env', 'lean', str(types)], 'elaborated-types', out)
+    # Real counterexample/mutation controls, not comparisons of fixed labels.
+    cases = {
+        'false_fold': ('import ResearchFormalCoreR1\nexample : ResearchFormalCoreR1.foldPotential 1 1 - ResearchFormalCoreR1.foldPotential 1 (-1) = (2 : Real)^3 / 7 := by\n  norm_num [ResearchFormalCoreR1.foldPotential]\n', False, None),
+        'false_power': ('import ResearchFormalCoreR1\nexample : (2 : Real)^4 <= (2 : Real)^3 := by\n  norm_num\n', False, None),
+        'sorry': ('import ResearchFormalCoreR1\ntheorem injected : False := by sorry\n#print axioms injected\n', True, 'injected'),
+        'custom_imported': ('import ResearchFormalCoreR1\naxiom hiddenPremise : False\ntheorem middle : False := hiddenPremise\ntheorem injected : False := middle\n#print axioms injected\n', True, 'injected'),
+        'native': ('import ResearchFormalCoreR1\ntheorem injected : (2 : Nat) + 2 = 4 := by native_decide\n#print axioms injected\n', True, 'injected')}
+    outcomes = {}
+    for label, (source, succeeds, target) in cases.items():
+        path = out / (label + '.lean'); path.write_text(source)
+        log = run(['lake', 'env', 'lean', str(path)], label, out, succeeds)
+        if target:
+            # Remove compiler diagnostics only by selecting the axiom line onward;
+            # absence remains an error, never an empty allowlist.
+            matches = list(AXIOM.finditer(log))
+            require(matches, 'negative control missing axiom report: ' + label)
+            payload = '\n'.join(x.group() for x in matches)
+            try:
+                audit_axioms(payload, [target])
+            except ValueError:
+                outcomes[label] = 'REJECTED_BY_AXIOM_GATE'
+            else:
+                raise ValueError('negative control escaped: ' + label)
+        else:
+            require('unsolved goals' in log or 'norm_num' in log and 'failed' in log, 'negative control did not fail on its proof goal')
+            outcomes[label] = 'REJECTED_BY_LEAN'
+    # Recheck after compilation: a build hook must not rewrite bound sources/lock.
+    _, after = source_check(); require(after == digest, 'manifest changed during execution')
+    # Final observation after the last Lean execution: the same exact release, the same locked
+    # and clean dependencies and the same bound sources as before the first one.
+    version = check_lean_version(run(['lake', 'env', 'lean', '--version'], 'version', out))
+    final = observation(version, dependency_state(m), after)
+    require(final == preflight, 'runtime, dependencies or sources changed during execution')
+    head = subprocess.check_output(['git', 'rev-parse', 'HEAD'], cwd=ROOT, text=True).strip()
+    require(COMMIT.fullmatch(head), 'missing exact checked commit')
+    receipt = dict(schema_version=1, scientific_effect='NONE', formalization_status='kernel-checked',
+                   alignment_status='PENDING_INDEPENDENT_REVIEW', manifest_sha256=digest,
+                   checked_commit=head, repository=os.environ.get('GITHUB_REPOSITORY'),
+                   workflow_run_id=os.environ.get('GITHUB_RUN_ID'),
+                   workflow_run_attempt=os.environ.get('GITHUB_RUN_ATTEMPT'), lean_version=version,
+                   dependency_revisions=m['dependency_revisions'], dependency_worktrees='CLEAN',
+                   observations={'preflight': preflight, 'final': final},
+                   axioms=axioms, negative_controls=outcomes)
+    receipt['logs'] = {p.name: sha(p.read_bytes()) for p in sorted(out.glob('*.log'))}
+    (out / 'receipt.json').write_text(json.dumps(receipt, indent=2, sort_keys=True) + '\n')
+    print(json.dumps(receipt, indent=2, sort_keys=True))
+    return receipt
+
+def main():
+    p = argparse.ArgumentParser(description=__doc__)
+    p.add_argument('--execute', action='store_true', help='run build, transitive axiom audit and negative controls')
+    p.add_argument('--alignment', type=Path, help='validate a separately authenticated alignment record; never promotes science')
+    args = p.parse_args()
+    try:
+        m, digest = source_check()
+        if args.alignment:
+            check_alignment(load_json(args.alignment.read_text()), digest, m['targets'], m['files']['SCOPE.md'])
+        if args.execute:
+            execute(m, digest)
+        else:
+            print('SOURCE_IDENTITY_PASS (not a Lean build or scientific acceptance): ' + digest)
+    except (ValueError, KeyError, TypeError, OSError, subprocess.SubprocessError) as e:
+        print('FORMAL_GATE_FAIL: ' + str(e), file=sys.stderr)
+        return 1
+    return 0
+
+if __name__ == '__main__':
+    sys.exit(main())
diff --git a/frontiers/determinant_moment_20261025/lake-manifest.json b/frontiers/determinant_moment_20261025/lake-manifest.json
new file mode 100644
index 000000000..d482b5f1e
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/lake-manifest.json
@@ -0,0 +1,117 @@
+{
+  "version": "1.2.0",
+  "packagesDir": ".lake/packages",
+  "packages": [
+    {
+      "name": "plausible",
+      "url": "https://github.com/leanprover-community/plausible",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "name": "LeanSearchClient",
+      "url": "https://github.com/leanprover-community/LeanSearchClient",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "name": "importGraph",
+      "url": "https://github.com/leanprover-community/import-graph",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "e928b72544873815af278d38681b31c0293588e3",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "name": "proofwidgets",
+      "url": "https://github.com/leanprover-community/ProofWidgets4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "name": "aesop",
+      "url": "https://github.com/leanprover-community/aesop",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "355695d523e41d0554926416cba2a2b3544fbbc9",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "master",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "name": "Qq",
+      "url": "https://github.com/leanprover-community/quote4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "master",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "name": "batteries",
+      "url": "https://github.com/leanprover-community/batteries",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "name": "Cli",
+      "url": "https://github.com/leanprover/lean4-cli",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover",
+      "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "v4.34.0",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "name": "mathlib",
+      "url": "https://github.com/leanprover-community/mathlib4.git",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "d13f23b723b8a846827a245b89c10fc7d3f11612",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "d13f23b723b8a846827a245b89c10fc7d3f11612",
+      "inherited": false,
+      "configFile": "lakefile.lean"
+    }
+  ],
+  "name": "universal_law_formal",
+  "lakeDir": ".lake",
+  "fixedToolchain": true
+}
diff --git a/frontiers/determinant_moment_20261025/lakefile.toml b/frontiers/determinant_moment_20261025/lakefile.toml
new file mode 100644
index 000000000..8117eae1b
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/lakefile.toml
@@ -0,0 +1,11 @@
+name = "universal_law_formal"
+version = "0.1.0"
+defaultTargets = ["ResearchFormalCoreR1"]
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4.git"
+rev = "d13f23b723b8a846827a245b89c10fc7d3f11612"
+
+[[lean_lib]]
+name = "ResearchFormalCoreR1"
diff --git a/frontiers/determinant_moment_20261025/lean-toolchain b/frontiers/determinant_moment_20261025/lean-toolchain
new file mode 100644
index 000000000..ba8ebf2db
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.34.1
diff --git a/frontiers/determinant_moment_20261025/manifest.json b/frontiers/determinant_moment_20261025/manifest.json
new file mode 100644
index 000000000..71a692415
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/manifest.json
@@ -0,0 +1,85 @@
+{
+  "schema_version": 1,
+  "scientific_effect": "NONE",
+  "formalization_status": "proved",
+  "alignment_status": "PENDING_INDEPENDENT_REVIEW",
+  "dependency_revisions": {
+    "plausible": "118aa17ee84656b8bd727fef7c458ee8c833385c",
+    "LeanSearchClient": "ddf04cf3949fa556442341e87d47f9f6e6074707",
+    "importGraph": "e928b72544873815af278d38681b31c0293588e3",
+    "proofwidgets": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5",
+    "aesop": "355695d523e41d0554926416cba2a2b3544fbbc9",
+    "Qq": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259",
+    "batteries": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
+    "Cli": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
+    "mathlib": "d13f23b723b8a846827a245b89c10fc7d3f11612"
+  },
+  "source_modules": [
+    "ResearchFormalCoreR1/AlgebraV2.lean",
+    "ResearchFormalCoreR1/ProbabilityCompanionsV2.lean",
+    "ResearchFormalCoreR1/DeterminantMoment.lean"
+  ],
+  "targets": [
+    "ResearchFormalCoreR1.ec005_fold_gap",
+    "ResearchFormalCoreR1.ec008_factor_expansion",
+    "ResearchFormalCoreR1.ec010_generic",
+    "ResearchFormalCoreR1.ec010_transverse",
+    "ResearchFormalCoreR1.ec011_scalar_cancellation",
+    "ResearchFormalCoreR1.ec014_contact_power",
+    "ResearchFormalCoreR1.p02_lm008_r2_cancel",
+    "ResearchFormalCoreR1.p02_lm008_cross_multiplied",
+    "ResearchFormalCoreR1.p02_lm008_quotient_bound",
+    "ResearchFormalCoreR1.p02_lm009_bad_event_threshold",
+    "ResearchFormalCoreR1.p02_lm009_power40_identity",
+    "ResearchFormalCoreR1.p02_lm009_r4_le_r3",
+    "ResearchFormalCoreR1.p02_lm009_palm_r4_to_r3",
+    "ResearchFormalCoreR1.dm2_untyped",
+    "ResearchFormalCoreR1.dm2_pointwise",
+    "ResearchFormalCoreR1.dm2_negative_iff",
+    "ResearchFormalCoreR1.dm2_weight_measurable",
+    "ResearchFormalCoreR1.dm2_moment"
+  ],
+  "files": {
+    "LINEAGE_VALIDATION.md": "bba9d0a859f1ba45670fe122e4e72ae1094a2226de98aa814d838b0baaf61815",
+    "lake-manifest.json": "d63753befccc21923783a5085148e3ff028d97134ea52f5a08bd87ecf1b0b043",
+    "COMPATIBILITY.md": "216b772d417ce273499b692481f3c4e6e1f499c67ff41cb92f008a9b9bf09513",
+    "gate.py": "25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a",
+    "ResearchFormalCoreR1.lean": "7fd8b5fee3db0847b52e01d7cb2515b7a9e77846f4c5db8b8277ef46084a6610",
+    "lean-toolchain": "d5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b",
+    "lakefile.toml": "d629891716c169404d1f0d76492441c8dd66f1e790b1b8b0819e51c8d5059255",
+    "README.md": "739acd26766ae9e883c9bdb1912096187f8b78e630ba59b960effdd84aa7c395",
+    ".gitignore": "b34af236d1df9e39ed4f98fca51702530ce76bdee4e1a69512f6caed933c3374",
+    "SCOPE.md": "c3cb56539a6b1dcb41c6ac378c1797e95ef878ba03276456276e0bb3abfa3ddd",
+    "SOURCE_MAP.md": "32b5e48e9d8150927542718e719a71f6d59ef7593b78dd827dd52c18c47681f6",
+    "GLOSSARY.md": "3cd098f26e3020b780307617fc65c53ed040789d54ea53930c5fa21524bc7323",
+    "ResearchFormalCoreR1/ProbabilityCompanionsV2.lean": "dbc42b17797be688fecec790f32fcfd0004d98ac776cbbe0471c62c3f506aa41",
+    "ResearchFormalCoreR1/DeterminantMoment.lean": "661b73c3f21c6d2529f5e09ce426d89c01939ab27a5cc868db3802c7e66ea82d",
+    "ResearchFormalCoreR1/AlgebraV2.lean": "71e4327df9f7d6979f1467f7e0d880e0ab0a70ab6d234802d8c7a1624b9ce2d9",
+    "originals/ProbabilityCompanions.lean.txt": "4ace6600a476859982c8851ae9097c89b082d3c96291b3c8330bd4cc00bae65d",
+    "originals/Algebra.lean.txt": "4c196820c4db8fafc288dd35642828ba577e3544d60aba7d1d6d24f14ad1e8ae",
+    "tests/test_gate.py": "b5fc1b723d5137d0a41ebb67b29e25da727edfad391d62afa6d44c32b5e114c6",
+    "tests/test_alignment_lineage.py": "c510c6566d7689bebde76843582e9936dfa9e62e783b816b5e4f63d83434b893",
+    "controls/false_omit_q.lean.txt": "cbcd846199ff2f48099bc33518188ddfcd3667f9e7a9ef932a2627e69b540a46",
+    "controls/false_r6.lean.txt": "c0ce4598ff5e188475e0ec9d0eeb3c3465169583a457baec90625d7b0f3a8439",
+    "evidence/history/dm2-compile-01.log": "44b7e4dcb7875573afefd90118a796051d92c6a4010776f65f5ecaddad71051f",
+    "evidence/history/dm2-compile-03.log": "be3c8fa0c7074bdcfaee86d48c022b759154108fe58a1d77c70b5492846c067d",
+    "evidence/history/dm2-target-first.log": "83ae9887c7f4d303907fd58e16a1c2a97db6fae268b9e9017a7bd3b1a837c324",
+    "evidence/history/dm2-narrow-build-01.log": "b374accd6131126859dc10b9d0143ce825ad55399decc4bc7be6ee5cf14b84c5",
+    "evidence/history/dm2-narrow-red.log": "6be5210e176a867bbb345377f341449b77baa1b6a12c7af868253aaf1adf6ed5",
+    "evidence/history/dm2-narrow-build-02.log": "2ac411e5aed7a76b291915910e8cf6902f425d194b8a648125645895495ba6c3",
+    "evidence/history/dm2-compile-04.log": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855",
+    "evidence/history/dm2-baseline-tests.log": "00c70d818d406bcca228ad07644d2307ed6ab61a3b2582c40d9cb89edb67749e",
+    "evidence/history/dm2-compile-02.log": "1a298e7d92c2376be92fce08f0993d0ee48e822a4c098c7b84b64539158e91cc",
+    "evidence/history/umbrella-mathlib-oom/version-preflight.log": "355a9a028f81641782d75d6e6b58dec70f29d2f61238a9e271690259d9bf5680",
+    "evidence/history/umbrella-mathlib-oom/build.log": "5c71383534ec697ec05727cbad4752d5f523518479fd1eba1c731f3291fd5e3c",
+    "evidence/history/umbrella-mathlib-oom/leanchecker.log": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855",
+    "evidence/history/umbrella-mathlib-oom/RESULT.txt": "80aa3b84279bd40bd98d612d24eca8556ecbfc0fb56005a8fdcbabe644493ecd",
+    "blueprint/src/content.tex": "70af0e53e6c7166477e511a90f7f79a872b14c7717e55453caee227752bb0c31"
+  },
+  "source_binding": {
+    "repository": "d6g8k5htny-coder/Math-",
+    "commit": "c4eabc1a917ba2c1b96fe4af425cf2a484877c03",
+    "path": "imports/hardening_ebedb780/P02-LM-002/proof.md.export.txt",
+    "sha256": "0f8f80922feb603e5b6e530eb885a7819b3a98d90d3c42d60a68259af766f7de"
+  }
+}
diff --git a/frontiers/determinant_moment_20261025/originals/Algebra.lean.txt b/frontiers/determinant_moment_20261025/originals/Algebra.lean.txt
new file mode 100644
index 000000000..4554c810a
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/originals/Algebra.lean.txt
@@ -0,0 +1,51 @@
+import Mathlib
+
+namespace ResearchFormalCoreR1
+
+set_option autoImplicit false
+
+/-- Canonical A₂ normal-form potential, parameterized by `s` with λ = s². -/
+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]
+  ring
+
+end ResearchFormalCoreR1
diff --git a/frontiers/determinant_moment_20261025/originals/ProbabilityCompanions.lean.txt b/frontiers/determinant_moment_20261025/originals/ProbabilityCompanions.lean.txt
new file mode 100644
index 000000000..82aa4208c
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/originals/ProbabilityCompanions.lean.txt
@@ -0,0 +1,89 @@
+import Mathlib
+
+namespace ResearchFormalCoreR1
+
+set_option autoImplicit false
+
+/-- P02-LM-008 algebraic companion: exact cancellation of the `r²` factor
+    after the Cauchy–Schwarz numerator bound and the normalizer lower bound
+    have been established in the surrounding probability theorem. -/
+theorem p02_lm008_r2_cancel
+    (r cW cZ q : ℝ) (hr : r ≠ 0) (hcZ : cZ ≠ 0) :
+    (Real.sqrt cW * r ^ 2 * Real.sqrt q) / (cZ * r ^ 2) =
+      (Real.sqrt cW / cZ) * Real.sqrt q := by
+  field_simp [hr, hcZ]
+  ring
+
+/-- P02-LM-008 cross-multiplied transfer companion.  This theorem starts
+    from an already supplied Cauchy–Schwarz numerator estimate and an exact
+    normalizer lower bound.  It does not formalize the measure-theoretic
+    Cauchy–Schwarz step itself. -/
+theorem p02_lm008_cross_multiplied
+    (n z r cW cZ q : ℝ)
+    (hr : 0 < r) (hcW : 0 ≤ cW) (hcZ : 0 < cZ) (hq : 0 ≤ q)
+    (hz : cZ * r ^ 2 ≤ z)
+    (hn : n ≤ Real.sqrt cW * r ^ 2 * Real.sqrt q) :
+    n * (cZ * r ^ 2) ≤
+      (Real.sqrt cW * r ^ 2 * Real.sqrt q) * z := by
+  have hden : 0 ≤ cZ * r ^ 2 :=
+    mul_nonneg (le_of_lt hcZ) (sq_nonneg r)
+  have hnum : 0 ≤ Real.sqrt cW * r ^ 2 * Real.sqrt q := by
+    positivity
+  calc
+    n * (cZ * r ^ 2) ≤
+        (Real.sqrt cW * r ^ 2 * Real.sqrt q) * (cZ * r ^ 2) := by
+      exact mul_le_mul_of_nonneg_right hn hden
+    _ ≤ (Real.sqrt cW * r ^ 2 * Real.sqrt q) * z := by
+      exact mul_le_mul_of_nonneg_left hz hnum
+
+/-- P02-LM-008 quotient companion.  With positive denominators, the
+    cross-multiplied inequality and exact `r²` cancellation yield the Palm
+    square-root transfer coefficient. -/
+theorem p02_lm008_quotient_bound
+    (n z r cW cZ q : ℝ)
+    (hr : 0 < r) (hcW : 0 ≤ cW) (hcZ : 0 < cZ) (hq : 0 ≤ q)
+    (hzpos : 0 < z) (hz : cZ * r ^ 2 ≤ z)
+    (hn : n ≤ Real.sqrt cW * r ^ 2 * Real.sqrt q) :
+    n / z ≤ (Real.sqrt cW / cZ) * Real.sqrt q := by
+  have hscaled : 0 < cZ * r ^ 2 :=
+    mul_pos hcZ (sq_pos_of_pos hr)
+  have hcross :=
+    p02_lm008_cross_multiplied n z r cW cZ q hr hcW hcZ hq hz hn
+  rw [← p02_lm008_r2_cancel r cW cZ q (ne_of_gt hr) (ne_of_gt hcZ)]
+  exact (div_le_div_iff₀ hzpos hscaled).2 hcross
+
+/-- P02-LM-009 deterministic threshold companion.  Failure of
+    `r * R^5 ≤ ε` implies the fifth-power threshold used before Markov's
+    inequality. -/
+theorem p02_lm009_bad_event_threshold
+    (r R ε : ℝ) (hr : 0 < r) (hbad : ε < r * R ^ 5) :
+    ε / r < R ^ 5 := by
+  exact (div_lt_iff₀ hr).2 (by simpa [mul_comm] using hbad)
+
+/-- The fixed exponent identity used when the 40th moment is selected in
+    the P02-LM-009 application. -/
+theorem p02_lm009_power40_identity (R : ℝ) :
+    (R ^ 5) ^ 8 = R ^ 40 := by
+  ring
+
+/-- In the final P0.2 power ledger, an `O(r^4)` Palm tail is also `O(r^3)`
+    on `0 ≤ r ≤ 1`. -/
+theorem p02_lm009_r4_le_r3
+    (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) :
+    r ^ 4 ≤ r ^ 3 := by
+  have h : 0 ≤ r ^ 3 * (1 - r) :=
+    mul_nonneg (pow_nonneg hr0 3) (sub_nonneg.mpr hr1)
+  nlinarith
+
+/-- Conditional rate companion: once the Palm square-root transfer has
+    produced a uniform `C r^4` bound, the cubic target follows on `r ≤ 1`. -/
+theorem p02_lm009_palm_r4_to_r3
+    (p C r : ℝ) (hC : 0 ≤ C) (hr0 : 0 ≤ r) (hr1 : r ≤ 1)
+    (hp : p ≤ C * r ^ 4) :
+    p ≤ C * r ^ 3 := by
+  calc
+    p ≤ C * r ^ 4 := hp
+    _ ≤ C * r ^ 3 := by
+      exact mul_le_mul_of_nonneg_left (p02_lm009_r4_le_r3 r hr0 hr1) hC
+
+end ResearchFormalCoreR1
diff --git a/frontiers/determinant_moment_20261025/tests/test_alignment_lineage.py b/frontiers/determinant_moment_20261025/tests/test_alignment_lineage.py
new file mode 100644
index 000000000..86636772d
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/tests/test_alignment_lineage.py
@@ -0,0 +1,181 @@
+"""Declared-lineage validation only; synthetic fixtures do not authenticate agents."""
+import copy
+import importlib.util
+import json
+import tempfile
+from pathlib import Path
+import unittest
+
+ROOT = Path(__file__).resolve().parents[1]
+SPEC = importlib.util.spec_from_file_location('lineage_gate_under_test', ROOT / 'gate.py')
+gate = importlib.util.module_from_spec(SPEC)
+SPEC.loader.exec_module(gate)
+
+TARGETS = ['ResearchFormalCoreR1.first', 'ResearchFormalCoreR1.second']
+MANIFEST, SCOPE = 'a' * 64, 'b' * 64
+
+
+def valid_review():
+    return {
+        'disposition': 'ACCEPTED', 'manifest_sha256': MANIFEST,
+        'scope_sha256': SCOPE, 'targets': list(TARGETS),
+        'author': {'provider': 'Author Provider', 'family': 'Author Family', 'agent': 'author-session'},
+        'reviewer': {'provider': 'Reviewer Provider', 'family': 'Reviewer Family', 'agent': 'review-session'},
+        'evidence': {'repository': 'fixture/repository', 'path': 'reviews/fixture.md',
+                     'commit': 'c' * 40, 'sha256': 'd' * 64},
+    }
+
+
+def proposer():
+    return {'provider': 'Proposal Provider', 'family': 'Proposal Family', 'agent': 'proposal-session',
+            'targets': [TARGETS[0]], 'pr': 'fixture#1'}
+
+
+class AlignmentLineageTests(unittest.TestCase):
+    def check(self, review):
+        return gate.check_alignment(review, MANIFEST, TARGETS, SCOPE)
+
+    def reject(self, review, reason='lineage'):
+        with self.assertRaisesRegex(ValueError, reason):
+            self.check(review)
+
+    def test_legacy_single_author_record(self):
+        self.check(valid_review())
+
+    def test_known_distinct_proposer(self):
+        r = valid_review(); r['proposal_authors'] = [proposer()]
+        self.check(r)
+
+    def test_explicit_empty_proposer_list(self):
+        r = valid_review(); r['proposal_authors'] = []
+        self.check(r)
+
+    def test_unscoped_known_proposer(self):
+        r = valid_review(); p = proposer(); del p['targets']; r['proposal_authors'] = [p]
+        self.check(r)
+
+    def test_every_declared_proposer_is_checked(self):
+        r = valid_review(); p = proposer(); p['provider'] = r['reviewer']['provider']
+        r['proposal_authors'] = [proposer(), p]
+        self.reject(r)
+
+    def test_same_proposer_provider(self):
+        r = valid_review(); p = proposer(); p['provider'] = r['reviewer']['provider']
+        r['proposal_authors'] = [p]; self.reject(r)
+
+    def test_same_proposer_family(self):
+        r = valid_review(); p = proposer(); p['family'] = r['reviewer']['family']
+        r['proposal_authors'] = [p]; self.reject(r)
+
+    def test_same_proposer_agent(self):
+        r = valid_review(); p = proposer(); p['agent'] = r['reviewer']['agent']
+        r['proposal_authors'] = [p]; self.reject(r)
+
+    def test_proposer_identity_normalization(self):
+        r = valid_review(); p = proposer(); p['provider'] = '  REVIEWER\tPROVIDER  '
+        r['proposal_authors'] = [p]; self.reject(r)
+
+    def test_primary_identity_normalization(self):
+        r = valid_review(); r['author']['provider'] = '  REVIEWER\tPROVIDER  '
+        self.reject(r)
+
+    def test_placeholder_lineage_in_all_roles(self):
+        for role in ('author', 'reviewer', 'proposal'):
+            for key in ('provider', 'family', 'agent'):
+                for value in ('UNKNOWN', ' unknown ', 'Unverified', 'UNSPECIFIED', 'TBD',
+                              'N/A', 'NONE', 'null', '?', 'not known', 'Not Available'):
+                    with self.subTest(role=role, key=key, value=value):
+                        r = valid_review(); p = proposer(); r['proposal_authors'] = [p]
+                        (p if role == 'proposal' else r[role])[key] = value
+                        self.reject(r)
+
+    def test_missing_proposer_identity_field(self):
+        for key in ('provider', 'family', 'agent'):
+            with self.subTest(key=key):
+                r = valid_review(); p = proposer(); del p[key]; r['proposal_authors'] = [p]
+                self.reject(r)
+
+    def test_blank_or_nonstring_proposer_identity(self):
+        for value in ('', ' \t\n ', None, 7, [], {}):
+            with self.subTest(value=value):
+                r = valid_review(); p = proposer(); p['provider'] = value
+                r['proposal_authors'] = [p]; self.reject(r)
+
+    def test_malformed_primary_and_reviewer_objects(self):
+        for role in ('author', 'reviewer'):
+            for value in (None, [], 'provider', 7):
+                with self.subTest(role=role, value=value):
+                    r = valid_review(); r[role] = value; self.reject(r)
+
+    def test_malformed_proposer_collection(self):
+        for value in (None, {}, 'provider', 7):
+            with self.subTest(value=value):
+                r = valid_review(); r['proposal_authors'] = value; self.reject(r)
+
+    def test_malformed_proposer_object(self):
+        for value in (None, [], 'provider', 7):
+            with self.subTest(value=value):
+                r = valid_review(); r['proposal_authors'] = [value]; self.reject(r)
+
+    def test_invalid_proposer_target_scope(self):
+        for value in ([], [TARGETS[0], TARGETS[0]], ['Unreviewed.target'],
+                      None, TARGETS[0], [1], [{}]):
+            with self.subTest(value=value):
+                r = valid_review(); p = proposer(); p['targets'] = value
+                r['proposal_authors'] = [p]; self.reject(r, 'proposal target')
+
+    def test_withheld_record_remains_rejected(self):
+        r = valid_review(); r['disposition'] = 'WITHHELD_PROPOSER_LINEAGE_UNKNOWN'
+        p = proposer(); p['provider'] = 'UNKNOWN'; r['proposal_authors'] = [p]
+        self.reject(r, 'alignment not accepted')
+
+    def test_disposition_only_edit_cannot_hide_unknown_proposer(self):
+        r = valid_review(); p = proposer(); p['provider'] = p['family'] = 'UNKNOWN'
+        r['proposal_authors'] = [p]
+        self.reject(r)
+
+    def test_input_not_mutated(self):
+        r = valid_review(); r['proposal_authors'] = [proposer()]; original = copy.deepcopy(r)
+        self.check(r); self.assertEqual(r, original)
+
+    def test_existing_digest_scope_and_coverage_checks(self):
+        for key, value in (('manifest_sha256', 'e' * 64), ('scope_sha256', 'f' * 64),
+                           ('targets', [TARGETS[0]])):
+            with self.subTest(key=key):
+                r = valid_review(); r[key] = value
+                with self.assertRaises(ValueError): self.check(r)
+
+
+    def assert_required_lineage_file(self, omitted):
+        # Fail at the required-file inventory before accessing any source bytes.
+        required = {'gate.py', 'tests/test_gate.py', 'lean-toolchain', 'lakefile.toml',
+                    'lake-manifest.json', 'ResearchFormalCoreR1.lean', 'SCOPE.md',
+                    'GLOSSARY.md', 'README.md', 'blueprint/src/content.tex',
+                    'tests/test_alignment_lineage.py', 'LINEAGE_VALIDATION.md'}
+        files = {name: '0' * 64 for name in required if name != omitted}
+        files.update({
+            'originals/Algebra.lean.txt': '4c196820c4db8fafc288dd35642828ba577e3544d60aba7d1d6d24f14ad1e8ae',
+            'originals/ProbabilityCompanions.lean.txt': '4ace6600a476859982c8851ae9097c89b082d3c96291b3c8330bd4cc00bae65d',
+            'COMPATIBILITY.md': '0' * 64,
+        })
+        manifest = {'schema_version': 1, 'scientific_effect': 'NONE',
+                    'formalization_status': 'proved', 'alignment_status': 'PENDING_INDEPENDENT_REVIEW',
+                    'files': files}
+        old_root = gate.ROOT
+        with tempfile.TemporaryDirectory() as directory:
+            gate.ROOT = Path(directory)
+            try:
+                (gate.ROOT / 'manifest.json').write_text(json.dumps(manifest))
+                with self.assertRaisesRegex(ValueError, 'unbound control or scope file'):
+                    gate.source_check()
+            finally:
+                gate.ROOT = old_root
+
+    def test_lineage_tests_cannot_be_unbound(self):
+        self.assert_required_lineage_file('tests/test_alignment_lineage.py')
+
+    def test_lineage_scope_cannot_be_unbound(self):
+        self.assert_required_lineage_file('LINEAGE_VALIDATION.md')
+
+if __name__ == '__main__':
+    unittest.main()
diff --git a/frontiers/determinant_moment_20261025/tests/test_gate.py b/frontiers/determinant_moment_20261025/tests/test_gate.py
new file mode 100644
index 000000000..781531251
--- /dev/null
+++ b/frontiers/determinant_moment_20261025/tests/test_gate.py
@@ -0,0 +1,370 @@
+import copy
+import hashlib
+import importlib.util
+import json
+import contextlib
+import io
+from pathlib import Path
+import shutil
+import subprocess
+import tempfile
+import unittest
+from unittest.mock import patch
+
+ROOT = Path(__file__).resolve().parents[1]
+spec = importlib.util.spec_from_file_location('gate', ROOT / 'gate.py')
+gate = importlib.util.module_from_spec(spec) if spec else None
+if spec and spec.loader and (ROOT / 'gate.py').exists():
+    spec.loader.exec_module(gate)
+
+class GateTests(unittest.TestCase):
+    def setUp(self):
+        self.assertTrue(hasattr(gate, 'audit_axioms'), 'formal evidence gate not implemented')
+
+    def test_standard_axioms(self):
+        self.assertEqual(gate.audit_axioms("'X.a' depends on axioms: [propext, Classical.choice, Quot.sound]", ['X.a'])['X.a'], ['Classical.choice', 'Quot.sound', 'propext'])
+    def test_axiom_free(self):
+        self.assertEqual(gate.audit_axioms("'X.a' does not depend on any axioms", ['X.a']), {'X.a': []})
+    def test_sorry(self):
+        with self.assertRaises(ValueError): gate.audit_axioms("'X.a' depends on axioms: [sorryAx]", ['X.a'])
+    def test_custom(self):
+        with self.assertRaises(ValueError): gate.audit_axioms("'X.a' depends on axioms: [Other.hidden]", ['X.a'])
+    def test_native(self):
+        with self.assertRaises(ValueError): gate.audit_axioms("'X.a' depends on axioms: [X.a._nativeDecide_1]", ['X.a'])
+    def test_missing_target(self):
+        with self.assertRaises(ValueError): gate.audit_axioms('', ['X.a'])
+    def test_duplicate_target_output(self):
+        with self.assertRaises(ValueError): gate.audit_axioms("'X.a' does not depend on any axioms\n'X.a' does not depend on any axioms", ['X.a'])
+    def test_duplicate_target_request(self):
+        with self.assertRaises(ValueError): gate.audit_axioms("'X.a' does not depend on any axioms", ['X.a','X.a'])
+    def test_unexpected_target(self):
+        with self.assertRaises(ValueError): gate.audit_axioms("'X.b' does not depend on any axioms", ['X.a'])
+    def test_multiline(self):
+        self.assertIn('X.a', gate.audit_axioms("'X.a' depends on axioms: [propext,\n Classical.choice]", ['X.a']))
+    def test_noise_denied(self):
+        with self.assertRaises(ValueError): gate.audit_axioms("error: bad\n'X.a' does not depend on any axioms", ['X.a'])
+    def test_manifest_content(self):
+        with tempfile.TemporaryDirectory() as d:
+            p=Path(d); (p/'x').write_bytes(b'abc')
+            self.assertEqual(gate.check_files(p, {'x':hashlib.sha256(b'abc').hexdigest()}), None)
+    def test_manifest_tamper(self):
+        with tempfile.TemporaryDirectory() as d:
+            p=Path(d); (p/'x').write_bytes(b'bad')
+            with self.assertRaises(ValueError): gate.check_files(p, {'x':hashlib.sha256(b'abc').hexdigest()})
+    def test_manifest_missing(self):
+        with tempfile.TemporaryDirectory() as d:
+            with self.assertRaises(ValueError): gate.check_files(Path(d), {'missing':'0'*64})
+    def test_manifest_escape(self):
+        with tempfile.TemporaryDirectory() as d:
+            with self.assertRaises(ValueError): gate.check_files(Path(d), {'../x':'0'*64})
+    def test_manifest_absolute(self):
+        with tempfile.TemporaryDirectory() as d:
+            with self.assertRaises(ValueError): gate.check_files(Path(d), {'/x':'0'*64})
+    def test_manifest_symlink(self):
+        with tempfile.TemporaryDirectory() as d:
+            p=Path(d); (p/'x').write_bytes(b'a'); (p/'y').symlink_to(p/'x')
+            with self.assertRaises(ValueError): gate.check_files(p, {'y':hashlib.sha256(b'a').hexdigest()})
+    def test_manifest_empty(self):
+        with tempfile.TemporaryDirectory() as d:
+            with self.assertRaises(ValueError): gate.check_files(Path(d), {})
+    def review(self):
+        return dict(disposition='ACCEPTED',manifest_sha256='a'*64,targets=['X.a'],scope_sha256='b'*64,
+                    author={'provider':'OpenAI','family':'GPT','agent':'A'},reviewer={'provider':'Other','family':'Different','agent':'B'},
+                    evidence={'repository':'o/r','commit':'c'*40,'path':'review.md','sha256':'d'*64})
+    def test_review_valid(self):
+        gate.check_alignment(self.review(), 'a'*64, ['X.a'], 'b'*64)
+    def test_review_stale(self):
+        with self.assertRaises(ValueError): gate.check_alignment(self.review(), 'e'*64, ['X.a'], 'b'*64)
+    def test_review_self(self):
+        r=self.review(); r['reviewer']=r['author'].copy()
+        with self.assertRaises(ValueError): gate.check_alignment(r, 'a'*64, ['X.a'], 'b'*64)
+    def test_review_same_provider(self):
+        r=self.review(); r['reviewer']['provider']='OpenAI'
+        with self.assertRaises(ValueError): gate.check_alignment(r, 'a'*64, ['X.a'], 'b'*64)
+    def test_review_partial(self):
+        with self.assertRaises(ValueError): gate.check_alignment(self.review(), 'a'*64, ['X.a','X.b'], 'b'*64)
+    def test_review_bad_disposition(self):
+        r=self.review(); r['disposition']='AMEND_REQUIRED'
+        with self.assertRaises(ValueError): gate.check_alignment(r, 'a'*64, ['X.a'], 'b'*64)
+    def test_review_bad_evidence(self):
+        r=self.review(); r['evidence']['commit']='main'
+        with self.assertRaises(ValueError): gate.check_alignment(r, 'a'*64, ['X.a'], 'b'*64)
+    def test_review_changed_scope(self):
+        with self.assertRaises(ValueError): gate.check_alignment(self.review(), 'a'*64, ['X.a'], 'c'*64)
+
+class BlueprintTests(unittest.TestCase):
+    def test_valid_link(self):
+        self.assertEqual(gate.check_blueprint(r'\lean{X.a}', ['X.a']), ['X.a'])
+    def test_wrong_link(self):
+        with self.assertRaises(ValueError): gate.check_blueprint(r'\lean{X.b}', ['X.a'])
+    def test_empty_link(self):
+        with self.assertRaises(ValueError): gate.check_blueprint('', ['X.a'])
+    def test_unsupported_leanok(self):
+        with self.assertRaises(ValueError): gate.check_blueprint(r'\lean{X.a}\leanok', ['X.a'])
+
+class SourceContractTests(unittest.TestCase):
+    def fixture(self):
+        import shutil
+        self.tmp = tempfile.TemporaryDirectory()
+        self.addCleanup(self.tmp.cleanup)
+        p = Path(self.tmp.name) / 'formal'
+        shutil.copytree(ROOT, p, ignore=shutil.ignore_patterns('.lake', '__pycache__'))
+        self.previous = gate.ROOT; gate.ROOT = p
+        self.addCleanup(lambda: setattr(gate, 'ROOT', self.previous))
+        self.m = json.loads((p/'manifest.json').read_text())
+        self.m['files'] = {q.relative_to(p).as_posix(): hashlib.sha256(q.read_bytes()).hexdigest() for q in p.rglob('*') if q.is_file() and q.name != 'manifest.json'}
+        self.p = p
+        return p
+    def save(self):
+        (self.p/'manifest.json').write_text(json.dumps(self.m))
+    def test_source_baseline(self):
+        self.fixture(); self.save(); gate.source_check()
+    def test_unbound_gate_refused(self):
+        self.fixture(); del self.m['files']['gate.py']; self.save()
+        with self.assertRaises(ValueError): gate.source_check()
+    def test_manifest_cannot_claim_kernel_status(self):
+        self.fixture(); self.m['formalization_status']='kernel-checked'; self.save()
+        with self.assertRaises(ValueError): gate.source_check()
+    def test_root_declaration_cannot_evade_audit(self):
+        p=self.fixture(); root=p/'ResearchFormalCoreR1.lean'
+        root.write_text(root.read_text()+'theorem hidden : False := by sorry\n')
+        self.m['files']['ResearchFormalCoreR1.lean']=hashlib.sha256(root.read_bytes()).hexdigest(); self.save()
+        with self.assertRaises(ValueError): gate.source_check()
+    def test_duplicate_json_rejected(self):
+        with self.assertRaises(ValueError): gate.load_json('{"a":1,"a":2}')
+    def test_json_object(self):
+        self.assertEqual(gate.load_json('{"a":1}'), {'a':1})
+
+class RuntimeVersionTests(unittest.TestCase):
+    # These are orchestration tests with synthetic external process results;
+    # source validation, log writes, build deletion and receipts are real.
+    RELEASE = 'Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)'
+
+    def fixture(self):
+        tmp = tempfile.TemporaryDirectory()
+        self.addCleanup(tmp.cleanup)
+        self.root = Path(tmp.name) / 'formal'
+        shutil.copytree(ROOT, self.root, ignore=shutil.ignore_patterns('.lake', '__pycache__'))
+        previous = gate.ROOT
+        gate.ROOT = self.root
+        self.addCleanup(lambda: setattr(gate, 'ROOT', previous))
+        manifest_path = self.root / 'manifest.json'
+        manifest = json.loads(manifest_path.read_text())
+        manifest['files'] = {p.relative_to(self.root).as_posix(): hashlib.sha256(p.read_bytes()).hexdigest()
+                             for p in self.root.rglob('*') if p.is_file() and p.name != 'manifest.json'}
+        manifest_path.write_text(json.dumps(manifest))
+        self.manifest, self.digest = gate.source_check()
+        self.sentinel = self.root / '.lake/build/preserve-before-preflight'
+        self.sentinel.parent.mkdir(parents=True)
+        self.sentinel.write_text('old build')
+        self.calls = []
+        self.version_index = 0
+
+    def execute_synthetic(self, versions, version_exit=0, mutate_source=False, wrong_dependency=False,
+                          dirty_dependency=None, drift_dependency=False, env=None):
+        def external_run(command, **kwargs):
+            self.calls.append(command)
+            if command == ['lake', 'env', 'lean', '--version']:
+                text = versions[min(self.version_index, len(versions) - 1)] + '\n'
+                self.version_index += 1
+                return subprocess.CompletedProcess(command, version_exit, text)
+            if command == ['lake', 'build'] and mutate_source:
+                path = self.root / 'lake-manifest.json'
+                path.write_bytes(path.read_bytes() + b'\n')
+            label = Path(command[-1]).stem
+            if label == 'Audit':
+                text = '\n'.join("'" + n + "' does not depend on any axioms" for n in self.manifest['targets'])
+            elif label in ('false_fold', 'false_power'):
+                return subprocess.CompletedProcess(command, 1, 'unsolved goals\n')
+            elif label in ('sorry', 'custom_imported', 'native'):
+                forbidden = {'sorry': 'sorryAx', 'custom_imported': 'hiddenPremise', 'native': 'injected._nativeDecide_1'}[label]
+                text = "'injected' depends on axioms: [" + forbidden + ']'
+            else:
+                text = ''
+            return subprocess.CompletedProcess(command, 0, text)
+
+        def external_git(command, **kwargs):
+            if command == ['git', 'rev-parse', 'HEAD']:
+                return 'b' * 40 + '\n'
+            name = Path(command[2]).name
+            final_phase = self.version_index >= 2  # after the final version observation
+            if command[3:] == ['status', '--porcelain', '--untracked-files=normal']:
+                dirty = dirty_dependency == 'preflight' and not final_phase or dirty_dependency == 'final' and final_phase
+                return ' M Mathlib/Injected.lean\n' if dirty else ''
+            revision = self.manifest['dependency_revisions'][name]
+            return ('c' * 40 if wrong_dependency or drift_dependency and final_phase else revision) + '\n'
+
+        with patch.object(gate.subprocess, 'run', side_effect=external_run), \
+             patch.object(gate.subprocess, 'check_output', side_effect=external_git), \
+             patch.dict(gate.os.environ, env or {}), \
+             contextlib.redirect_stdout(io.StringIO()):
+            return gate.execute(self.manifest, self.digest)
+
+    def assert_no_receipt(self):
+        self.assertFalse((self.root / '.lake/formal-evidence/receipt.json').exists())
+
+    def test_complete_pinned_release_record(self):
+        self.assertTrue(callable(getattr(gate, 'check_lean_version', None)), 'complete release validator missing')
+        self.assertEqual(gate.check_lean_version(self.RELEASE + '\n'), self.RELEASE)
+
+    def test_other_versions_and_incomplete_or_extra_records_refused(self):
+        self.assertTrue(callable(getattr(gate, 'check_lean_version', None)), 'complete release validator missing')
+        invalid = ['', 'unrelated version 4.34.1 text',
+                   self.RELEASE.replace('4.34.1', '4.34.10'), self.RELEASE.replace('4.34.1', '4.34.100'),
+                   self.RELEASE.replace('4.34.1', '4.34.1-rc1'), self.RELEASE.replace('4.34.1', '4.34.1-nightly'),
+                   'Lean (version 4.34.1,', self.RELEASE.replace(', Release)', ', Debug)'),
+                   'noise\n' + self.RELEASE, self.RELEASE + '\nnoise', self.RELEASE + '\n' + self.RELEASE]
+        for text in invalid:
+            with self.subTest(text=text), self.assertRaisesRegex(ValueError, 'unexpected running Lean version'):
+                gate.check_lean_version(text)
+
+    def test_short_and_other_release_commits_refused(self):
+        # A release label cannot authenticate a truncated or different compiler.
+        for commit in ('a', '5045d005', '0' * 40, 'f' * 40):
+            text = 'Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit ' + commit + ', Release)'
+            with self.subTest(commit=commit), self.assertRaisesRegex(ValueError, 'unexpected running Lean version'):
+                gate.check_lean_version(text)
+
+    def test_other_commit_preflight_preserves_build(self):
+        self.fixture()
+        wrong = 'Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit ' + '0' * 40 + ', Release)'
+        with self.assertRaisesRegex(ValueError, 'unexpected running Lean version'):
+            self.execute_synthetic([wrong])
+        self.assertEqual(self.sentinel.read_bytes(), b'old build')
+        self.assertEqual(self.calls, [['lake', 'env', 'lean', '--version']])
+        self.assert_no_receipt()
+
+    def test_other_commit_after_execution_refuses_receipt(self):
+        self.fixture()
+        wrong = 'Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit ' + 'f' * 40 + ', Release)'
+        with self.assertRaisesRegex(ValueError, 'unexpected running Lean version'):
+            self.execute_synthetic([self.RELEASE, wrong])
+        self.assertEqual(self.version_index, 2)
+        self.assertFalse(self.sentinel.exists())
+        self.assert_no_receipt()
+
+    def test_invalid_preflight_preserves_build_and_runs_no_build(self):
+        self.fixture()
+        with self.assertRaisesRegex(ValueError, 'unexpected running Lean version'):
+            self.execute_synthetic([self.RELEASE.replace('4.34.1', '4.34.10')])
+        self.assertTrue(self.sentinel.exists(), 'preflight refusal deleted the old build')
+        self.assertEqual(self.calls, [['lake', 'env', 'lean', '--version']])
+        self.assert_no_receipt()
+
+    def test_preflight_process_failure_preserves_build(self):
+        self.fixture()
+        with self.assertRaisesRegex(ValueError, 'unexpected process outcome'):
+            self.execute_synthetic([self.RELEASE], version_exit=1)
+        self.assertTrue(self.sentinel.exists(), 'failed preflight deleted the old build')
+        self.assertEqual(self.calls, [['lake', 'env', 'lean', '--version']])
+        self.assert_no_receipt()
+
+    def test_success_checks_before_build_and_after_controls_and_binds_both_logs(self):
+        self.fixture()
+        receipt = self.execute_synthetic([self.RELEASE, self.RELEASE])
+        self.assertEqual(self.calls[0], ['lake', 'env', 'lean', '--version'])
+        self.assertEqual(self.calls[1], ['lake', 'build'])
+        self.assertEqual(self.calls[-1], ['lake', 'env', 'lean', '--version'])
+        self.assertEqual(self.version_index, 2)
+        self.assertFalse(self.sentinel.exists())
+        self.assertEqual(receipt['lean_version'], self.RELEASE)
+        self.assertEqual(receipt['manifest_sha256'], self.digest)
+        self.assertEqual(receipt['checked_commit'], 'b' * 40)  # synthetic Git result
+        self.assertEqual(set(receipt['negative_controls']), {'false_fold', 'false_power', 'sorry', 'custom_imported', 'native'})
+        out = self.root / '.lake/formal-evidence'
+        self.assertEqual(set(receipt['logs']), {p.name for p in out.glob('*.log')})
+        for name in ('version-preflight.log', 'version.log'):
+            self.assertEqual(receipt['logs'][name], hashlib.sha256((out / name).read_bytes()).hexdigest())
+
+    def test_version_change_after_execution_refuses_receipt(self):
+        self.fixture()
+        with self.assertRaisesRegex(ValueError, 'unexpected running Lean version'):
+            self.execute_synthetic([self.RELEASE, self.RELEASE.replace('4.34.1', '4.34.10')])
+        self.assertEqual(self.version_index, 2)
+        self.assert_no_receipt()
+
+    def test_source_change_during_build_still_refuses_receipt(self):
+        self.fixture()
+        with self.assertRaisesRegex(ValueError, 'source hash mismatch: lake-manifest.json'):
+            self.execute_synthetic([self.RELEASE], mutate_source=True)
+        self.assert_no_receipt()
+
+    def test_installed_dependency_change_still_refuses_receipt(self):
+        self.fixture()
+        with self.assertRaisesRegex(ValueError, 'installed dependency HEAD differs from lock'):
+            self.execute_synthetic([self.RELEASE], wrong_dependency=True)
+        self.assert_no_receipt()
+
+class RuntimeGuardTests(unittest.TestCase):
+    # The uniform runtime guard: the exact release, locked and clean dependencies and the bound
+    # sources are observed before the first Lean execution and again after the last one, and the
+    # two observations must be equal. These controls fail on a gate that checks only versions.
+    # Reuses the synthetic-process harness above without re-running its tests.
+    RELEASE = RuntimeVersionTests.RELEASE
+    OTHER_PLATFORM = RELEASE.replace('x86_64-unknown-linux-gnu', 'aarch64-unknown-linux-gnu')
+    fixture = RuntimeVersionTests.fixture
+    execute_synthetic = RuntimeVersionTests.execute_synthetic
+    assert_no_receipt = RuntimeVersionTests.assert_no_receipt
+
+    def test_dirty_dependency_before_execution_refuses_and_preserves_build(self):
+        self.fixture()
+        with self.assertRaisesRegex(ValueError, 'dependency worktree is not clean'):
+            self.execute_synthetic([self.RELEASE, self.RELEASE], dirty_dependency='preflight')
+        self.assertEqual(self.calls, [['lake', 'env', 'lean', '--version']])
+        self.assertTrue(self.sentinel.exists(), 'preflight refusal deleted the old build')
+        self.assert_no_receipt()
+
+    def test_wrong_dependency_before_execution_refuses_and_preserves_build(self):
+        self.fixture()
+        with self.assertRaisesRegex(ValueError, 'installed dependency HEAD differs from lock'):
+            self.execute_synthetic([self.RELEASE, self.RELEASE], wrong_dependency=True)
+        self.assertEqual(self.calls, [['lake', 'env', 'lean', '--version']])
+        self.assertTrue(self.sentinel.exists(), 'preflight refusal deleted the old build')
+        self.assert_no_receipt()
+
+    def test_dependency_dirtied_during_execution_refuses_receipt(self):
+        self.fixture()
+        with self.assertRaisesRegex(ValueError, 'dependency worktree is not clean'):
+            self.execute_synthetic([self.RELEASE, self.RELEASE], dirty_dependency='final')
+        self.assertEqual(self.version_index, 2)
+        self.assert_no_receipt()
+
+    def test_dependency_moved_during_execution_refuses_receipt(self):
+        self.fixture()
+        with self.assertRaisesRegex(ValueError, 'installed dependency HEAD differs from lock'):
+            self.execute_synthetic([self.RELEASE, self.RELEASE], drift_dependency=True)
+        self.assertEqual(self.version_index, 2)
+        self.assert_no_receipt()
+
+    def test_runtime_changed_between_observations_refuses_receipt(self):
+        # Both lines are well-formed records of the pinned release; only the platform differs.
+        self.fixture()
+        self.assertEqual(gate.check_lean_version(self.OTHER_PLATFORM), self.OTHER_PLATFORM)
+        with self.assertRaisesRegex(ValueError, 'changed during execution'):
+            self.execute_synthetic([self.RELEASE, self.OTHER_PLATFORM])
+        self.assert_no_receipt()
+
+    def test_receipt_binds_attempt_and_both_equal_observations(self):
+        self.fixture()
+        receipt = self.execute_synthetic([self.RELEASE, self.RELEASE],
+                                         env={'GITHUB_RUN_ID': '12345', 'GITHUB_RUN_ATTEMPT': '2'})
+        self.assertEqual(receipt['workflow_run_id'], '12345')
+        self.assertEqual(receipt['workflow_run_attempt'], '2')
+        self.assertEqual(receipt['dependency_worktrees'], 'CLEAN')
+        expected = {'lean_version': self.RELEASE, 'dependency_revisions': self.manifest['dependency_revisions'],
+                    'dependency_worktrees': 'CLEAN', 'manifest_sha256': self.digest}
+        self.assertEqual(receipt['observations'], {'preflight': expected, 'final': expected})
+        written = json.loads((self.root / '.lake/formal-evidence/receipt.json').read_text())
+        self.assertEqual(written['observations'], receipt['observations'])
+
+class SuccessorTests(unittest.TestCase):
+    def test_only_documented_algebra_repairs(self):
+        original=(ROOT/'originals/Algebra.lean.txt').read_text()
+        expected=original.replace('def foldPotential', 'noncomputable def foldPotential').replace('  field_simp [hr]\n  ring\n', '  field_simp [hr]\n')
+        self.assertEqual((ROOT/'ResearchFormalCoreR1/AlgebraV2.lean').read_text(), expected.replace("import Mathlib\n", 'import Mathlib.Basic.Real.Basic\nimport Mathlib.Tactic.FieldSimp\nimport Mathlib.Tactic.Ring\nimport Mathlib.Tactic.NormNum\n'))
+    def test_only_documented_probability_repair(self):
+        original=(ROOT/'originals/ProbabilityCompanions.lean.txt').read_text()
+        expected=original.replace('  field_simp [hr, hcZ]\n  ring\n', '  field_simp [hr, hcZ]\n')
+        self.assertEqual((ROOT/'ResearchFormalCoreR1/ProbabilityCompanionsV2.lean').read_text(), expected.replace("import Mathlib\n", 'import Mathlib.Analysis.Real.Sqrt\nimport Mathlib.Tactic.FieldSimp\nimport Mathlib.Tactic.Ring\nimport Mathlib.Tactic.NormNum\nimport Mathlib.Tactic.Positivity\nimport Mathlib.Tactic.Linarith\n'))
+
+if __name__ == '__main__': unittest.main()