From deb28a751f620715ec65d3bd73690905e6fee94d Mon Sep 17 00:00:00 2001 From: Dylan Roy <8n96mrd5d4@privaterelay.appleid.com> Date: Sun, 25 Oct 2026 20:02:37 +0000 Subject: [PATCH 1/4] Prove exact P02-LM-002 endpoint determinant moment bound --- .../determinant_moment_20261025/.gitignore | 2 + .../COMPATIBILITY.md | 15 + .../determinant_moment_20261025/GLOSSARY.md | 7 + .../LINEAGE_VALIDATION.md | 76 ++++ .../determinant_moment_20261025/README.md | 32 ++ .../ResearchFormalCoreR1.lean | 3 + .../ResearchFormalCoreR1/AlgebraV2.lean | 50 +++ .../DeterminantMoment.lean | 207 ++++++++++ .../ProbabilityCompanionsV2.lean | 88 +++++ .../determinant_moment_20261025/SCOPE.md | 29 ++ .../determinant_moment_20261025/SOURCE_MAP.md | 46 +++ .../blueprint/src/content.tex | 5 + .../controls/false_omit_q.lean.txt | 6 + .../controls/false_r6.lean.txt | 6 + .../evidence/history/dm2-baseline-tests.log | 83 ++++ .../evidence/history/dm2-compile-01.log | 1 + .../evidence/history/dm2-compile-02.log | 214 ++++++++++ .../evidence/history/dm2-compile-03.log | 16 + .../evidence/history/dm2-compile-04.log | 0 .../evidence/history/dm2-target-first.log | 15 + frontiers/determinant_moment_20261025/gate.py | 262 +++++++++++++ .../lake-manifest.json | 117 ++++++ .../determinant_moment_20261025/lakefile.toml | 11 + .../lean-toolchain | 1 + .../determinant_moment_20261025/manifest.json | 78 ++++ .../originals/Algebra.lean.txt | 51 +++ .../originals/ProbabilityCompanions.lean.txt | 89 +++++ .../tests/test_alignment_lineage.py | 181 +++++++++ .../tests/test_gate.py | 370 ++++++++++++++++++ 29 files changed, 2061 insertions(+) create mode 100644 frontiers/determinant_moment_20261025/.gitignore create mode 100644 frontiers/determinant_moment_20261025/COMPATIBILITY.md create mode 100644 frontiers/determinant_moment_20261025/GLOSSARY.md create mode 100644 frontiers/determinant_moment_20261025/LINEAGE_VALIDATION.md create mode 100644 frontiers/determinant_moment_20261025/README.md create mode 100644 frontiers/determinant_moment_20261025/ResearchFormalCoreR1.lean create mode 100644 frontiers/determinant_moment_20261025/ResearchFormalCoreR1/AlgebraV2.lean create mode 100644 frontiers/determinant_moment_20261025/ResearchFormalCoreR1/DeterminantMoment.lean create mode 100644 frontiers/determinant_moment_20261025/ResearchFormalCoreR1/ProbabilityCompanionsV2.lean create mode 100644 frontiers/determinant_moment_20261025/SCOPE.md create mode 100644 frontiers/determinant_moment_20261025/SOURCE_MAP.md create mode 100644 frontiers/determinant_moment_20261025/blueprint/src/content.tex create mode 100644 frontiers/determinant_moment_20261025/controls/false_omit_q.lean.txt create mode 100644 frontiers/determinant_moment_20261025/controls/false_r6.lean.txt create mode 100644 frontiers/determinant_moment_20261025/evidence/history/dm2-baseline-tests.log create mode 100644 frontiers/determinant_moment_20261025/evidence/history/dm2-compile-01.log create mode 100644 frontiers/determinant_moment_20261025/evidence/history/dm2-compile-02.log create mode 100644 frontiers/determinant_moment_20261025/evidence/history/dm2-compile-03.log create mode 100644 frontiers/determinant_moment_20261025/evidence/history/dm2-compile-04.log create mode 100644 frontiers/determinant_moment_20261025/evidence/history/dm2-target-first.log create mode 100644 frontiers/determinant_moment_20261025/gate.py create mode 100644 frontiers/determinant_moment_20261025/lake-manifest.json create mode 100644 frontiers/determinant_moment_20261025/lakefile.toml create mode 100644 frontiers/determinant_moment_20261025/lean-toolchain create mode 100644 frontiers/determinant_moment_20261025/manifest.json create mode 100644 frontiers/determinant_moment_20261025/originals/Algebra.lean.txt create mode 100644 frontiers/determinant_moment_20261025/originals/ProbabilityCompanions.lean.txt create mode 100644 frontiers/determinant_moment_20261025/tests/test_alignment_lineage.py create mode 100644 frontiers/determinant_moment_20261025/tests/test_gate.py 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..47052c7b6 --- /dev/null +++ b/frontiers/determinant_moment_20261025/COMPATIBILITY.md @@ -0,0 +1,15 @@ +# 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. 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..4682dc03a --- /dev/null +++ b/frontiers/determinant_moment_20261025/README.md @@ -0,0 +1,32 @@ +# Exact endpoint-Hessian determinant second moment + +P02-LM-002: for the source's exact nine-jet endpoint convention and 0 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..57adcc3d1 --- /dev/null +++ b/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/ProbabilityCompanionsV2.lean @@ -0,0 +1,88 @@ +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] + +/-- 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..3c8d30a1a --- /dev/null +++ b/frontiers/determinant_moment_20261025/SCOPE.md @@ -0,0 +1,29 @@ +# 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` 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 ` 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-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/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..f27c2efba --- /dev/null +++ b/frontiers/determinant_moment_20261025/manifest.json @@ -0,0 +1,78 @@ +{ + "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": "33721aad32f82131a6956a06b58c5bc41f5d28f26efe840a99a4d51ad60cf247", + "gate.py": "25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a", + "ResearchFormalCoreR1.lean": "7fd8b5fee3db0847b52e01d7cb2515b7a9e77846f4c5db8b8277ef46084a6610", + "lean-toolchain": "d5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b", + "lakefile.toml": "d629891716c169404d1f0d76492441c8dd66f1e790b1b8b0819e51c8d5059255", + "README.md": "292bfc8cf96b5beb2748b7c557a512bca002522a5f79930c857d5e29df417740", + ".gitignore": "b34af236d1df9e39ed4f98fca51702530ce76bdee4e1a69512f6caed933c3374", + "SCOPE.md": "7d8c3205bf1d382cb069aec38b7754a44af540e411762507e889eb61239ead4e", + "SOURCE_MAP.md": "1d21d9d283047a2bbaceec402e2af0009b2b53e3eb3c4fa47654b73bc748460e", + "GLOSSARY.md": "3cd098f26e3020b780307617fc65c53ed040789d54ea53930c5fa21524bc7323", + "ResearchFormalCoreR1/ProbabilityCompanionsV2.lean": "338452a0c2ba24d016059354d543cc995b8cb29c9d4a41d98bb93499f5f8cb8f", + "ResearchFormalCoreR1/DeterminantMoment.lean": "c12731c88cd7c7dee32b2cb59b3a4eb5016f2b59a96e3cda4b523632a0bf61c4", + "ResearchFormalCoreR1/AlgebraV2.lean": "4480708263c40a2f7f03f12ef7e15f0eb4f8193c2dccbb253921a7ec251863c3", + "originals/ProbabilityCompanions.lean.txt": "4ace6600a476859982c8851ae9097c89b082d3c96291b3c8330bd4cc00bae65d", + "originals/Algebra.lean.txt": "4c196820c4db8fafc288dd35642828ba577e3544d60aba7d1d6d24f14ad1e8ae", + "tests/test_gate.py": "e279e5b1e8c14f913728a18fa345dd1060d856799369fc4c9dce4a5f6dfb7574", + "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-compile-04.log": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "evidence/history/dm2-baseline-tests.log": "00c70d818d406bcca228ad07644d2307ed6ab61a3b2582c40d9cb89edb67749e", + "evidence/history/dm2-compile-02.log": "1a298e7d92c2376be92fce08f0993d0ee48e822a4c098c7b84b64539158e91cc", + "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..e031f0b9b --- /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) + 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) + +if __name__ == '__main__': unittest.main() From dcfc89366f590342b4cd30b141a22c9ae2a562bb Mon Sep 17 00:00:00 2001 From: Dylan Roy <8n96mrd5d4@privaterelay.appleid.com> Date: Sun, 25 Oct 2026 20:06:42 +0000 Subject: [PATCH 2/4] Reduce only imports after recorded kernel replay memory failure --- .../COMPATIBILITY.md | 7 ++ .../determinant_moment_20261025/README.md | 9 +- .../ResearchFormalCoreR1/AlgebraV2.lean | 5 +- .../DeterminantMoment.lean | 13 +- .../ProbabilityCompanionsV2.lean | 7 +- .../determinant_moment_20261025/SCOPE.md | 10 +- .../determinant_moment_20261025/SOURCE_MAP.md | 19 +++ .../evidence/DM2_NONAUTHOR_REVIEW.md | 117 ++++++++++++++++++ .../evidence/history/dm2-narrow-build-01.log | 87 +++++++++++++ .../evidence/history/dm2-narrow-build-02.log | 17 +++ .../evidence/history/dm2-narrow-red.log | 78 ++++++++++++ .../history/umbrella-mathlib-oom/RESULT.txt | 1 + .../history/umbrella-mathlib-oom/build.log | 17 +++ .../umbrella-mathlib-oom/leanchecker.log | 0 .../version-preflight.log | 1 + .../determinant_moment_20261025/manifest.json | 23 ++-- .../tests/test_gate.py | 4 +- 17 files changed, 399 insertions(+), 16 deletions(-) create mode 100644 frontiers/determinant_moment_20261025/evidence/DM2_NONAUTHOR_REVIEW.md create mode 100644 frontiers/determinant_moment_20261025/evidence/history/dm2-narrow-build-01.log create mode 100644 frontiers/determinant_moment_20261025/evidence/history/dm2-narrow-build-02.log create mode 100644 frontiers/determinant_moment_20261025/evidence/history/dm2-narrow-red.log create mode 100644 frontiers/determinant_moment_20261025/evidence/history/umbrella-mathlib-oom/RESULT.txt create mode 100644 frontiers/determinant_moment_20261025/evidence/history/umbrella-mathlib-oom/build.log create mode 100644 frontiers/determinant_moment_20261025/evidence/history/umbrella-mathlib-oom/leanchecker.log create mode 100644 frontiers/determinant_moment_20261025/evidence/history/umbrella-mathlib-oom/version-preflight.log diff --git a/frontiers/determinant_moment_20261025/COMPATIBILITY.md b/frontiers/determinant_moment_20261025/COMPATIBILITY.md index 47052c7b6..629825c5e 100644 --- a/frontiers/determinant_moment_20261025/COMPATIBILITY.md +++ b/frontiers/determinant_moment_20261025/COMPATIBILITY.md @@ -13,3 +13,10 @@ The actual first hosted run, 36351673121, on Math- commit 9cc0fff64b5e48b48b1ebc 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/README.md b/frontiers/determinant_moment_20261025/README.md index 4682dc03a..0b9eae248 100644 --- a/frontiers/determinant_moment_20261025/README.md +++ b/frontiers/determinant_moment_20261025/README.md @@ -9,7 +9,7 @@ Concrete Gaussian moments, endpoint identification, normalizer and parent result 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 targets. It does not modify the occupied core gate +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. @@ -30,3 +30,10 @@ A nonauthor same-provider source review is recorded separately and does not sati 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/AlgebraV2.lean b/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/AlgebraV2.lean index a8b42432c..768d0bab9 100644 --- a/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/AlgebraV2.lean +++ b/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/AlgebraV2.lean @@ -1,4 +1,7 @@ -import Mathlib +import Mathlib.Basic.Real.Basic +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Ring +import Mathlib.Tactic.NormNum namespace ResearchFormalCoreR1 diff --git a/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/DeterminantMoment.lean b/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/DeterminantMoment.lean index 5eac3c6c0..93e296ca1 100644 --- a/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/DeterminantMoment.lean +++ b/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/DeterminantMoment.lean @@ -1,4 +1,15 @@ -import Mathlib +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 diff --git a/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/ProbabilityCompanionsV2.lean b/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/ProbabilityCompanionsV2.lean index 57adcc3d1..e4073dc21 100644 --- a/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/ProbabilityCompanionsV2.lean +++ b/frontiers/determinant_moment_20261025/ResearchFormalCoreR1/ProbabilityCompanionsV2.lean @@ -1,4 +1,9 @@ -import Mathlib +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 diff --git a/frontiers/determinant_moment_20261025/SCOPE.md b/frontiers/determinant_moment_20261025/SCOPE.md index 3c8d30a1a..0a3e15e04 100644 --- a/frontiers/determinant_moment_20261025/SCOPE.md +++ b/frontiers/determinant_moment_20261025/SCOPE.md @@ -12,8 +12,7 @@ The complete preimplementation source binding is SOURCE_MAP.md and remains bound | dm2_moment | Sections 2–3: measurable nine-jet map, integrable eighth radius power, integral<=M8, 0= 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/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/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/manifest.json b/frontiers/determinant_moment_20261025/manifest.json index f27c2efba..71a692415 100644 --- a/frontiers/determinant_moment_20261025/manifest.json +++ b/frontiers/determinant_moment_20261025/manifest.json @@ -42,31 +42,38 @@ "files": { "LINEAGE_VALIDATION.md": "bba9d0a859f1ba45670fe122e4e72ae1094a2226de98aa814d838b0baaf61815", "lake-manifest.json": "d63753befccc21923783a5085148e3ff028d97134ea52f5a08bd87ecf1b0b043", - "COMPATIBILITY.md": "33721aad32f82131a6956a06b58c5bc41f5d28f26efe840a99a4d51ad60cf247", + "COMPATIBILITY.md": "216b772d417ce273499b692481f3c4e6e1f499c67ff41cb92f008a9b9bf09513", "gate.py": "25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a", "ResearchFormalCoreR1.lean": "7fd8b5fee3db0847b52e01d7cb2515b7a9e77846f4c5db8b8277ef46084a6610", "lean-toolchain": "d5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b", "lakefile.toml": "d629891716c169404d1f0d76492441c8dd66f1e790b1b8b0819e51c8d5059255", - "README.md": "292bfc8cf96b5beb2748b7c557a512bca002522a5f79930c857d5e29df417740", + "README.md": "739acd26766ae9e883c9bdb1912096187f8b78e630ba59b960effdd84aa7c395", ".gitignore": "b34af236d1df9e39ed4f98fca51702530ce76bdee4e1a69512f6caed933c3374", - "SCOPE.md": "7d8c3205bf1d382cb069aec38b7754a44af540e411762507e889eb61239ead4e", - "SOURCE_MAP.md": "1d21d9d283047a2bbaceec402e2af0009b2b53e3eb3c4fa47654b73bc748460e", + "SCOPE.md": "c3cb56539a6b1dcb41c6ac378c1797e95ef878ba03276456276e0bb3abfa3ddd", + "SOURCE_MAP.md": "32b5e48e9d8150927542718e719a71f6d59ef7593b78dd827dd52c18c47681f6", "GLOSSARY.md": "3cd098f26e3020b780307617fc65c53ed040789d54ea53930c5fa21524bc7323", - "ResearchFormalCoreR1/ProbabilityCompanionsV2.lean": "338452a0c2ba24d016059354d543cc995b8cb29c9d4a41d98bb93499f5f8cb8f", - "ResearchFormalCoreR1/DeterminantMoment.lean": "c12731c88cd7c7dee32b2cb59b3a4eb5016f2b59a96e3cda4b523632a0bf61c4", - "ResearchFormalCoreR1/AlgebraV2.lean": "4480708263c40a2f7f03f12ef7e15f0eb4f8193c2dccbb253921a7ec251863c3", + "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": "e279e5b1e8c14f913728a18fa345dd1060d856799369fc4c9dce4a5f6dfb7574", + "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": { diff --git a/frontiers/determinant_moment_20261025/tests/test_gate.py b/frontiers/determinant_moment_20261025/tests/test_gate.py index e031f0b9b..781531251 100644 --- a/frontiers/determinant_moment_20261025/tests/test_gate.py +++ b/frontiers/determinant_moment_20261025/tests/test_gate.py @@ -361,10 +361,10 @@ 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) + 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) + 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() From 144f371fd5a7990f4d53db01ad8f76dbeba45b4a Mon Sep 17 00:00:00 2001 From: Dylan Roy <8n96mrd5d4@privaterelay.appleid.com> Date: Sun, 25 Oct 2026 20:09:26 +0000 Subject: [PATCH 3/4] Deliver exact local kernel replay and nonauthor source review --- .../evidence/DELIVERY.md | 102 +++++ .../evidence/DM2_IMPORT_SUCCESSOR_REVIEW.md | 104 +++++ .../evidence/final/Audit.lean.txt | 19 + .../evidence/final/EXPORT_IDENTITIES.json | 116 +++++ .../evidence/final/Types.lean.txt | 20 + .../evidence/final/axioms.log | 18 + .../evidence/final/build.log | 17 + .../evidence/final/custom_imported.lean.txt | 5 + .../evidence/final/custom_imported.log | 1 + .../evidence/final/dm2_extra_controls.json | 30 ++ .../evidence/final/dm2_false_omit_q.lean.txt | 6 + .../evidence/final/dm2_false_omit_q.log | 2 + .../evidence/final/dm2_false_r6.lean.txt | 6 + .../evidence/final/dm2_false_r6.log | 2 + .../evidence/final/elaborated-types.log | 432 ++++++++++++++++++ .../evidence/final/false_fold.lean.txt | 3 + .../evidence/final/false_fold.log | 2 + .../evidence/final/false_power.lean.txt | 3 + .../evidence/final/false_power.log | 2 + .../evidence/final/gate-terminal.log | 181 ++++++++ .../evidence/final/leanchecker.log | 0 .../evidence/final/native.lean.txt | 3 + .../evidence/final/native.log | 1 + .../evidence/final/receipt.json | 170 +++++++ .../evidence/final/sorry.lean.txt | 3 + .../evidence/final/sorry.log | 2 + .../evidence/final/tests-normal.log | 83 ++++ .../evidence/final/tests-optimized.log | 83 ++++ .../evidence/final/version-preflight.log | 1 + .../evidence/final/version.log | 1 + 30 files changed, 1418 insertions(+) create mode 100644 frontiers/determinant_moment_20261025/evidence/DELIVERY.md create mode 100644 frontiers/determinant_moment_20261025/evidence/DM2_IMPORT_SUCCESSOR_REVIEW.md create mode 100644 frontiers/determinant_moment_20261025/evidence/final/Audit.lean.txt create mode 100644 frontiers/determinant_moment_20261025/evidence/final/EXPORT_IDENTITIES.json create mode 100644 frontiers/determinant_moment_20261025/evidence/final/Types.lean.txt create mode 100644 frontiers/determinant_moment_20261025/evidence/final/axioms.log create mode 100644 frontiers/determinant_moment_20261025/evidence/final/build.log create mode 100644 frontiers/determinant_moment_20261025/evidence/final/custom_imported.lean.txt create mode 100644 frontiers/determinant_moment_20261025/evidence/final/custom_imported.log create mode 100644 frontiers/determinant_moment_20261025/evidence/final/dm2_extra_controls.json create mode 100644 frontiers/determinant_moment_20261025/evidence/final/dm2_false_omit_q.lean.txt create mode 100644 frontiers/determinant_moment_20261025/evidence/final/dm2_false_omit_q.log create mode 100644 frontiers/determinant_moment_20261025/evidence/final/dm2_false_r6.lean.txt create mode 100644 frontiers/determinant_moment_20261025/evidence/final/dm2_false_r6.log create mode 100644 frontiers/determinant_moment_20261025/evidence/final/elaborated-types.log create mode 100644 frontiers/determinant_moment_20261025/evidence/final/false_fold.lean.txt create mode 100644 frontiers/determinant_moment_20261025/evidence/final/false_fold.log create mode 100644 frontiers/determinant_moment_20261025/evidence/final/false_power.lean.txt create mode 100644 frontiers/determinant_moment_20261025/evidence/final/false_power.log create mode 100644 frontiers/determinant_moment_20261025/evidence/final/gate-terminal.log create mode 100644 frontiers/determinant_moment_20261025/evidence/final/leanchecker.log create mode 100644 frontiers/determinant_moment_20261025/evidence/final/native.lean.txt create mode 100644 frontiers/determinant_moment_20261025/evidence/final/native.log create mode 100644 frontiers/determinant_moment_20261025/evidence/final/receipt.json create mode 100644 frontiers/determinant_moment_20261025/evidence/final/sorry.lean.txt create mode 100644 frontiers/determinant_moment_20261025/evidence/final/sorry.log create mode 100644 frontiers/determinant_moment_20261025/evidence/final/tests-normal.log create mode 100644 frontiers/determinant_moment_20261025/evidence/final/tests-optimized.log create mode 100644 frontiers/determinant_moment_20261025/evidence/final/version-preflight.log create mode 100644 frontiers/determinant_moment_20261025/evidence/final/version.log 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_