From c0e56020285291aff14152a389a0df37f37c325b Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Sun, 27 Sep 2026 21:43:07 +0000 Subject: [PATCH 1/3] Add Layer 1 formal verification pilot: Lean 4 SIDE24 arithmetic ledger, registry, fail-closed gate - formal/: dependency-free Lean 4 (v4.34.1) library; 31 kernel-checked, axiom-free theorems covering every exact integer/rational identity and inequality in sections 1-4 of the SIDE24 coefficient note, plus the published ENCLOSURE.json endpoints. Analytic content is explicitly not formalised. - formal/registry.json: per-claim formalization status (none/specified/proved/kernel-checked), byte-pinned informal anchors, Lean file hashes, allowed/forbidden axiom lists, alignment-review lane. scientific_status_authority: false. - formal/sources/: byte copies of Math-@9d7b6802 PROOF.md and ENCLOSURE.json. - tools/formal_gate_check.py: fail-closed gate (hashes, unregistered files, sorry/native_decide/axiom scan, anchors, declarations, #print axioms audit). - tests/test_formal_gate.py: 38 controls incl. Lean mutants rejected by kernel. Co-authored-by: Dylan Roy --- .gitignore | 1 + formal/ALIGNMENT.md | 47 ++ formal/UniversalLaw.lean | 13 + formal/UniversalLaw/Audit.lean | 54 ++ formal/UniversalLaw/Side24/ConeMoments.lean | 85 ++ formal/UniversalLaw/Side24/Endpoints.lean | 41 + formal/UniversalLaw/Side24/Ledger.lean | 141 ++++ formal/lake-manifest.json | 6 + formal/lakefile.toml | 11 + formal/lean-toolchain | 1 + formal/registry.json | 828 ++++++++++++++++++++ formal/sources/side24_v1/ENCLOSURE.json | 29 + formal/sources/side24_v1/PROOF.md | 216 +++++ tests/test_formal_gate.py | 348 ++++++++ tools/formal_gate_check.py | 399 ++++++++++ 15 files changed, 2220 insertions(+) create mode 100644 formal/ALIGNMENT.md create mode 100644 formal/UniversalLaw.lean create mode 100644 formal/UniversalLaw/Audit.lean create mode 100644 formal/UniversalLaw/Side24/ConeMoments.lean create mode 100644 formal/UniversalLaw/Side24/Endpoints.lean create mode 100644 formal/UniversalLaw/Side24/Ledger.lean create mode 100644 formal/lake-manifest.json create mode 100644 formal/lakefile.toml create mode 100644 formal/lean-toolchain create mode 100644 formal/registry.json create mode 100644 formal/sources/side24_v1/ENCLOSURE.json create mode 100644 formal/sources/side24_v1/PROOF.md create mode 100644 tests/test_formal_gate.py create mode 100644 tools/formal_gate_check.py diff --git a/.gitignore b/.gitignore index 7a60b85e1..5a55daf61 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ __pycache__/ *.pyc +.lake/ diff --git a/formal/ALIGNMENT.md b/formal/ALIGNMENT.md new file mode 100644 index 000000000..cdf80501b --- /dev/null +++ b/formal/ALIGNMENT.md @@ -0,0 +1,47 @@ +# Informal–formal alignment table + +Generated from `formal/registry.json` by `tools/formal_gate_check.py --write-alignment`; do not hand-edit. +Each row pairs one Lean declaration with the verbatim informal text it is attached to. The kernel checks the +declaration; the alignment review lane checks that the declaration says what the anchor says. Status here is +formalization status only and changes no Layer 0 review outcome. + +| Claim | Layer 0 object | Status | Alignment | Lean declaration | Informal anchor | Does not claim | +|---|---|---|---|---|---|---| +| side24-pairing-sum-six | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.pairing_sum_six` | `The coefficient sum for q=6 is 1+15+45+15=76` | the derivative bound 76\|x\|^6 e^(-\|x\|^2/2) itself | +| side24-pairing-sum-lower-orders | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.pairing_sum_le_six` | `it bounds the smaller orders as well` | the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem | +| side24-pairing-terms | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.pairing_terms_six` | `1+15+45+15=76` | the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem | +| side24-sixth-moment | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.sixth_moment_double_factorial` | `At zero, every such contraction has absolute value at most15.` | that Gaussian derivative contractions at zero are bounded by 15 | +| side24-lattice-shell | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.lattice_shell_constant` | `<=729 sum_{j>=1} j^9 e^(-288j^2) <=1458 e^(-288).` | the lattice-point count or the geometric tail sum | +| side24-geometric-ratio | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.geometric_ratio_constants` | `successive terms have ratio at most512e^(-864)<1/2` | that the ratio is below 1/2 | +| side24-period-exponent | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.period_exponent` | `sum_{n!=0} \|n\|^6 e^(-288\|n\|^2)` | the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem | +| side24-image-constant | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.image_constant_value` | `E := 1458*(76*24^6+15)*10^(-125) = 21175738586478 *10^(-125).` | the inequality \|D^q K_24(0)-D^q K_infty(0)\| < E | +| side24-exp-taylor | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.exp_taylor_partial_sum_gt_ten` | `The code proves e^(288/125)>10 using the positive rational Taylor sum through20` | that the partial sum is below exp(288/125) (positivity of the omitted terms is analysis) | +| side24-covariance-bound | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.covariance_relative_bound` | `epsilon=10^(-108), since60E= I/3 | +| side24-odd-block-eigen | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.odd_block_eigenvalues` | `[[1,-3],[-3,15]], whose eigenvalues are8 +/- sqrt(58)` | the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem | +| side24-odd-block-shift | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.odd_block_shifted_minors` | `subtract I/3 and use first principal minor2/3 and determinant7/9` | Sylvester's criterion | +| side24-eigen-third | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.smaller_eigenvalue_exceeds_third` | `Its smaller eigenvalue exceeds 1/3` | monotonicity of the square root | +| side24-exponent-bounds | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.exponent_bounds` | `For d=2,3, a+2b<14 and2a+b<13.` | the log/exp estimates that follow | +| side24-exponent-values | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.exponent_values` | `a=m+2/3+n/2, b=d+n/2.` | the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem | +| side24-ratio-constants | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.ratio_constant_ordering` | `ratio between1-13epsilon and 1+28epsilon, hence safely between1-32epsilon and1+32epsilon` | the elementary log/exp bounds | +| side24-density-comparison | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.density_comparison_below_reported` | `\|c_d,24/c_d,ref -1\| < 10^(-106), d=2,3.` | the multiplicative density comparison | +| side24-tau-squared | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.conditional_third_derivative_variance` | `Var(t)=15, Cov(t,G)=(-3,0,...,0)` | the Gaussian conditioning formula or the covariance derivatives | +| side24-transverse-covariance | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.transverse_covariance_entries_thirds` | `Cov(A_ij,A_kl \| V=0) = (2/3)delta_ij delta_kl + delta_ik delta_jl + delta_il delta_jk.` | the delta formula itself | +| side24-cone-m1 | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.cone_moment_m1_thirds` | `D_1=E[A^2 1{A<0}]=4/3.` | centred Gaussian symmetry | +| side24-trace-variance | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.trace_and_traceless_variances` | `Var(s)=5/3 and Var(x)=Var(y)=1.` | independence beyond zero covariance, which is Gaussian | +| side24-fourth-moment | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.fourth_moment_of_trace` | `E s^2=5/3, E s^4=25/3` | the Gaussian fourth-moment identity | +| side24-exp-moment | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.exponential_moment_of_trace` | `E exp(-s^2/2)=sqrt(3/8)` | the Gaussian exponential-moment identity | +| side24-cone-m2 | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.cone_moment_m2_algebra` | `D_2 = (1/2)[25/3-20/3+8-8sqrt(3/8)] = 29/6-sqrt(6).` | the integral identity or the Rayleigh cone integration | +| side24-cube-root | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.cube_root_simplification` | `simplifying 6^(2/3)/24^(1/3)=(3/2)^(1/3)` | the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem | +| side24-pin-dimension | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.pin_determinant_and_joint_dimension` | `Its dimension is at most10.` | the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem | +| side24-hessian-eigen | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.hessian_block_eigenvalues` | `The reference Hessian block has eigenvalues d+2 on trace and2 on traceless matrices` | the spectral decomposition | +| side24-d2-endpoints | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.d2_endpoints_adjacent` | `"2": { "lower": "0.07340691930603427103", "upper": "0.07340691930603427104"` | that c_2,24 lies between them | +| side24-d3-endpoints | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.d3_endpoints_adjacent` | `"3": { "lower": "0.04177593184059834334", "upper": "0.04177593184059834335"` | that c_3,24 lies between them | +| side24-d3-below-d2 | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.d3_below_d2` | `"scientific_acceptance": false` | anything about the true coefficients | +| side24-endpoints-range | D3 — SIDE24 coefficient calculation | kernel-checked | open | `UniversalLaw.Side24.endpoints_in_unit_tenth` | `"relative_periodization_bound": "1e-106"` | anything about the true coefficients | +| d3-side24-coefficient-bound | D3 — SIDE24 coefficient calculation | none | not-applicable | — | — | any formal verification; Layer 0 review status is unchanged | +| d2-lifetime-remainder | D2 — unrestricted lifetime remainder | none | not-applicable | — | — | any formal verification; Layer 0 review status is unchanged | +| d4-fixed-remote-rn-count | D4 — fixed-remote RN count theorem | none | not-applicable | — | — | any formal verification; Layer 0 review status is unchanged | +| d6-p15-full-price | D6 — P15 full-price theorem | none | not-applicable | — | — | any formal verification; Layer 0 review status is unchanged | +| d1-parent-selection-chain | D1 — parent quantitative Theorem-A selection chain | none | not-applicable | — | — | any formal verification; Layer 0 review status is unchanged | +| d5-pin-neighborhoods | D5 — pin neighborhoods / microdisk | none | not-applicable | — | — | any formal verification; Layer 0 review status is unchanged | +| sard-g-a1-a6 | SARD-G A1/A6 | none | not-applicable | — | — | any formal verification; Layer 0 review status is unchanged | diff --git a/formal/UniversalLaw.lean b/formal/UniversalLaw.lean new file mode 100644 index 000000000..8eb549e25 --- /dev/null +++ b/formal/UniversalLaw.lean @@ -0,0 +1,13 @@ +import UniversalLaw.Side24.Ledger +import UniversalLaw.Side24.ConeMoments +import UniversalLaw.Side24.Endpoints + +/-! +# Universal Law — formal layer (Layer 1) + +Root module of the dependency-free Lean 4 library. Each imported module is +kernel-checked by `lake build`; `UniversalLaw/Audit.lean` prints the axioms +each registered declaration depends on, and `tools/formal_gate_check.py` +refuses any declaration that is registered as `kernel-checked` but uses an +axiom outside the allow-list, `sorryAx`, or `Lean.ofReduceBool`. +-/ diff --git a/formal/UniversalLaw/Audit.lean b/formal/UniversalLaw/Audit.lean new file mode 100644 index 000000000..9eefaec3a --- /dev/null +++ b/formal/UniversalLaw/Audit.lean @@ -0,0 +1,54 @@ +import UniversalLaw + +/-! +# Axiom audit + +Run after `lake build`: + + lake env lean UniversalLaw/Audit.lean + +Every declaration registered in `formal/registry.json` with status +`kernel-checked` or `proved` must appear below. `tools/formal_gate_check.py` +parses the output and fails closed if a registered declaration is missing, or +depends on `sorryAx`, `Lean.ofReduceBool`, or any axiom outside the allow-list +(`propext`, `Classical.choice`, `Quot.sound`). +-/ + +open UniversalLaw.Side24 + +-- Ledger.lean +#print axioms pairing_sum_six +#print axioms pairing_sum_le_six +#print axioms pairing_terms_six +#print axioms sixth_moment_double_factorial +#print axioms lattice_shell_constant +#print axioms geometric_ratio_constants +#print axioms period_exponent +#print axioms image_constant_value +#print axioms exp_taylor_partial_sum_gt_ten +#print axioms covariance_relative_bound +#print axioms odd_block_eigenvalues +#print axioms odd_block_shifted_minors +#print axioms smaller_eigenvalue_exceeds_third +#print axioms exponent_bounds +#print axioms exponent_values +#print axioms ratio_constant_ordering +#print axioms density_comparison_below_reported + +-- ConeMoments.lean +#print axioms conditional_third_derivative_variance +#print axioms transverse_covariance_entries_thirds +#print axioms cone_moment_m1_thirds +#print axioms trace_and_traceless_variances +#print axioms fourth_moment_of_trace +#print axioms exponential_moment_of_trace +#print axioms cone_moment_m2_algebra +#print axioms cube_root_simplification +#print axioms pin_determinant_and_joint_dimension +#print axioms hessian_block_eigenvalues + +-- Endpoints.lean +#print axioms d2_endpoints_adjacent +#print axioms d3_endpoints_adjacent +#print axioms d3_below_d2 +#print axioms endpoints_in_unit_tenth diff --git a/formal/UniversalLaw/Side24/ConeMoments.lean b/formal/UniversalLaw/Side24/ConeMoments.lean new file mode 100644 index 000000000..e18e69b08 --- /dev/null +++ b/formal/UniversalLaw/Side24/ConeMoments.lean @@ -0,0 +1,85 @@ +/-! +# SIDE24 coefficient note — reference covariance and cone moments, arithmetic skeleton + +Informal source (Layer 0, byte-pinned): `Math-` commit +`9d7b6802424fb4715b31999066aafca8ee2f3cca`, `coefficients/side24_v1/PROOF.md`, +SHA-256 `c06daccc4ba4b9168522b9888b76a7d599934fc3b91bd753ee5d492262917769`, +section 1. + +Core Lean has no rational-number type, so every rational identity is stated +as the equivalent cross-multiplied integer identity, with the rational form in +the docstring. The kernel checks the integers; a reviewer checks that the +integer statement is the stated rational statement (the alignment review lane). + +Not formalised here: the Gaussian conditioning that produces the covariance +formula `Cov(A_ij,A_kl | V=0) = (2/3)δ_ijδ_kl + δ_ikδ_jl + δ_ilδ_jk`, the +elementary integral `∫_0^a (a-z)^2 e^{-z/2} dz/2 = a^2-4a+8-8e^{-a/2}`, the +Gaussian moment identities `E s^4 = 3 (Var s)^2` and +`E exp(-s^2/2) = (1+Var s)^{-1/2}`, and the Rayleigh cone integration. Only the +arithmetic that combines those inputs is kernel-checked. +-/ + +namespace UniversalLaw.Side24 + +/-- Source: "Var(t)=15, Cov(t,G)=(-3,0,...,0)" and "tau^2=Var(t|G=0)=6": +the Gaussian conditional variance `15 - (-3)^2 / Var(G_1)` with `Var(G_1) = 1`. -/ +theorem conditional_third_derivative_variance : (15 : Int) - (-3) * (-3) / 1 = 6 := by + decide + +/-- Source: "Cov(A_ij,A_kl | V=0) = (2/3)delta_ij delta_kl + delta_ik delta_jl ++ delta_il delta_jk". With `i=j=k=l` the three deltas give `2/3 + 1 + 1 = 8/3` +(source: "For m=1 the variance of A is8/3"); for `A_12` only `δ_ik δ_jl` survives +(variance `1`); for the pair `A_11, A_22` only `(2/3)δ_ij δ_kl` survives +(covariance `2/3`). All in thirds. -/ +theorem transverse_covariance_entries_thirds : + 2 + 3 + 3 = 8 ∧ 0 + 3 + 0 = 3 ∧ 2 + 0 + 0 = 2 := by decide + +/-- Source: "D_1=E[A^2 1{A<0}]=4/3" — half of the variance `8/3` by centred +symmetry. In thirds: `8 = 2 · 4`. -/ +theorem cone_moment_m1_thirds : 8 = 2 * 4 := by decide + +/-- Source: "For m=2 write A=[[s+x,y],[y,s-x]]. Then s,x,y are independent, +Var(s)=5/3 and Var(x)=Var(y)=1." With `s = (A_11+A_22)/2`, `x = (A_11-A_22)/2`: +`Var s = (8/3 + 8/3 + 2·2/3)/4 = 20/12 = 5/3`, +`Var x = (8/3 + 8/3 - 2·2/3)/4 = 12/12 = 1`, +`Cov(s,x) = (Var A_11 - Var A_22)/4 = 0`, `Var y = Var A_12 = 1`. +Stated in thirds over the common denominator 12. This is the "shared trace +variance5/3" that the note lists first among the items for nonauthor review. -/ +theorem trace_and_traceless_variances : + 8 + 8 + 2 * 2 = 20 ∧ 20 * 3 = 5 * 12 ∧ + 8 + 8 - 2 * 2 = 12 ∧ 12 = 1 * 12 ∧ + (8 : Int) - 8 = 0 := by decide + +/-- Source: "E s^2=5/3, E s^4=25/3": for a centred Gaussian `E s^4 = 3 (E s^2)^2`, +so `E s^4 = 3 · (5/3)^2 = 75/9 = 25/3`. Cross-multiplied: `3 · 5^2 · 3 = 25 · 9`. -/ +theorem fourth_moment_of_trace : 3 * 5 ^ 2 * 3 = 25 * 9 := by decide + +/-- Source: "E exp(-s^2/2)=sqrt(3/8)": `E exp(-s^2/2) = (1 + Var s)^{-1/2}` with +`1 + 5/3 = 8/3`. In thirds: `3 + 5 = 8`. -/ +theorem exponential_moment_of_trace : 3 + 5 = 8 := by decide + +/-- Source: "D_2 = (1/2)[25/3-20/3+8-8sqrt(3/8)] = 29/6-sqrt(6)". +The bracket is the polynomial `a^2 - 4a + 8 - 8e^{-a/2}` averaged at +`a = s^2`, so `4 · E s^2 = 4 · 5/3 = 20/3`. +Rational part: `(25/3 - 20/3 + 8)/2 = (29/3)/2 = 29/6`; in thirds +`25 - 20 + 24 = 29`. Irrational part: `(1/2)·8·√(3/8) = 4√(3/8) = √(16·3/8) = √6`; +cross-multiplied `4^2 · 3 = 6 · 8`. -/ +theorem cone_moment_m2_algebra : + 4 * 5 = 20 ∧ 25 - 20 + 24 = 29 ∧ 4 ^ 2 * 3 = 6 * 8 := by decide + +/-- Source: "simplifying 6^(2/3)/24^(1/3)=(3/2)^(1/3)". Cubing both sides: +`6^2 / 24 = 3/2`, i.e. `6^2 · 2 = 3 · 24`. -/ +theorem cube_root_simplification : 6 ^ 2 * 2 = 3 * 24 := by decide + +/-- Source: "p_G(0) p_V(0) = (2pi)^(-d) / sqrt(3)": `det diag(3,1,...,1) = 3`, and +"Its dimension is at most10": the joint vector `(G, t, svec H)` has +`d + 1 + d(d+1)/2` coordinates, `6` for `d = 2` and `10` for `d = 3`. -/ +theorem pin_determinant_and_joint_dimension : + 3 * 1 * 1 = 3 ∧ 2 + 1 + 2 * 3 / 2 = 6 ∧ 3 + 1 + 3 * 4 / 2 = 10 := by decide + +/-- Source: "The reference Hessian block has eigenvalues d+2 on trace and2 on +traceless matrices": for `d = 2,3` these are `4, 5` and `2`; each exceeds `1/3` +(`1 < 3·2`), consistent with the later `C_ref >= I/3`. -/ +theorem hessian_block_eigenvalues : 2 + 2 = 4 ∧ 3 + 2 = 5 ∧ 1 < 3 * 2 := by decide + +end UniversalLaw.Side24 diff --git a/formal/UniversalLaw/Side24/Endpoints.lean b/formal/UniversalLaw/Side24/Endpoints.lean new file mode 100644 index 000000000..f39037e1d --- /dev/null +++ b/formal/UniversalLaw/Side24/Endpoints.lean @@ -0,0 +1,41 @@ +/-! +# SIDE24 published endpoints — consistency of the frozen artifact + +Informal source (Layer 0, byte-pinned): `Math-` commit +`9d7b6802424fb4715b31999066aafca8ee2f3cca`, `coefficients/side24_v1/ENCLOSURE.json`, +1090 bytes, SHA-256 `72b6cd92d31394cdaf5da8919a5d548e902228af1f095cc184158a71d8287811`. + +The published decimal endpoints are transcribed here as integers in units of +`10^-20`. The kernel checks that each interval is nonempty and exactly one +`10^-20` step wide, and that the two intervals are disjoint and ordered. + +This module does **not** establish that the coefficient lies in either +interval: that claim needs `Real.Gamma`, `Real.pi`, `Real.exp` and the +Gaussian cone moments, none of which exist in core Lean. Its formalization +status is recorded as `none` in `formal/registry.json`. +-/ + +namespace UniversalLaw.Side24 + +/-- `0.07340691930603427103` and `0.07340691930603427104` in units of `10^-20`. -/ +def d2Lower : Nat := 7340691930603427103 +def d2Upper : Nat := 7340691930603427104 + +/-- `0.04177593184059834334` and `0.04177593184059834335` in units of `10^-20`. -/ +def d3Lower : Nat := 4177593184059834334 +def d3Upper : Nat := 4177593184059834335 + +/-- Source: "0.07340691930603427103 < c_2,24 < 0.07340691930603427104" — the +published endpoints are distinct and adjacent on the 20-digit grid. -/ +theorem d2_endpoints_adjacent : d2Lower < d2Upper ∧ d2Upper = d2Lower + 1 := by decide + +/-- Source: "0.04177593184059834334 < c_3,24 < 0.04177593184059834335". -/ +theorem d3_endpoints_adjacent : d3Lower < d3Upper ∧ d3Upper = d3Lower + 1 := by decide + +/-- The published `d = 3` interval lies strictly below the `d = 2` interval. -/ +theorem d3_below_d2 : d3Upper < d2Lower := by decide + +/-- Both published intervals lie in `(0, 1/10)`: `10^-20`-units below `10^19`. -/ +theorem endpoints_in_unit_tenth : 0 < d3Lower ∧ d2Upper < 10 ^ 19 := by decide + +end UniversalLaw.Side24 diff --git a/formal/UniversalLaw/Side24/Ledger.lean b/formal/UniversalLaw/Side24/Ledger.lean new file mode 100644 index 000000000..38b5d76c6 --- /dev/null +++ b/formal/UniversalLaw/Side24/Ledger.lean @@ -0,0 +1,141 @@ +/-! +# SIDE24 coefficient note — analytic-image ledger, arithmetic skeleton + +Informal source (Layer 0, byte-pinned): `Math-` commit +`9d7b6802424fb4715b31999066aafca8ee2f3cca`, `coefficients/side24_v1/PROOF.md`, +SHA-256 `c06daccc4ba4b9168522b9888b76a7d599934fc3b91bd753ee5d492262917769`, +sections 2–4, and the `image_ledger()` function of `coefficient.py`. + +What this module establishes: every *exact integer or rational* identity and +inequality that sections 2–4 of the note rely on is checked by the Lean kernel. +No `sorry`, no `native_decide`, no axioms (see `UniversalLaw/Audit.lean`). + +What this module does **not** establish: the analytic facts the arithmetic is +attached to — the Gaussian derivative bound `76|x|^6 e^{-|x|^2/2}` for `|x| ≥ 1`, +the geometric-tail argument, the positive-semidefinite covariance comparison, +the Schur-complement monotonicity, the Gaussian density comparison, and the +`log`/`exp` estimates that turn exponents into the factor `32ε`. Those remain +author-side prose under nonauthor review (Layer 0). Nothing here changes the +scientific status of the coefficient or of its parent theorem. +-/ + +namespace UniversalLaw.Side24 + +/-- Factorial on `Nat`; kept local so that the library has no dependencies. -/ +def fact : Nat → Nat + | 0 => 1 + | n + 1 => (n + 1) * fact n + +/-- Product-rule pairing count for `q` unit directional derivatives of +`exp(-|x|^2/2)`: `∑_{j=0}^{⌊q/2⌋} q! / (2^j j! (q-2j)!)`. Section 2 of the note +uses its value at `q = 6` and the fact that it dominates the lower orders. -/ +def pairingSum (q : Nat) : Nat := + (List.range (q / 2 + 1)).foldl + (fun acc j => acc + fact q / (2 ^ j * fact j * fact (q - 2 * j))) 0 + +/-- Source: "The coefficient sum for q=6 is 1+15+45+15=76". -/ +theorem pairing_sum_six : pairingSum 6 = 76 := by decide + +/-- Source: "and it bounds the smaller orders as well". -/ +theorem pairing_sum_le_six : ∀ q, q ∈ [0, 1, 2, 3, 4, 5, 6] → pairingSum q ≤ 76 := by + decide + +/-- The individual pairing terms at `q = 6`, as displayed in the note. -/ +theorem pairing_terms_six : + fact 6 / (2 ^ 0 * fact 0 * fact 6) = 1 ∧ + fact 6 / (2 ^ 1 * fact 1 * fact 4) = 15 ∧ + fact 6 / (2 ^ 2 * fact 2 * fact 2) = 45 ∧ + fact 6 / (2 ^ 3 * fact 3 * fact 0) = 15 := by + decide + +/-- Source: "At zero, every such contraction has absolute value at most 15". +The sixth Gaussian moment / sixth derivative of `exp(-x^2/2)` at zero is the +double factorial `5!! = 1·3·5`. Only the arithmetic value is checked here. -/ +theorem sixth_moment_double_factorial : 1 * 3 * 5 = 15 := by decide + +/-- Source: "there are at most 27j^3 possibilities for d<=3, |n|^6<=27j^6" and +"<=729 sum_{j>=1} j^9 e^(-288j^2) <=1458 e^(-288)". The two factors of 27 give +729; the geometric tail with ratio at most 1/2 gives the factor 2. -/ +theorem lattice_shell_constant : 27 * 27 = 729 ∧ 729 * 2 = 1458 := by decide + +/-- Source: "successive terms have ratio at most 512e^(-864)". `512 = 2^9` is +the worst ratio `(j+1)^9 / j^9` at `j = 1`; `864 = 288·3` is the exponent gap +`288((j+1)^2 - j^2)` at `j = 1`. -/ +theorem geometric_ratio_constants : 2 ^ 9 = 512 ∧ 288 * 3 = 864 := by decide + +/-- `24^2 / 2 = 288`: the periodization exponent for lattice period 24. -/ +theorem period_exponent : 24 ^ 2 / 2 = 288 := by decide + +/-- The image constant `E · 10^125` of display (2): +`1458 · (76 · 24^6 + 15)`. -/ +def imageConstant : Nat := 1458 * (76 * 24 ^ 6 + 15) + +/-- Source: "E := 1458*(76*24^6+15)*10^(-125) = 21175738586478 *10^(-125)". -/ +theorem image_constant_value : imageConstant = 21175738586478 := by decide + +/-- Numerator of the degree-20 Taylor partial sum of `exp(288/125)` after +clearing the denominator `125^20 · 20!`: +`∑_{k=0}^{20} 288^k · 125^(20-k) · 20!/k!`. -/ +def expTaylorNumerator : Nat := + (List.range 21).foldl + (fun acc k => acc + 288 ^ k * 125 ^ (20 - k) * (fact 20 / fact k)) 0 + +/-- Source: "The code proves e^(288/125)>10 using the positive rational Taylor +sum through20". Because every Taylor term of `exp` at a positive argument is +positive, the partial sum is a lower bound; this theorem checks that the exact +rational partial sum exceeds 10. The step from the partial sum to `exp` itself +is analysis and is not formalised here. -/ +theorem exp_taylor_partial_sum_gt_ten : + 10 * (125 ^ 20 * fact 20) < expTaylorNumerator := by decide + +/-- Source: "Each covariance entry differs from the reference by at most2E ... +the spectral norm of the difference is at most20E" (dimension at most 10) and +"C_ref >= I/3 ... epsilon=10^(-108), since60E 1/3 ⇔ 23/3 > √58 ⇔ 23^2 > 58·9`. -/ +theorem smaller_eigenvalue_exceeds_third : 58 * 9 < 23 ^ 2 := by decide + +/-- Source (section 4): with `m = d-1`, `n = m(m+1)/2`, `a = m + 2/3 + n/2`, +`b = d + n/2`. These are `6a` and `6b` as natural numbers. -/ +def sixA (d : Nat) : Nat := 6 * (d - 1) + 4 + 3 * ((d - 1) * d / 2) +def sixB (d : Nat) : Nat := 6 * d + 3 * ((d - 1) * d / 2) + +/-- Source: "For d=2,3, a+2b<14 and2a+b<13". In sixths: `6a + 12b < 84` and +`12a + 6b < 78`. For `d = 3` the second inequality is `77 < 78`, so this is a +genuinely tight check. -/ +theorem exponent_bounds : + ∀ d, d ∈ [2, 3] → sixA d + 2 * sixB d < 84 ∧ 2 * sixA d + sixB d < 78 := by + decide + +/-- The exact values behind `exponent_bounds`: `d = 2` gives `a = 13/6`, `b = 5/2`; +`d = 3` gives `a = 25/6`, `b = 9/2`. -/ +theorem exponent_values : + sixA 2 = 13 ∧ sixB 2 = 15 ∧ sixA 3 = 25 ∧ sixB 3 = 27 := by decide + +/-- Source: "ratio between1-13epsilon and1+28epsilon, hence safely between +1-32epsilon and1+32epsilon". The analytic `log`/`exp` estimates are not +formalised; the ordering of the constants is. -/ +theorem ratio_constant_ordering : 13 ≤ 32 ∧ 28 ≤ 32 := by decide + +/-- Source: "|c_d,24/c_d,ref -1| < 10^(-106)" together with `ε = 10^(-108)` +and the factor 32 from section 4: `32 · 10^(-108) < 10^(-106)`. -/ +theorem density_comparison_below_reported : 32 * 10 ^ 106 < 10 ^ 108 := by decide + +end UniversalLaw.Side24 diff --git a/formal/lake-manifest.json b/formal/lake-manifest.json new file mode 100644 index 000000000..fc7655fad --- /dev/null +++ b/formal/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "UniversalLaw", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/formal/lakefile.toml b/formal/lakefile.toml new file mode 100644 index 000000000..d986aa8d7 --- /dev/null +++ b/formal/lakefile.toml @@ -0,0 +1,11 @@ +name = "UniversalLaw" +defaultTargets = ["UniversalLaw"] + +# Layer 1 (formal) pilot. Deliberately dependency-free: every theorem in this +# library is checked by the Lean 4 kernel from core Lean alone, so `lake build` +# needs no Mathlib cache, no network after the toolchain download, and finishes +# in seconds. Adding Mathlib is the documented next step for statements that +# need real analysis (see README.md, "Expansion path"). + +[[lean_lib]] +name = "UniversalLaw" diff --git a/formal/lean-toolchain b/formal/lean-toolchain new file mode 100644 index 000000000..ba8ebf2db --- /dev/null +++ b/formal/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.34.1 diff --git a/formal/registry.json b/formal/registry.json new file mode 100644 index 000000000..ec1b19248 --- /dev/null +++ b/formal/registry.json @@ -0,0 +1,828 @@ +{ + "schema": 1, + "scope": "FORMALIZATION_STATUS_ONLY", + "scientific_status_authority": false, + "meaning": "Per-claim formalization status for the Lean 4 layer. A status here records what the Lean kernel checked and nothing else: it cannot promote, close, or reclassify a Layer 0 (source-bound review) status in STATUS.md or PROOF_INDEX.md, and a kernel-checked arithmetic lemma does not make its surrounding analytic argument verified.", + "lean_toolchain": "leanprover/lean4:v4.34.1", + "project_root": "formal", + "audit_module": "formal/UniversalLaw/Audit.lean", + "allowed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "forbidden_axioms": [ + "sorryAx", + "Lean.ofReduceBool", + "Lean.ofReduceNat" + ], + "status_levels": { + "none": "No Lean object. The claim lives only in Layer 0 prose.", + "specified": "A Lean statement (a `def ... : Prop`) compiles; no proof is offered. Its hypotheses are the exact claimed scope.", + "proved": "A Lean proof compiles but depends on project-declared axioms (for example an unformalized parent theorem taken as an explicit axiom with a scope note) or on axioms outside the allow-list other than the forbidden ones.", + "kernel-checked": "A Lean proof compiles and `#print axioms` reports only allowed axioms. No sorry, no native_decide, no project axioms." + }, + "alignment_review_levels": { + "open": "Author-side only. Nobody other than the author has checked that the Lean statement says what the informal anchor says.", + "reviewed": "A distinct reviewer has recorded, in formal/reviews/, that the Lean statement matches the informal anchor at the stated scope. Same-provider reviewers earn zero organizational-independence credit.", + "not-applicable": "No Lean statement exists." + }, + "lean_files": [ + { + "path": "formal/lean-toolchain", + "sha256": "d5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b" + }, + { + "path": "formal/lakefile.toml", + "sha256": "58f0fa6864cc03e9bcbef2d8c0404e9f3385a30a6124000454319367906cbe4a" + }, + { + "path": "formal/UniversalLaw.lean", + "sha256": "985368dd6009921e6487597e622ff0e37225a4b21d4ee9724c76c193eb718d4d" + }, + { + "path": "formal/UniversalLaw/Audit.lean", + "sha256": "bdccd68c108fd1d1ed48f4f27690cae3c0d6ea679e8026b10e402dc49067973a" + }, + { + "path": "formal/UniversalLaw/Side24/Ledger.lean", + "sha256": "7e321cef49195b7c920960f965cbddb8fe17ad6a31e09371fa860a204f3721d1" + }, + { + "path": "formal/UniversalLaw/Side24/ConeMoments.lean", + "sha256": "2bcd4a83683188856bce010c3dcdec6904e45a6d73b50b9f3891e632ff58985c" + }, + { + "path": "formal/UniversalLaw/Side24/Endpoints.lean", + "sha256": "3e285bd81b906b1b15f9e14a2552ea800380b14c862ae85148abfe1ef6a27f8a" + } + ], + "sources": [ + { + "id": "side24-proof", + "repository": "d6g8k5htny-coder/Math-", + "commit": "9d7b6802424fb4715b31999066aafca8ee2f3cca", + "path": "coefficients/side24_v1/PROOF.md", + "bytes": 10272, + "sha256": "c06daccc4ba4b9168522b9888b76a7d599934fc3b91bd753ee5d492262917769", + "local_copy": "formal/sources/side24_v1/PROOF.md" + }, + { + "id": "side24-enclosure", + "repository": "d6g8k5htny-coder/Math-", + "commit": "9d7b6802424fb4715b31999066aafca8ee2f3cca", + "path": "coefficients/side24_v1/ENCLOSURE.json", + "bytes": 1090, + "sha256": "72b6cd92d31394cdaf5da8919a5d548e902228af1f095cc184158a71d8287811", + "local_copy": "formal/sources/side24_v1/ENCLOSURE.json" + } + ], + "cross_checks": [], + "cross_check_schema": { + "prover": "name and version", + "date": "YYYY-MM-DD", + "declaration": "Lean name", + "outcome": "kernel-checked | failed | not-attempted", + "record": "path under formal/reviews/", + "note": "An AI-prover success is an additional lane, recorded here; it is still checked by the same kernel and does not replace the alignment review." + }, + "claims": [ + { + "id": "side24-pairing-sum-six", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Product-rule pairing count at q=6 equals 76", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.pairing_sum_six", + "lean_file": "formal/UniversalLaw/Side24/Ledger.lean", + "source": "side24-proof", + "informal_anchor": "The coefficient sum for q=6 is\n1+15+45+15=76", + "does_not_claim": "the derivative bound 76|x|^6 e^(-|x|^2/2) itself", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-pairing-sum-lower-orders", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Pairing counts for q<=6 are at most 76", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.pairing_sum_le_six", + "lean_file": "formal/UniversalLaw/Side24/Ledger.lean", + "source": "side24-proof", + "informal_anchor": "it bounds the smaller orders as well", + "does_not_claim": "the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-pairing-terms", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Individual pairing terms 1, 15, 45, 15", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.pairing_terms_six", + "lean_file": "formal/UniversalLaw/Side24/Ledger.lean", + "source": "side24-proof", + "informal_anchor": "1+15+45+15=76", + "does_not_claim": "the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-sixth-moment", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Double factorial 5!! = 15", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.sixth_moment_double_factorial", + "lean_file": "formal/UniversalLaw/Side24/Ledger.lean", + "source": "side24-proof", + "informal_anchor": "At zero, every such\ncontraction has absolute value at most15.", + "does_not_claim": "that Gaussian derivative contractions at zero are bounded by 15", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-lattice-shell", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Shell constants 27·27 = 729 and 729·2 = 1458", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.lattice_shell_constant", + "lean_file": "formal/UniversalLaw/Side24/Ledger.lean", + "source": "side24-proof", + "informal_anchor": "<=729 sum_{j>=1} j^9 e^(-288j^2)\n <=1458 e^(-288).", + "does_not_claim": "the lattice-point count or the geometric tail sum", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-geometric-ratio", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Ratio constants 2^9 = 512 and 288·3 = 864", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.geometric_ratio_constants", + "lean_file": "formal/UniversalLaw/Side24/Ledger.lean", + "source": "side24-proof", + "informal_anchor": "successive terms have ratio at most512e^(-864)<1/2", + "does_not_claim": "that the ratio is below 1/2", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-period-exponent", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Period-24 exponent 24^2/2 = 288", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.period_exponent", + "lean_file": "formal/UniversalLaw/Side24/Ledger.lean", + "source": "side24-proof", + "informal_anchor": "sum_{n!=0} |n|^6 e^(-288|n|^2)", + "does_not_claim": "the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-image-constant", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Image constant 1458·(76·24^6+15) = 21175738586478", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.image_constant_value", + "lean_file": "formal/UniversalLaw/Side24/Ledger.lean", + "source": "side24-proof", + "informal_anchor": "E := 1458*(76*24^6+15)*10^(-125)\n = 21175738586478 *10^(-125).", + "does_not_claim": "the inequality |D^q K_24(0)-D^q K_infty(0)| < E", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-exp-taylor", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Degree-20 Taylor partial sum of exp(288/125) exceeds 10", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.exp_taylor_partial_sum_gt_ten", + "lean_file": "formal/UniversalLaw/Side24/Ledger.lean", + "source": "side24-proof", + "informal_anchor": "The code proves e^(288/125)>10 using the positive rational Taylor sum through20", + "does_not_claim": "that the partial sum is below exp(288/125) (positivity of the omitted terms is analysis)", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-covariance-bound", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "60E < 10^(-108) as the integer inequality 60·21175738586478 < 10^17", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.covariance_relative_bound", + "lean_file": "formal/UniversalLaw/Side24/Ledger.lean", + "source": "side24-proof", + "informal_anchor": "epsilon=10^(-108), since60E= I/3", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-odd-block-eigen", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Odd block trace 16 and determinant 6 = 8^2 - 58", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.odd_block_eigenvalues", + "lean_file": "formal/UniversalLaw/Side24/Ledger.lean", + "source": "side24-proof", + "informal_anchor": "[[1,-3],[-3,15]], whose eigenvalues are8 +/- sqrt(58)", + "does_not_claim": "the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-odd-block-shift", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Shifted odd block minors 2/3 and 7/9 (scaled by 3: 2 and 7)", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.odd_block_shifted_minors", + "lean_file": "formal/UniversalLaw/Side24/Ledger.lean", + "source": "side24-proof", + "informal_anchor": "subtract I/3 and use first principal minor2/3 and determinant7/9", + "does_not_claim": "Sylvester's criterion", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-eigen-third", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "8 - sqrt(58) > 1/3 via 23^2 > 58·9", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.smaller_eigenvalue_exceeds_third", + "lean_file": "formal/UniversalLaw/Side24/Ledger.lean", + "source": "side24-proof", + "informal_anchor": "Its smaller eigenvalue exceeds\n1/3", + "does_not_claim": "monotonicity of the square root", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-exponent-bounds", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Exponent inequalities a+2b<14 and 2a+b<13 for d=2,3 (in sixths)", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.exponent_bounds", + "lean_file": "formal/UniversalLaw/Side24/Ledger.lean", + "source": "side24-proof", + "informal_anchor": "For d=2,3, a+2b<14 and2a+b<13.", + "does_not_claim": "the log/exp estimates that follow", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-exponent-values", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Exact a, b values for d=2,3", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.exponent_values", + "lean_file": "formal/UniversalLaw/Side24/Ledger.lean", + "source": "side24-proof", + "informal_anchor": "a=m+2/3+n/2, b=d+n/2.", + "does_not_claim": "the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-ratio-constants", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "13 <= 32 and 28 <= 32", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.ratio_constant_ordering", + "lean_file": "formal/UniversalLaw/Side24/Ledger.lean", + "source": "side24-proof", + "informal_anchor": "ratio between1-13epsilon and\n1+28epsilon, hence safely between1-32epsilon and1+32epsilon", + "does_not_claim": "the elementary log/exp bounds", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-density-comparison", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "32·10^(-108) < 10^(-106)", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.density_comparison_below_reported", + "lean_file": "formal/UniversalLaw/Side24/Ledger.lean", + "source": "side24-proof", + "informal_anchor": "|c_d,24/c_d,ref -1| < 10^(-106), d=2,3.", + "does_not_claim": "the multiplicative density comparison", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-tau-squared", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Conditional variance tau^2 = 15 - 9 = 6", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.conditional_third_derivative_variance", + "lean_file": "formal/UniversalLaw/Side24/ConeMoments.lean", + "source": "side24-proof", + "informal_anchor": "Var(t)=15, Cov(t,G)=(-3,0,...,0)", + "does_not_claim": "the Gaussian conditioning formula or the covariance derivatives", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-transverse-covariance", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Transverse covariance entries 8/3, 1, 2/3 from the delta formula", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.transverse_covariance_entries_thirds", + "lean_file": "formal/UniversalLaw/Side24/ConeMoments.lean", + "source": "side24-proof", + "informal_anchor": "Cov(A_ij,A_kl | V=0)\n = (2/3)delta_ij delta_kl + delta_ik delta_jl + delta_il delta_jk.", + "does_not_claim": "the delta formula itself", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-cone-m1", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "D_1 = 4/3 is half of 8/3", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.cone_moment_m1_thirds", + "lean_file": "formal/UniversalLaw/Side24/ConeMoments.lean", + "source": "side24-proof", + "informal_anchor": "D_1=E[A^2 1{A<0}]=4/3.", + "does_not_claim": "centred Gaussian symmetry", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-trace-variance", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Var(s) = 5/3, Var(x) = Var(y) = 1, Cov(s,x) = 0 from the 2x2 covariance entries", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.trace_and_traceless_variances", + "lean_file": "formal/UniversalLaw/Side24/ConeMoments.lean", + "source": "side24-proof", + "informal_anchor": "Var(s)=5/3 and Var(x)=Var(y)=1.", + "does_not_claim": "independence beyond zero covariance, which is Gaussian", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-fourth-moment", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "E s^4 = 3·(5/3)^2 = 25/3", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.fourth_moment_of_trace", + "lean_file": "formal/UniversalLaw/Side24/ConeMoments.lean", + "source": "side24-proof", + "informal_anchor": "E s^2=5/3, E s^4=25/3", + "does_not_claim": "the Gaussian fourth-moment identity", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-exp-moment", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "1 + 5/3 = 8/3 behind E exp(-s^2/2) = sqrt(3/8)", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.exponential_moment_of_trace", + "lean_file": "formal/UniversalLaw/Side24/ConeMoments.lean", + "source": "side24-proof", + "informal_anchor": "E exp(-s^2/2)=sqrt(3/8)", + "does_not_claim": "the Gaussian exponential-moment identity", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-cone-m2", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "D_2 algebra: rational part 29/6 and 4·sqrt(3/8) = sqrt(6)", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.cone_moment_m2_algebra", + "lean_file": "formal/UniversalLaw/Side24/ConeMoments.lean", + "source": "side24-proof", + "informal_anchor": "D_2 = (1/2)[25/3-20/3+8-8sqrt(3/8)]\n = 29/6-sqrt(6).", + "does_not_claim": "the integral identity or the Rayleigh cone integration", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-cube-root", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "6^2·2 = 3·24 behind 6^(2/3)/24^(1/3) = (3/2)^(1/3)", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.cube_root_simplification", + "lean_file": "formal/UniversalLaw/Side24/ConeMoments.lean", + "source": "side24-proof", + "informal_anchor": "simplifying 6^(2/3)/24^(1/3)=(3/2)^(1/3)", + "does_not_claim": "the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-pin-dimension", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "det diag(3,1,..,1) = 3 and joint dimensions 6, 10", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.pin_determinant_and_joint_dimension", + "lean_file": "formal/UniversalLaw/Side24/ConeMoments.lean", + "source": "side24-proof", + "informal_anchor": "Its dimension is at most10.", + "does_not_claim": "the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-hessian-eigen", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Hessian block eigenvalues 4, 5, 2 exceed 1/3", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.hessian_block_eigenvalues", + "lean_file": "formal/UniversalLaw/Side24/ConeMoments.lean", + "source": "side24-proof", + "informal_anchor": "The reference Hessian block has eigenvalues d+2 on trace and2 on traceless matrices", + "does_not_claim": "the spectral decomposition", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-d2-endpoints", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Published d=2 endpoints are adjacent 20-digit decimals", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.d2_endpoints_adjacent", + "lean_file": "formal/UniversalLaw/Side24/Endpoints.lean", + "source": "side24-enclosure", + "informal_anchor": "\"2\": {\n \"lower\": \"0.07340691930603427103\",\n \"upper\": \"0.07340691930603427104\"", + "does_not_claim": "that c_2,24 lies between them", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-d3-endpoints", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Published d=3 endpoints are adjacent 20-digit decimals", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.d3_endpoints_adjacent", + "lean_file": "formal/UniversalLaw/Side24/Endpoints.lean", + "source": "side24-enclosure", + "informal_anchor": "\"3\": {\n \"lower\": \"0.04177593184059834334\",\n \"upper\": \"0.04177593184059834335\"", + "does_not_claim": "that c_3,24 lies between them", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-d3-below-d2", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Published d=3 interval lies below the d=2 interval", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.d3_below_d2", + "lean_file": "formal/UniversalLaw/Side24/Endpoints.lean", + "source": "side24-enclosure", + "informal_anchor": "\"scientific_acceptance\": false", + "does_not_claim": "anything about the true coefficients", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "side24-endpoints-range", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "Published endpoints lie in (0, 1/10)", + "status": "kernel-checked", + "lean_declaration": "UniversalLaw.Side24.endpoints_in_unit_tenth", + "lean_file": "formal/UniversalLaw/Side24/Endpoints.lean", + "source": "side24-enclosure", + "informal_anchor": "\"relative_periodization_bound\": \"1e-106\"", + "does_not_claim": "anything about the true coefficients", + "alignment_review": { + "status": "open", + "author": "Anthropic / Claude (Cursor cloud agent), 2026-09-27; author-side, AI-generated", + "reviewer": null, + "record": null + } + }, + { + "id": "d3-side24-coefficient-bound", + "layer0_object": "D3 — SIDE24 coefficient calculation", + "title": "0.07340691930603427103 < c_2,24 < 0.07340691930603427104 and the d=3 analogue", + "status": "none", + "lean_declaration": null, + "lean_file": null, + "source": null, + "informal_anchor": null, + "blocked_on": [ + "Real.Gamma and its Stirling remainder", + "Real.pi enclosure", + "Real.exp / Real.log enclosures", + "Gaussian cone moments D_1, D_2", + "positive-semidefinite covariance comparison", + "Mathlib dependency" + ], + "glossary_terms": [ + "SIDE24", + "cone moment", + "reference coefficient", + "image ledger" + ], + "layer0_source": "https://github.com/d6g8k5htny-coder/Math-/blob/9d7b6802424fb4715b31999066aafca8ee2f3cca/coefficients/side24_v1/PROOF.md", + "layer0_status_note": "ACCEPT — scoped at Layer 0 (STATUS.md); the arithmetic skeleton above is kernel-checked, the analytic content is not", + "does_not_claim": "any formal verification; Layer 0 review status is unchanged", + "alignment_review": { + "status": "not-applicable", + "author": null, + "reviewer": null, + "record": null + } + }, + { + "id": "d2-lifetime-remainder", + "layer0_object": "D2 — unrestricted lifetime remainder", + "title": "Theorem R: bounded O(1) remainder for candidate and elder densities", + "status": "none", + "lean_declaration": null, + "lean_file": null, + "source": null, + "informal_anchor": null, + "blocked_on": [ + "Gaussian random fields on the torus", + "marked Kac–Rice formula", + "Gaussian regression", + "Mathlib probability" + ], + "glossary_terms": [ + "candidate density", + "elder density", + "lifetime", + "pin", + "full normalizer" + ], + "layer0_source": "https://github.com/d6g8k5htny-coder/Math-/blob/main/frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md", + "layer0_status_note": "ACCEPT — scoped at Layer 0; no formal object yet", + "does_not_claim": "any formal verification; Layer 0 review status is unchanged", + "alignment_review": { + "status": "not-applicable", + "author": null, + "reviewer": null, + "record": null + } + }, + { + "id": "d4-fixed-remote-rn-count", + "layer0_object": "D4 — fixed-remote RN count theorem", + "title": "Expected count O(r^3) in the between-pin height window at fixed rho, eta", + "status": "none", + "lean_declaration": null, + "lean_file": null, + "source": null, + "informal_anchor": null, + "blocked_on": [ + "Kac–Rice counting formula", + "conditioned Gaussian covariance", + "determinant factor bounds", + "Mathlib" + ], + "glossary_terms": [ + "RN count", + "remote critical point", + "pin", + "contact kernel", + "height window" + ], + "layer0_source": "https://github.com/d6g8k5htny-coder/Math-/blob/main/frontiers/remote_window_20260924/PROOF.md", + "layer0_status_note": "ACCEPT — scoped at Layer 0; no formal object yet", + "does_not_claim": "any formal verification; Layer 0 review status is unchanged", + "alignment_review": { + "status": "not-applicable", + "author": null, + "reviewer": null, + "record": null + } + }, + { + "id": "d6-p15-full-price", + "layer0_object": "D6 — P15 full-price theorem", + "title": "Theorem F: sharp uniform factor rho* = 1/(3 - log(3e-2)) on the realized family", + "status": "none", + "lean_declaration": null, + "lean_file": null, + "source": null, + "informal_anchor": null, + "blocked_on": [ + "finite hypergraph / clutter definitions", + "independent product measure", + "Real.log", + "Mathlib" + ], + "glossary_terms": [ + "realized family", + "palette", + "capacity", + "clutter", + "price" + ], + "layer0_source": "https://github.com/d6g8k5htny-coder/Math-/blob/main/frontiers/full_price_20260924/PROOF.md", + "layer0_status_note": "ACCEPT — scoped at Layer 0; finite combinatorics makes this the most tractable next formalization target", + "does_not_claim": "any formal verification; Layer 0 review status is unchanged", + "alignment_review": { + "status": "not-applicable", + "author": null, + "reviewer": null, + "record": null + } + }, + { + "id": "d1-parent-selection-chain", + "layer0_object": "D1 — parent quantitative Theorem-A selection chain", + "title": "Sections 2–7 quantitative selection chain of UNIFORM-MATRIX-CAP-LIFETIME-20260924-v1", + "status": "none", + "lean_declaration": null, + "lean_file": null, + "source": null, + "informal_anchor": null, + "blocked_on": [ + "Layer 0 review is itself reopened (AMEND)", + "all of the above" + ], + "glossary_terms": [ + "elder selection", + "matrix cap", + "marked cylinder" + ], + "layer0_source": "https://github.com/d6g8k5htny-coder/Math-/blob/main/imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "layer0_status_note": "AMEND / open at Layer 0; formalization would begin by stating the hypotheses as explicit axioms with scope notes", + "does_not_claim": "any formal verification; Layer 0 review status is unchanged", + "alignment_review": { + "status": "not-applicable", + "author": null, + "reviewer": null, + "record": null + } + }, + { + "id": "d5-pin-neighborhoods", + "layer0_object": "D5 — pin neighborhoods / microdisk", + "title": "Summed pin-neighborhood bound including the inner microdisk", + "status": "none", + "lean_declaration": null, + "lean_file": null, + "source": null, + "informal_anchor": null, + "blocked_on": [ + "no complete informal proof yet" + ], + "glossary_terms": [ + "pin neighborhood", + "microdisk", + "collar", + "annulus" + ], + "layer0_source": "https://github.com/d6g8k5htny-coder/Math-/issues/58", + "layer0_status_note": "AMEND / open at Layer 0; nothing to formalize until a complete candidate exists", + "does_not_claim": "any formal verification; Layer 0 review status is unchanged", + "alignment_review": { + "status": "not-applicable", + "author": null, + "reviewer": null, + "record": null + } + }, + { + "id": "sard-g-a1-a6", + "layer0_object": "SARD-G A1/A6", + "title": "A1 and A6 of the SARD-G successor", + "status": "none", + "lean_declaration": null, + "lean_file": null, + "source": null, + "informal_anchor": null, + "blocked_on": [ + "open-chart premise not yet repaired at Layer 0" + ], + "glossary_terms": [ + "SARD-G" + ], + "layer0_source": "https://github.com/d6g8k5htny-coder/main/blob/main/reviews/sard_g_successor_a1_a6_20260926/REVIEW.md", + "layer0_status_note": "AMEND / open at Layer 0", + "does_not_claim": "any formal verification; Layer 0 review status is unchanged", + "alignment_review": { + "status": "not-applicable", + "author": null, + "reviewer": null, + "record": null + } + } + ] +} diff --git a/formal/sources/side24_v1/ENCLOSURE.json b/formal/sources/side24_v1/ENCLOSURE.json new file mode 100644 index 000000000..57af39a05 --- /dev/null +++ b/formal/sources/side24_v1/ENCLOSURE.json @@ -0,0 +1,29 @@ +{ + "cone_moments": { + "2": "4/3", + "3": "29/6-sqrt(6)" + }, + "dimensions": { + "2": { + "lower": "0.07340691930603427103", + "upper": "0.07340691930603427104" + }, + "3": { + "lower": "0.04177593184059834334", + "upper": "0.04177593184059834335" + } + }, + "image_ledger": { + "covariance_relative_bound": "31763607879717/2500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "density_comparison_below_reported": true, + "derivative_bound": "10587869293239/50000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "exp_lower_gt_10": true, + "image_constant": 21175738586478, + "relative_below_eps": true + }, + "method": "outward rational arithmetic; analytic image and Stirling remainder bounds", + "object": "SIDE24-COEFFICIENT-D23-20260924-v1", + "relative_periodization_bound": "1e-106", + "scientific_acceptance": false, + "scope": "coefficient of issue63 Eq15.2; parent theorem unreviewed" +} diff --git a/formal/sources/side24_v1/PROOF.md b/formal/sources/side24_v1/PROOF.md new file mode 100644 index 000000000..44b66f04f --- /dev/null +++ b/formal/sources/side24_v1/PROOF.md @@ -0,0 +1,216 @@ +# SIDE24 coefficient in dimensions two and three + +Object: SIDE24-COEFFICIENT-D23-20260924-v1. Author: OpenAI / ChatGPT. +Disposition: author-side coefficient-evaluation candidate; nonauthor review open. + +## Scope and exact parent + +This note evaluates the coefficient defined in equation (15.2) of +UNIFORM-MATRIX-CAP-LIFETIME-20260924-v1, SHA256 +`9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7`, +Drive ID `1foDgiDi4XIKOfbrZEE8dWKV_BkZU8LIb`, main issue63. +It does not independently accept that parent's global elder-selection or Kac-Rice +proof. Interpreting this coefficient as the finite-bar asymptotic constant remains +conditional on that proof. The parent source is not modified. + +Use its centered variance-one field with the exact normalized covariance + + K_24(z) = sum_{n in Z^d} exp(-|z+24n|^2/2) + / sum_{n in Z^d} exp(-|24n|^2/2), d in {2,3}. + +Let c_d,24 be precisely its equation (15.2), using ordinary sphere area, ordered +maximum/saddle roles and the full height/gradient pin Jacobian. Then the bounds +proved below, with endpoints rational decimal numbers, are + + 0.07340691930603427103 < c_2,24 < 0.07340691930603427104, + 0.04177593184059834334 < c_3,24 < 0.04177593184059834335. + +The uncertainty in these intervals is numerical/arithmetic uncertainty in this +specified expression, not a probability of correctness of the parent theorem. +No finite-radius error estimate, unrestricted remainder or RN/24-jet claim follows. + +## 1. A nonperiodic reference coefficient with exact cone moments + +Use K_infty(z)=exp(-|z|^2/2) only to define a reference CONTACT covariance and its +coefficient expression. No infinite-volume persistence theorem is asserted. +In an orthonormal frame with u=e1, covariance differentiation gives + + Cov(G)=I_d, + Cov(H_ij,H_kl)=delta_ij delta_kl+delta_ik delta_jl+delta_il delta_jk, + Var(t)=15, Cov(t,G)=(-3,0,...,0), t=partial_1^3 f. + +Thus V=Hu has covariance diag(3,1,...,1), tau^2=Var(t|G=0)=6, and + + p_G(0) p_V(0) = (2pi)^(-d) / sqrt(3). + +Writing m=d-1 and A for the transverse Hessian, Gaussian conditioning on V=0 gives + + Cov(A_ij,A_kl | V=0) + = (2/3)delta_ij delta_kl + delta_ik delta_jl + delta_il delta_jk. + +Equivalently A=Q+sqrt(2/3) Z I_m, with Q's diagonal variances2, off-diagonal +variances1, and independent upper-triangular entries, and Z an independent standard +normal. This explicitly specified reference law is not substituted for the actual +periodic law without an error bound. + +For m=1 the variance of A is8/3. Centered Gaussian symmetry gives + + D_1=E[A^2 1{A<0}]=4/3. + +For m=2 write A=[[s+x,y],[y,s-x]]. Then s,x,y are independent, +Var(s)=5/3 and Var(x)=Var(y)=1. The negative-definite cone is s<-R, +R=sqrt(x^2+y^2), and det A=s^2-R^2. The variable R^2 has density e^(-z/2)/2. +For a>=0, elementary integration gives + + integral_0^a (a-z)^2 e^(-z/2) dz/2 = a^2-4a+8-8e^(-a/2). + +Using symmetry in s, E s^2=5/3, E s^4=25/3 and +E exp(-s^2/2)=sqrt(3/8), one obtains + + D_2 = (1/2)[25/3-20/3+8-8sqrt(3/8)] + = 29/6-sqrt(6). + +The truncation R<|s| is essential: half the UNTRUNCATED determinant-squared moment +would instead give29/6, an incorrect value. The shared scalar shift of the matrix +is likewise essential. + +Substituting these moments and |S^1|=2pi, |S^2|=4pi into the exact parent coefficient +and simplifying 6^(2/3)/24^(1/3)=(3/2)^(1/3) gives + + c_d,ref = Gamma(7/6)*(3/2)^(1/3)*D_(d-1) + / [2sqrt(3)*pi^(d-1)*sqrt(pi)], d=2,3. (1) + +This eliminates BOTH the angular and cone integrals for the reference expression. + +## 2. A uniform, deterministic bound for every omitted periodic image + +For q<=6 unit directional differentiations of phi(x)=exp(-|x|^2/2), product-rule +pairings bound the absolute derivative by + + e^(-|x|^2/2) sum_{j=0}^{floor(q/2)} + q! |x|^(q-2j) / [2^j j! (q-2j)!]. + +At |x|>=1 this is at most76 |x|^6 e^(-|x|^2/2). The coefficient sum for q=6 is +1+15+45+15=76 and it bounds the smaller orders as well. At zero, every such +contraction has absolute value at most15. + +For an integer point with maximum coordinate magnitude j>=1, there are at most +27j^3 possibilities for d<=3, |n|^6<=27j^6, and |n|^2>=j^2. Consequently + + sum_{n!=0} |n|^6 e^(-288|n|^2) + <=729 sum_{j>=1} j^9 e^(-288j^2) + <=1458 e^(-288). + +The last step follows because successive terms have ratio at most512e^(-864)<1/2. +The code proves e^(288/125)>10 using the positive rational Taylor sum through20; +hence e^(-288)<10^(-125) and the geometric-ratio inequality follows too. + +Normalizing by S=sum_n exp(-288|n|^2)>=1 costs the subtraction of +(S-1)D^q phi(0), which is included. Thus for EVERY unit-direction contraction, +including mixed directions, through total order6, + + |D^q K_24(0)-D^q K_infty(0)| + < E := 1458*(76*24^6+15)*10^(-125) + = 21175738586478 *10^(-125). (2) + +This is a bound on the infinite image sum, not a sampled orientation or truncated +floating-point comparison. It applies to the exact variance-one normalization. + +## 3. Full joint covariance and all orientations + +Use the joint vector (G,t,svec H), where svec lists diagonal Hessian entries and +sqrt(2) times independent off-diagonal entries. Its dimension is at most10. +Each covariance entry differs from the reference by at most2E, by (2). +Hence the spectral norm of the difference is at most20E. + +The reference Hessian block has eigenvalues d+2 on trace and2 on traceless matrices; +it is independent of the odd derivative block. The only nontrivial odd block is +[[1,-3],[-3,15]], whose eigenvalues are8 +/- sqrt(58). Its smaller eigenvalue exceeds +1/3: subtract I/3 and use first principal minor2/3 and determinant7/9. +All remaining gradient variances are1. Thus C_ref >= I/3 and + + (1-epsilon) C_ref <= C_24 <= (1+epsilon) C_ref, + epsilon=10^(-108), since60E0 its expectation scales by a^m, since h has degree2m and the cone is scale +invariant. Thus the exact conditional cone moment has the same bounds, multiplied +by (1-epsilon)^m D0 and (1+epsilon)^m D0 respectively. No continuity claim about +an indicator at a singular matrix is used. + +Combining this with the two d-dimensional densities and tau^(4/3) yields an +integrand ratio between + + (1-epsilon)^a/(1+epsilon)^b and (1+epsilon)^a/(1-epsilon)^b, + a=m+2/3+n/2, b=d+n/2. + +For d=2,3, a+2b<14 and2a+b<13. Since epsilon is far below1/28, elementary bounds +on log(1+epsilon), -log(1-epsilon) and exp give ratio between1-13epsilon and +1+28epsilon, hence safely between1-32epsilon and1+32epsilon. Angular integration +preserves these multiplicative bounds because every reference integrand is positive. +It follows that + + |c_d,24/c_d,ref -1| < 10^(-106), d=2,3. (4) + +The exact periodic constant is NOT claimed equal to the reference constant. +Equation (4) bounds it and justifies the numerical interval in this note. + +## 5. Outward arithmetic and special-function remainder + +`coefficient.py` uses only integer and Fraction arithmetic to obtain (1)-(4). +Every interval operation rounds outward to the rational grid10^(-80); negative +values use mathematical floor/ceiling rather than rounding toward zero. Floats and +booleans are rejected as inputs. Roots use exact integer root brackets. + +Pi uses Machin's identity16atan(1/5)-4atan(1/239) with alternating-series remainder. +Log uses range reduction and the positive atanh series, with its geometric tail. +Exp uses reduction to[0,1/4], its positive Taylor series and a ratio-bounded tail; +negative arguments use reciprocal intervals. + +Gamma(7/6) is obtained by shifting to z=199/6, using Stirling's LOG-gamma expansion +through B20, enclosing the remainder by the positive first omitted B22 term, then +subtracting the32 recurrence logarithms and exponentiating. The rigorous positive- +real remainder rule is NIST DLMF5.11(ii), and recurrence is DLMF5.5(i). +The periodization allowance in (4) is applied to exact rational endpoints BEFORE +the final outward rounding; it is not silently rounded to zero. +The displayed endpoints are outward rational decimal bounds, not rounded guesses. + +The supplied unit tests and mutation runs are finite implementation/algebra checks. +They do not constitute formal verification or nonauthor analytic acceptance. +`ENCLOSURE.json` records the computed bounds and explicit scope. + +## Review and remaining work + +Nonauthor review should independently check the shared trace variance5/3, Rayleigh +cone integration, ordered-pair/gamma normalization inherited from the parent, +all-direction derivative bound, covariance and Schur-complement comparison, and +rational interval implementation. No frozen proof, review grade, RN/24-jet obligation, +P15 assertion or project completion flag is changed. + +### External reconnaissance, 24 September 2026 + +Primary sources read: NIST DLMF5.11, especially equation5.11.1 and positive-real +remainder statement in5.11(ii); DLMF5.5 for the gamma recurrence. These are established +numerical-analysis inputs. The Gaussian covariance/cone and image comparison above +are derived here; no priority or novelty claim follows. Main issue63 and its exact +Drive source provide the project coefficient and conventions. diff --git a/tests/test_formal_gate.py b/tests/test_formal_gate.py new file mode 100644 index 000000000..1ddffca62 --- /dev/null +++ b/tests/test_formal_gate.py @@ -0,0 +1,348 @@ +"""Positive and negative controls for the formalization gate. + +Synthetic controls use a disposable mini project so that each mutation is +isolated. Repository controls run the real registry statically, and — when a +Lean toolchain is on PATH or in ~/.elan — build the real library, run the +axiom audit, and confirm that tightened inequalities are rejected by Lean. +""" +import hashlib +import importlib.util +import json +import os +from pathlib import Path +import shutil +import subprocess +import tempfile +import unittest + +ROOT = Path(__file__).resolve().parents[1] +spec = importlib.util.spec_from_file_location("gate", ROOT / "tools/formal_gate_check.py") +gate = importlib.util.module_from_spec(spec) +spec.loader.exec_module(gate) + +TOOLCHAIN = "leanprover/lean4:v4.34.1" +LEAN = """namespace Demo + +/-- Source: "two and two make four". A comment mentioning sorry is harmless. -/ +theorem two_add : 2 + 2 = 4 := by decide + +theorem tight : 77 < 78 := by decide + +end Demo +""" +SOURCE = "Section 1. In the source, two and two make four; also 77 < 78 here.\n" +AUDIT = ("'Demo.two_add' does not depend on any axioms\n" + "'Demo.tight' does not depend on any axioms\n") + + +def sha(data: bytes) -> str: + return hashlib.sha256(data).hexdigest() + + +class SyntheticControls(unittest.TestCase): + def setUp(self): + self.tmp = tempfile.TemporaryDirectory() + self.addCleanup(self.tmp.cleanup) + self.root = Path(self.tmp.name) + (self.root / "formal/Demo").mkdir(parents=True) + (self.root / "formal/sources").mkdir() + (self.root / "formal/reviews").mkdir() + self.write("formal/lean-toolchain", TOOLCHAIN + "\n") + self.write("formal/lakefile.toml", 'name = "Demo"\n[[lean_lib]]\nname = "Demo"\n') + self.write("formal/Demo.lean", "import Demo.Basic\n") + self.write("formal/Demo/Basic.lean", LEAN) + self.write("formal/Demo/Audit.lean", "import Demo\n#print axioms Demo.two_add\n#print axioms Demo.tight\n") + self.write("formal/sources/SOURCE.md", SOURCE) + self.audit = self.root / "audit.txt" + self.audit.write_text(AUDIT) + self.registry = { + "schema": 1, "scope": "FORMALIZATION_STATUS_ONLY", "scientific_status_authority": False, + "meaning": "test", "lean_toolchain": TOOLCHAIN, "project_root": "formal", + "audit_module": "formal/Demo/Audit.lean", + "allowed_axioms": ["propext", "Classical.choice", "Quot.sound"], + "forbidden_axioms": ["sorryAx", "Lean.ofReduceBool"], + "status_levels": {"none": "", "specified": "", "proved": "", "kernel-checked": ""}, + "alignment_review_levels": {"open": "", "reviewed": "", "not-applicable": ""}, + "project_axioms": [], + "lean_files": [], + "sources": [{"id": "src", "repository": "d6g8k5htny-coder/Math-", "commit": "a" * 40, + "path": "SOURCE.md", "bytes": len(SOURCE.encode()), "sha256": sha(SOURCE.encode()), + "local_copy": "formal/sources/SOURCE.md"}], + "cross_checks": [], + "claims": [ + {"id": "two-add", "layer0_object": "Demo", "title": "two add", "status": "kernel-checked", + "lean_declaration": "Demo.two_add", "lean_file": "formal/Demo/Basic.lean", "source": "src", + "informal_anchor": "two and two make four", "does_not_claim": "anything else", + "alignment_review": {"status": "open", "author": "author", "reviewer": None, "record": None}}, + {"id": "tight", "layer0_object": "Demo", "title": "tight", "status": "kernel-checked", + "lean_declaration": "Demo.tight", "lean_file": "formal/Demo/Basic.lean", "source": "src", + "informal_anchor": "77 < 78", "does_not_claim": "anything else", + "alignment_review": {"status": "open", "author": "author", "reviewer": None, "record": None}}, + {"id": "big-theorem", "layer0_object": "Demo", "title": "big", "status": "none", + "lean_declaration": None, "lean_file": None, "source": None, "informal_anchor": None, + "does_not_claim": "any formal verification", + "alignment_review": {"status": "not-applicable", "author": None, "reviewer": None, "record": None}}, + ], + } + self.refresh_files() + (self.root / "formal/ALIGNMENT.md").write_text(gate.render_alignment(self.registry)) + + def write(self, relative, text): + (self.root / relative).write_text(text) + + def refresh_files(self): + self.registry["lean_files"] = [ + {"path": p, "sha256": sha((self.root / p).read_bytes())} + for p in ["formal/lean-toolchain", "formal/lakefile.toml", "formal/Demo.lean", + "formal/Demo/Basic.lean", "formal/Demo/Audit.lean"]] + self.save() + + def save(self): + (self.root / "formal/registry.json").write_text(json.dumps(self.registry)) + + def run_check(self, **kwargs): + kwargs.setdefault("axioms_output", self.audit) + return gate.check(self.root, **kwargs) + + def assertProblem(self, fragment, **kwargs): + problems = self.run_check(**kwargs)["problems"] + self.assertTrue(any(fragment in p for p in problems), problems) + + def assertInvalid(self, fragment, **kwargs): + with self.assertRaisesRegex((ValueError, OSError), fragment): + self.run_check(**kwargs) + + # positive control + + def test_valid_and_no_writes(self): + before = {str(p): p.read_bytes() for p in self.root.rglob("*") if p.is_file()} + result = self.run_check(alignment="formal/ALIGNMENT.md") + self.assertEqual(result["problems"], []) + self.assertEqual(result["status_counts"]["kernel-checked"], 2) + self.assertEqual(result["status_counts"]["none"], 1) + self.assertEqual(result["axiom_audit"]["declarations_required"], 2) + self.assertEqual(before, {str(p): p.read_bytes() for p in self.root.rglob("*") if p.is_file()}) + + def test_static_only_is_reported_not_silent(self): + result = self.run_check(axioms_output=None, static_only=True) + self.assertEqual(result["problems"], []) + self.assertIn("NOT RUN", result["axiom_audit"]) + + def test_axiom_lane_required_by_default(self): + self.assertInvalid("axiom lane required", axioms_output=None) + + # Lean file identity and content + + def test_lean_hash_mismatch(self): + self.write("formal/Demo/Basic.lean", LEAN.replace("77 < 78", "77 < 79")) + self.assertProblem("sha256 differs") + + def test_unregistered_lean_file(self): + self.write("formal/Demo/Extra.lean", "theorem extra : True := trivial\n") + self.assertProblem("present but not registered") + + def test_sorry_in_code(self): + self.write("formal/Demo/Basic.lean", LEAN.replace("by decide\n\ntheorem tight", "by sorry\n\ntheorem tight")) + self.refresh_files() + self.assertProblem("contains sorry") + + def test_sorry_only_in_comment_is_ignored(self): + self.write("formal/Demo/Basic.lean", LEAN + "-- sorry, native_decide and axiom words in a comment\n/- nested /- sorry -/ still comment -/\n") + self.refresh_files() + self.assertEqual(self.run_check()["problems"], []) + + def test_native_decide_refused(self): + self.write("formal/Demo/Basic.lean", LEAN.replace(":= by decide\n\ntheorem tight", ":= by native_decide\n\ntheorem tight")) + self.refresh_files() + self.assertProblem("native_decide") + + def test_unregistered_axiom_declaration(self): + self.write("formal/Demo/Basic.lean", LEAN + "axiom parent_theorem : 1 = 1\n") + self.refresh_files() + self.assertProblem("axiom parent_theorem is not registered") + + def test_registered_axiom_with_scope_note_accepted(self): + self.write("formal/Demo/Basic.lean", LEAN + "axiom parent_theorem : 1 = 1\n") + self.registry["project_axioms"] = [{"name": "parent_theorem", "scope_note": "assumed, not verified"}] + self.refresh_files() + self.assertEqual(self.run_check()["problems"], []) + + def test_project_axiom_needs_scope_note(self): + self.registry["project_axioms"] = [{"name": "parent_theorem", "scope_note": ""}] + self.save() + self.assertInvalid("scope_note") + + def test_toolchain_mismatch(self): + self.write("formal/lean-toolchain", "leanprover/lean4:v4.0.0\n") + self.refresh_files() + self.assertProblem("lean-toolchain file differs") + + def test_toolchain_must_be_listed(self): + self.registry["lean_files"] = [f for f in self.registry["lean_files"] if not f["path"].endswith("lean-toolchain")] + self.save() + self.assertInvalid("lean-toolchain must be a listed") + + # sources and anchors + + def test_source_bytes_changed(self): + self.write("formal/sources/SOURCE.md", SOURCE + "x") + self.assertProblem("differs from pinned bytes") + + def test_anchor_not_verbatim(self): + self.registry["claims"][0]["informal_anchor"] = "two and two make five" + self.save() + self.assertProblem("not a verbatim substring") + + def test_nonpublic_source_repository_refused(self): + self.registry["sources"][0]["repository"] = "someone/private" + self.save() + self.assertInvalid("nonpublic source repository") + + def test_bad_commit_refused(self): + self.registry["sources"][0]["commit"] = "abc" + self.save() + self.assertInvalid("invalid commit") + + # claims + + def test_declaration_missing_from_file(self): + self.registry["claims"][0]["lean_declaration"] = "Demo.three_add" + self.save() + self.assertProblem("three_add not found") + + def test_declaration_in_wrong_namespace(self): + self.registry["claims"][0]["lean_declaration"] = "Other.two_add" + self.save() + self.assertProblem("not found") + + def test_none_status_cannot_carry_declaration(self): + self.registry["claims"][2]["lean_declaration"] = "Demo.two_add" + self.save() + self.assertInvalid("status none cannot carry") + + def test_unknown_status(self): + self.registry["claims"][0]["status"] = "verified" + self.save() + self.assertInvalid("unknown status") + + def test_duplicate_claim_id(self): + self.registry["claims"][1]["id"] = "two-add" + self.save() + self.assertInvalid("duplicate claim id") + + def test_duplicate_json_key(self): + (self.root / "formal/registry.json").write_text('{"schema":1,"schema":1}') + self.assertInvalid("duplicate JSON key") + + def test_status_authority_must_be_false(self): + self.registry["scientific_status_authority"] = True + self.save() + self.assertInvalid("scientific_status_authority") + + def test_reviewed_alignment_needs_record_file(self): + self.registry["claims"][0]["alignment_review"] = {"status": "reviewed", "author": "a", "reviewer": "r", + "record": "formal/reviews/missing.md"} + self.save() + self.assertInvalid("missing or outside-root") + + def test_reviewed_alignment_with_record_accepted(self): + self.write("formal/reviews/two_add.md", "reviewed\n") + self.registry["claims"][0]["alignment_review"] = {"status": "reviewed", "author": "a", "reviewer": "r", + "record": "formal/reviews/two_add.md"} + self.save() + self.assertEqual(self.run_check()["problems"], []) + + def test_does_not_claim_required(self): + self.registry["claims"][0]["does_not_claim"] = " " + self.save() + self.assertInvalid("does_not_claim") + + # axiom audit + + def test_missing_from_audit(self): + self.audit.write_text("'Demo.two_add' does not depend on any axioms\n") + self.assertProblem("Demo.tight missing from axiom audit") + + def test_sorry_axiom_in_audit(self): + self.audit.write_text(AUDIT.replace("'Demo.tight' does not depend on any axioms", + "'Demo.tight' depends on axioms: [sorryAx]")) + problems = self.run_check()["problems"] + self.assertTrue(any("forbidden axioms ['sorryAx']" in p for p in problems), problems) + + def test_native_decide_axiom_in_audit(self): + self.audit.write_text(AUDIT.replace("'Demo.tight' does not depend on any axioms", + "'Demo.tight' depends on axioms: [Lean.ofReduceBool]")) + self.assertProblem("Lean.ofReduceBool") + + def test_allowed_axioms_pass_for_kernel_checked(self): + self.audit.write_text(AUDIT.replace("'Demo.tight' does not depend on any axioms", + "'Demo.tight' depends on axioms: [propext, Classical.choice, Quot.sound]")) + self.assertEqual(self.run_check()["problems"], []) + + def test_unlisted_axiom_fails_kernel_checked_but_not_proved(self): + self.audit.write_text(AUDIT.replace("'Demo.tight' does not depend on any axioms", + "'Demo.tight' depends on axioms: [Demo.parent]")) + self.assertProblem("non-allowed axioms ['Demo.parent']") + self.registry["claims"][1]["status"] = "proved" + self.save() + self.assertEqual(self.run_check()["problems"], []) + + def test_audit_error_line_fails(self): + self.audit.write_text(AUDIT + "Basic.lean:4:0: error: something\n") + self.assertProblem("reports an error") + + # alignment table + + def test_alignment_table_drift(self): + (self.root / "formal/ALIGNMENT.md").write_text("stale\n") + self.assertProblem("differs from the registry rendering", alignment="formal/ALIGNMENT.md") + + +class RepositoryControls(unittest.TestCase): + def test_real_registry_static(self): + result = gate.check(ROOT, static_only=True, alignment="formal/ALIGNMENT.md") + self.assertEqual(result["problems"], []) + self.assertGreaterEqual(result["status_counts"]["kernel-checked"], 1) + self.assertEqual(result["status_counts"]["proved"], 0) + + def test_real_registry_has_no_status_authority(self): + data = json.loads((ROOT / "formal/registry.json").read_text()) + self.assertIs(data["scientific_status_authority"], False) + for claim in data["claims"]: + self.assertTrue(claim["does_not_claim"].strip()) + + @unittest.skipUnless(gate.lake_binary(), "Lean toolchain not installed") + def test_real_library_builds_and_audit_passes(self): + result = gate.check(ROOT, run=True, alignment="formal/ALIGNMENT.md") + self.assertEqual(result["problems"], []) + self.assertEqual(result["axiom_audit"]["declarations_reported"], result["axiom_audit"]["declarations_required"]) + + @unittest.skipUnless(gate.lake_binary(), "Lean toolchain not installed") + def test_lean_rejects_tightened_bounds(self): + lake = gate.lake_binary() + project = ROOT / "formal" + env = dict(os.environ, PATH=f"{Path(lake).parent}{os.pathsep}{os.environ.get('PATH', '')}") + ledger = (project / "UniversalLaw/Side24/Ledger.lean").read_text() + mutants = { + "exponent d=3 tight": ("sixB d < 78", "sixB d < 77"), + "covariance bound": ("60 * imageConstant < 10 ^ 17", "60 * imageConstant < 10 ^ 15"), + "exp partial sum": ("10 * (125 ^ 20 * fact 20) < expTaylorNumerator", "11 * (125 ^ 20 * fact 20) < expTaylorNumerator"), + "image constant": ("= 21175738586478", "= 21175738586479"), + "eigenvalue third": ("58 * 9 < 23 ^ 2", "58 * 9 < 22 ^ 2"), + } + with tempfile.TemporaryDirectory() as tmp: + for name, (old, new) in mutants.items(): + self.assertIn(old, ledger, name) + mutant = Path(tmp) / "Mutant.lean" + mutant.write_text(ledger.replace(old, new)) + run = subprocess.run([lake, "env", "lean", str(mutant)], cwd=project, capture_output=True, text=True, env=env) + self.assertNotEqual(run.returncode, 0, f"{name}: Lean accepted a false statement") + self.assertIn("is false", run.stdout + run.stderr, name) + control = Path(tmp) / "Control.lean" + control.write_text(ledger) + run = subprocess.run([lake, "env", "lean", str(control)], cwd=project, capture_output=True, text=True, env=env) + self.assertEqual(run.returncode, 0, run.stdout + run.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/formal_gate_check.py b/tools/formal_gate_check.py new file mode 100644 index 000000000..f3985809a --- /dev/null +++ b/tools/formal_gate_check.py @@ -0,0 +1,399 @@ +#!/usr/bin/env python3 +"""Fail-closed gate for the Lean formalization registry (Layer 1). + +Checks, offline and without writing: + +* `formal/registry.json` is well formed (unique keys, known statuses, pinned + toolchain, allowed/forbidden axiom lists). +* Every Lean file under the project is listed with a matching SHA-256; no + `sorry`, `native_decide`, or unregistered `axiom` appears in any of them. +* Every byte-pinned informal source has a local copy with the recorded size and + SHA-256, and every registered informal anchor is a verbatim substring of it. +* Every claim with a Lean status names a declaration that exists in the listed + file; every `none` claim names nothing. +* With `--axioms-output FILE` (the captured output of + `lake env lean UniversalLaw/Audit.lean`) or `--run-lean`, every + `kernel-checked` declaration depends only on allowed axioms and every + `proved` declaration avoids the forbidden ones. Missing declarations fail. + +`--static-only` skips the axiom lane and says so in the output. The check never +changes a status: it can only refuse one. A green run establishes that the +registered arithmetic is kernel-checked; it is not mathematical acceptance of +any Layer 0 claim. +""" +from __future__ import annotations + +import argparse +import hashlib +import json +import os +from pathlib import Path, PurePosixPath +import re +import shutil +import subprocess + +ROOT = Path(__file__).resolve().parents[1] +REGISTRY = "formal/registry.json" +HEX40 = re.compile(r"[0-9a-f]{40}") +HEX64 = re.compile(r"[0-9a-f]{64}") +PUBLIC_REPOS = {"d6g8k5htny-coder/main", "d6g8k5htny-coder/Math-", "d6g8k5htny-coder/query-", + "d6g8k5htny-coder/meta-framework", "d6g8k5htny-coder/Universal-Law-Workspace"} +LEAN_STATUSES = ("specified", "proved", "kernel-checked") +AUDIT_LINE = re.compile(r"^'(?P[^']+)' (?:does not depend on any axioms|depends on axioms: \[(?P[^\]]*)\])\s*$") +DECL = re.compile(r"^\s*(?:private\s+|protected\s+|noncomputable\s+)*(?:theorem|lemma|def|abbrev|instance|structure|inductive)\s+([^\s:({]+)", re.M) +AXIOM_DECL = re.compile(r"^\s*axiom\s+([^\s:({]+)", re.M) +NAMESPACE = re.compile(r"^\s*namespace\s+([^\s]+)", re.M) + + +def unique_pairs(pairs): + result = {} + for key, value in pairs: + if key in result: + raise ValueError(f"duplicate JSON key: {key}") + result[key] = value + return result + + +def local_file(root: Path, relative) -> Path: + if not isinstance(relative, str) or not relative or "\\" in relative: + raise ValueError(f"expected nonempty relative path: {relative!r}") + pure = PurePosixPath(relative) + if pure.is_absolute() or ".." in pure.parts: + raise ValueError(f"unsafe path: {relative}") + path = root + for part in pure.parts: + path = path / part + if path.is_symlink(): + raise ValueError(f"symlink refused: {relative}") + path = path.resolve() + if not path.is_relative_to(root.resolve()) or not path.is_file(): + raise ValueError(f"missing or outside-root file: {relative}") + return path + + +def sha256(data: bytes) -> str: + return hashlib.sha256(data).hexdigest() + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def load_registry(root: Path, registry: str) -> dict: + data = json.loads(local_file(root, registry).read_text(encoding="utf-8"), object_pairs_hook=unique_pairs) + require(isinstance(data, dict) and data.get("schema") == 1, "unknown registry schema") + require(data.get("scope") == "FORMALIZATION_STATUS_ONLY", "unknown registry scope") + require(data.get("scientific_status_authority") is False, "registry must declare scientific_status_authority false") + for key in ("lean_toolchain", "project_root", "audit_module"): + require(isinstance(data.get(key), str) and data[key], f"{key} must be a nonempty string") + for key in ("allowed_axioms", "forbidden_axioms"): + value = data.get(key) + require(isinstance(value, list) and all(isinstance(x, str) and x for x in value), f"{key} must list axiom names") + require(not set(data["allowed_axioms"]) & set(data["forbidden_axioms"]), "an axiom cannot be both allowed and forbidden") + levels = data.get("status_levels") + require(isinstance(levels, dict) and set(levels) == {"none", *LEAN_STATUSES}, "status_levels must define exactly none/specified/proved/kernel-checked") + alignment = data.get("alignment_review_levels") + require(isinstance(alignment, dict) and set(alignment) == {"open", "reviewed", "not-applicable"}, "alignment_review_levels must define open/reviewed/not-applicable") + for key in ("lean_files", "sources", "claims", "cross_checks"): + require(isinstance(data.get(key), list), f"{key} must be a list") + axioms = data.get("project_axioms", []) + require(isinstance(axioms, list), "project_axioms must be a list") + for item in axioms: + require(isinstance(item, dict) and isinstance(item.get("name"), str) and isinstance(item.get("scope_note"), str) + and item["name"] and item["scope_note"], "each project axiom needs a name and a scope_note") + return data + + +def strip_lean_comments(text: str) -> str: + """Remove `--` line comments and (nested) `/- -/` block comments. + + Comment text cannot smuggle a proof term, and the kernel audit of `sorryAx` + is the authoritative guard; this only keeps the cheap textual scan honest. + """ + out, i, depth, n = [], 0, 0, len(text) + while i < n: + two = text[i:i + 2] + if depth: + if two == "/-": + depth += 1 + i += 2 + elif two == "-/": + depth -= 1 + i += 2 + else: + out.append("\n" if text[i] == "\n" else " ") + i += 1 + elif two == "/-": + depth, i = 1, i + 2 + elif two == "--": + end = text.find("\n", i) + i = n if end < 0 else end + else: + out.append(text[i]) + i += 1 + return "".join(out) + + +def check_lean_files(root: Path, data: dict, problems: list) -> dict: + project = data["project_root"] + listed = {} + for item in data["lean_files"]: + require(isinstance(item, dict) and set(item) == {"path", "sha256"}, "lean_files rows need exactly path and sha256") + require(isinstance(item["sha256"], str) and HEX64.fullmatch(item["sha256"]), f"invalid sha256 for {item['path']}") + require(item["path"] not in listed, f"duplicate lean file: {item['path']}") + path = local_file(root, item["path"]) + payload = path.read_bytes() + listed[item["path"]] = payload + if sha256(payload) != item["sha256"]: + problems.append(f"{item['path']}: sha256 differs from registry") + toolchain_rel = f"{project}/lean-toolchain" + require(toolchain_rel in listed, "lean-toolchain must be a listed lean file") + require(f"{project}/lakefile.toml" in listed or f"{project}/lakefile.lean" in listed, "lakefile must be a listed lean file") + require(data["audit_module"] in listed, "audit module must be a listed lean file") + if listed[toolchain_rel].decode("utf-8").strip() != data["lean_toolchain"]: + problems.append("lean-toolchain file differs from registry lean_toolchain") + project_dir = local_file(root, toolchain_rel).parent + for path in sorted(project_dir.rglob("*.lean")): + if ".lake" in path.relative_to(project_dir).parts: + continue + relative = path.relative_to(root.resolve()).as_posix() + if relative not in listed: + problems.append(f"{relative}: Lean file present but not registered") + registered_axioms = {item["name"] for item in data.get("project_axioms", [])} + for relative, payload in listed.items(): + if not relative.endswith(".lean"): + continue + text = strip_lean_comments(payload.decode("utf-8")) + if re.search(r"\bsorry\b", text): + problems.append(f"{relative}: contains sorry") + if re.search(r"\bnative_decide\b", text): + problems.append(f"{relative}: contains native_decide") + for name in AXIOM_DECL.findall(text): + if name not in registered_axioms and not any(name.endswith("." + n) or n.endswith("." + name) for n in registered_axioms): + problems.append(f"{relative}: axiom {name} is not registered in project_axioms") + return listed + + +def check_sources(root: Path, data: dict, problems: list) -> dict: + sources = {} + for item in data["sources"]: + require(isinstance(item, dict) and set(item) == {"id", "repository", "commit", "path", "bytes", "sha256", "local_copy"}, "source rows have a fixed schema") + require(item["repository"] in PUBLIC_REPOS, f"nonpublic source repository refused: {item['repository']}") + require(isinstance(item["commit"], str) and HEX40.fullmatch(item["commit"]), f"invalid commit for {item['id']}") + require(isinstance(item["sha256"], str) and HEX64.fullmatch(item["sha256"]), f"invalid sha256 for {item['id']}") + require(type(item["bytes"]) is int and item["bytes"] > 0, f"invalid byte count for {item['id']}") + require(isinstance(item["id"], str) and item["id"] and item["id"] not in sources, f"invalid or duplicate source id: {item['id']}") + payload = local_file(root, item["local_copy"]).read_bytes() + if len(payload) != item["bytes"] or sha256(payload) != item["sha256"]: + problems.append(f"{item['id']}: local copy {item['local_copy']} differs from pinned bytes") + sources[item["id"]] = payload.decode("utf-8") + return sources + + +def declared_names(text: str) -> set: + names = set() + namespaces = NAMESPACE.findall(text) + for short in DECL.findall(text): + names.add(short) + for ns in namespaces: + names.add(f"{ns}.{short}") + return names + + +def check_claims(root: Path, data: dict, lean_files: dict, sources: dict, problems: list) -> dict: + ids = set() + counts = {status: 0 for status in data["status_levels"]} + alignment_counts = {level: 0 for level in data["alignment_review_levels"]} + audited = {} + declared_cache = {} + for claim in data["claims"]: + require(isinstance(claim, dict), "claims must be objects") + cid = claim.get("id") + require(isinstance(cid, str) and re.fullmatch(r"[a-z0-9][a-z0-9-]*", cid or ""), f"invalid claim id: {cid!r}") + require(cid not in ids, f"duplicate claim id: {cid}") + ids.add(cid) + status = claim.get("status") + require(status in data["status_levels"], f"{cid}: unknown status {status!r}") + counts[status] += 1 + for key in ("layer0_object", "title", "does_not_claim"): + require(isinstance(claim.get(key), str) and claim[key].strip(), f"{cid}: {key} must be a nonempty string") + review = claim.get("alignment_review") + require(isinstance(review, dict) and set(review) == {"status", "author", "reviewer", "record"}, f"{cid}: alignment_review schema") + require(review["status"] in data["alignment_review_levels"], f"{cid}: unknown alignment status") + alignment_counts[review["status"]] += 1 + if status == "none": + for key in ("lean_declaration", "lean_file", "source", "informal_anchor"): + require(claim.get(key) is None, f"{cid}: status none cannot carry {key}") + require(review["status"] == "not-applicable", f"{cid}: status none requires alignment not-applicable") + continue + require(review["status"] != "not-applicable", f"{cid}: a Lean statement needs an alignment status") + require(isinstance(review["author"], str) and review["author"], f"{cid}: alignment author required") + if review["status"] == "reviewed": + require(isinstance(review["reviewer"], str) and review["reviewer"], f"{cid}: reviewed alignment needs a reviewer") + require(isinstance(review["record"], str), f"{cid}: reviewed alignment needs a record path") + local_file(root, review["record"]) + decl, lean_file, source_id, anchor = (claim.get(k) for k in ("lean_declaration", "lean_file", "source", "informal_anchor")) + require(isinstance(decl, str) and re.fullmatch(r"[A-Za-z_][\w'.]*", decl), f"{cid}: invalid lean_declaration") + require(lean_file in lean_files and lean_file.endswith(".lean"), f"{cid}: lean_file must be a registered .lean file") + if lean_file not in declared_cache: + declared_cache[lean_file] = declared_names(strip_lean_comments(lean_files[lean_file].decode("utf-8"))) + if decl not in declared_cache[lean_file]: + problems.append(f"{cid}: declaration {decl} not found in {lean_file}") + require(source_id in sources, f"{cid}: unknown source {source_id!r}") + require(isinstance(anchor, str) and anchor.strip(), f"{cid}: informal_anchor must be a nonempty string") + if anchor not in sources[source_id]: + problems.append(f"{cid}: informal anchor is not a verbatim substring of source {source_id}") + if status in ("proved", "kernel-checked"): + audited[decl] = (cid, status) + return {"counts": counts, "alignment": alignment_counts, "audited": audited} + + +def parse_audit(text: str) -> dict: + result = {} + for line in text.splitlines(): + match = AUDIT_LINE.match(line.strip()) + if match: + axioms = match.group("axioms") + result[match.group("name")] = set() if axioms is None else {a.strip() for a in axioms.split(",") if a.strip()} + return result + + +def check_axioms(data: dict, audited: dict, audit_text: str, problems: list) -> dict: + if re.search(r"\berror\b", audit_text): + problems.append("axiom audit output reports an error") + parsed = parse_audit(audit_text) + allowed, forbidden = set(data["allowed_axioms"]), set(data["forbidden_axioms"]) + for decl, (cid, status) in audited.items(): + if decl not in parsed: + problems.append(f"{cid}: {decl} missing from axiom audit output") + continue + used = parsed[decl] + if status == "kernel-checked" and not used <= allowed: + problems.append(f"{cid}: {decl} depends on non-allowed axioms {sorted(used - allowed)}") + if used & forbidden: + problems.append(f"{cid}: {decl} depends on forbidden axioms {sorted(used & forbidden)}") + return {"declarations_reported": len(parsed), "declarations_required": len(audited)} + + +def lake_binary() -> str | None: + found = shutil.which("lake") + if found: + return found + candidate = Path.home() / ".elan/bin/lake" + return str(candidate) if candidate.is_file() else None + + +def run_lean(root: Path, data: dict) -> str: + lake = lake_binary() + if lake is None: + raise OSError("lake not found on PATH or in ~/.elan/bin") + project = local_file(root, f"{data['project_root']}/lean-toolchain").parent + env = dict(os.environ, PATH=f"{Path(lake).parent}{os.pathsep}{os.environ.get('PATH', '')}") + build = subprocess.run([lake, "build"], cwd=project, capture_output=True, text=True, env=env) + if build.returncode != 0: + raise OSError("lake build failed:\n" + build.stdout[-4000:] + build.stderr[-4000:]) + audit_rel = PurePosixPath(data["audit_module"]).relative_to(data["project_root"]).as_posix() + audit = subprocess.run([lake, "env", "lean", audit_rel], cwd=project, capture_output=True, text=True, env=env) + if audit.returncode != 0: + raise OSError("axiom audit failed:\n" + audit.stdout[-4000:] + audit.stderr[-4000:]) + return audit.stdout + + +def render_alignment(data: dict) -> str: + lines = ["# Informal–formal alignment table", "", + "Generated from `formal/registry.json` by `tools/formal_gate_check.py --write-alignment`; do not hand-edit.", + "Each row pairs one Lean declaration with the verbatim informal text it is attached to. The kernel checks the", + "declaration; the alignment review lane checks that the declaration says what the anchor says. Status here is", + "formalization status only and changes no Layer 0 review outcome.", "", + "| Claim | Layer 0 object | Status | Alignment | Lean declaration | Informal anchor | Does not claim |", + "|---|---|---|---|---|---|---|"] + for claim in data["claims"]: + anchor = claim["informal_anchor"] + anchor_cell = "—" if anchor is None else "`" + " ".join(anchor.split()).replace("`", "'").replace("|", "\\|") + "`" + decl = "—" if claim["lean_declaration"] is None else f"`{claim['lean_declaration']}`" + cells = [claim["id"], claim["layer0_object"], claim["status"], claim["alignment_review"]["status"], decl, + anchor_cell, claim["does_not_claim"]] + lines.append("| " + " | ".join(c.replace("|", "\\|") if i != 5 else c for i, c in enumerate(cells)) + " |") + lines.append("") + return "\n".join(lines) + + +def check(root: Path, registry: str = REGISTRY, axioms_output: Path | None = None, static_only: bool = False, + run: bool = False, alignment: str | None = None) -> dict: + root = root.resolve() + data = load_registry(root, registry) + problems: list[str] = [] + lean_files = check_lean_files(root, data, problems) + sources = check_sources(root, data, problems) + claims = check_claims(root, data, lean_files, sources, problems) + audit_summary: dict | str + if run: + audit_summary = check_axioms(data, claims["audited"], run_lean(root, data), problems) + elif axioms_output is not None: + audit_summary = check_axioms(data, claims["audited"], Path(axioms_output).read_text(encoding="utf-8"), problems) + elif static_only: + audit_summary = "NOT RUN (--static-only): kernel and axiom lane unchecked in this invocation" + else: + raise ValueError("axiom lane required: pass --axioms-output FILE, --run-lean, or --static-only") + if alignment is not None: + try: + current = local_file(root, alignment).read_text(encoding="utf-8") + except ValueError as exc: + problems.append(f"alignment table: {exc}") + else: + if current != render_alignment(data): + problems.append(f"{alignment}: differs from the registry rendering; regenerate with --write-alignment") + return {"scope": data["scope"], "lean_toolchain": data["lean_toolchain"], "lean_files": len(lean_files), + "sources": len(sources), "claims": sum(claims["counts"].values()), "status_counts": claims["counts"], + "alignment_counts": claims["alignment"], "cross_checks": len(data["cross_checks"]), + "axiom_audit": audit_summary, "problems": problems} + + +def refresh_hashes(root: Path, registry: str) -> int: + path = local_file(root, registry) + data = json.loads(path.read_text(encoding="utf-8"), object_pairs_hook=unique_pairs) + changed = 0 + for item in data["lean_files"]: + digest = sha256(local_file(root, item["path"]).read_bytes()) + if item["sha256"] != digest: + item["sha256"] = digest + changed += 1 + path.write_text(json.dumps(data, indent=2, ensure_ascii=False) + "\n", encoding="utf-8") + return changed + + +def main(argv=None) -> int: + parser = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument("--root", type=Path, default=ROOT) + parser.add_argument("--registry", default=REGISTRY) + parser.add_argument("--axioms-output", type=Path, help="captured output of `lake env lean `") + parser.add_argument("--run-lean", action="store_true", help="run lake build and the axiom audit now") + parser.add_argument("--static-only", action="store_true", help="skip the kernel/axiom lane and say so") + parser.add_argument("--alignment", default="formal/ALIGNMENT.md", help="alignment table to compare against the registry") + parser.add_argument("--no-alignment", action="store_true", help="do not compare the alignment table") + parser.add_argument("--write-alignment", action="store_true", help="regenerate the alignment table and exit") + parser.add_argument("--refresh-hashes", action="store_true", help="rewrite lean_files hashes from disk and exit") + args = parser.parse_args(argv) + try: + if args.write_alignment: + data = load_registry(args.root.resolve(), args.registry) + (args.root.resolve() / args.alignment).write_text(render_alignment(data), encoding="utf-8") + print(f"wrote {args.alignment}") + return 0 + if args.refresh_hashes: + print(f"updated {refresh_hashes(args.root, args.registry)} lean_files hashes") + return 0 + result = check(args.root, args.registry, args.axioms_output, args.static_only, args.run_lean, + None if args.no_alignment else args.alignment) + except (ValueError, OSError, TypeError, KeyError, UnicodeDecodeError) as exc: + print(f"formal_gate_check: INVALID_INPUT: {exc}") + return 2 + print(json.dumps(result, indent=2, sort_keys=True)) + print("Scope: formalization registry, Lean file identity, informal anchors, and axiom audit only. " + "Kernel-checked arithmetic is not acceptance of the surrounding analytic argument or of any Layer 0 claim.") + return 1 if result["problems"] else 0 + + +if __name__ == "__main__": + raise SystemExit(main()) From 8b684330393a65186b4a819e14c00563e132524d Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Sun, 27 Sep 2026 21:51:43 +0000 Subject: [PATCH 2/3] Document the formal layer: README, glossary, alignment review lane, cross-repo rollout record - formal/README.md: Layer 0 / Layer 1 architecture, status levels, pilot scope and non-claims, run instructions, expansion path (Mathlib lane, specified statements, explicit parent axioms, Lean Blueprint, AI-prover cross-check lane, external validation). - formal/GLOSSARY.md: project terminology -> standard objects -> Lean, for Gaussian persistence, RN counting, P15 and process terms. - formal/REVIEW_LANE.md + reviews/TEMPLATE.md: statement-alignment review lane, distinct from kernel checking and from Layer 0 review. - docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md: coordination record for all agents and repositories: owner instruction, what landed, what did not change, design rationale, per-repository requests, capability limits. - Front door: README verification-stack section, AGENTS/CONTRIBUTING/ WORKSPACE/RESEARCH_INDEX pointers; landing and navigation manifests now check the new pages. STATUS.md deliberately untouched (byte-pinned). Co-authored-by: Dylan Roy --- AGENTS.md | 10 ++ CONTRIBUTING.md | 34 ++++ README.md | 15 ++ docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md | 168 +++++++++++++++++++ docs/LANDING_MANIFEST.json | 7 +- docs/NAVIGATION.json | 6 +- docs/RESEARCH_INDEX.md | 1 + docs/WORKSPACE.md | 16 ++ formal/GLOSSARY.md | 79 +++++++++ formal/README.md | 153 +++++++++++++++++ formal/REVIEW_LANE.md | 64 +++++++ formal/reviews/TEMPLATE.md | 27 +++ 12 files changed, 578 insertions(+), 2 deletions(-) create mode 100644 docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md create mode 100644 formal/GLOSSARY.md create mode 100644 formal/README.md create mode 100644 formal/REVIEW_LANE.md create mode 100644 formal/reviews/TEMPLATE.md diff --git a/AGENTS.md b/AGENTS.md index d6eaef156..046f4257c 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -30,3 +30,13 @@ not a reason to ask for permission already granted. Drive record, and collaboration surfaces. This `main` initially contains the renewed landing, not the complete research stack. Bring improvements into it coherently; there is no permanent landing-only restriction. + +## Verification stack + +Layer 0 is the existing provenance, scope and source-bound review system. Layer 1 is +the Lean 4 formal layer in [`formal/`](formal/README.md): kernel-checked statements +bound by hash to Layer 0 bytes, one formalization status per claim in +[`formal/registry.json`](formal/registry.json), a glossary, and a statement-alignment +review lane. Read the [rollout record](docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md) +before touching either layer: it says what changed, why, what each repository is asked +to do, and that no formalization status ever moves a Layer 0 status. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 7f7b34229..566db9a5e 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -142,6 +142,40 @@ back regardless of how good the result looks. - **Python 3.11, standard library only.** `pytest` is the single test dependency; guard any `mpmath` or `numpy` import and skip when absent. +## Formal verification (Lean 4, Layer 1) + +The [`formal/`](formal/README.md) directory holds Lean 4 statements and proofs +bound by hash to the exact Layer 0 bytes they formalise, and +[`formal/registry.json`](formal/registry.json) records one **formalization +status** per claim: `none`, `specified`, `proved`, or `kernel-checked`. Rules: + +- **Register every Lean file and every declaration you want counted.** The gate + (`tools/formal_gate_check.py`) refuses unregistered `.lean` files, hash + mismatches, `sorry`, `native_decide`, and any `axiom` not listed in + `project_axioms` with a scope note. After editing Lean text run + `--refresh-hashes`, then `--write-alignment`, then the gate with the kernel lane + (`--run-lean` or `--axioms-output`), never only `--static-only`. +- **`kernel-checked` means allowed axioms only.** `propext`, `Classical.choice`, + `Quot.sound` or none. A proof that leans on a project axiom (an unformalised + parent theorem stated explicitly with a scope note) is `proved`, not + `kernel-checked`, until the parent is formalised. +- **Every Lean statement carries a verbatim `informal_anchor`** from a + byte-pinned local source copy under `formal/sources/`, and a `does_not_claim`. + Core Lean has no rationals: state rational identities as cross-multiplied + integers and give the rational form in the docstring. +- **Statement alignment is its own review.** AI- or human-authored Lean text is + author-side until a distinct reviewer records, under `formal/reviews/`, that + the Lean statement says what the anchor says. Follow + [`formal/REVIEW_LANE.md`](formal/REVIEW_LANE.md). Same-provider reviewers earn + zero independence credit, as everywhere else in this repository. +- **Formalization status never moves Layer 0 status.** A `kernel-checked` lemma + does not edit `STATUS.md`, `PROOF_INDEX.md` or any ACCEPT/AMEND row, and does + not make the surrounding analytic argument verified. Use the vocabulary in + [`formal/GLOSSARY.md`](formal/GLOSSARY.md) when writing for external readers. +- **Mathlib is a separate step.** The pilot is dependency-free on purpose. A + Mathlib lane (needed for `ℝ`, `Real.Gamma`, `Real.log`, Gaussian measures) + changes CI cost and is proposed in its own PR. + ## Claims and status - **No status moves by merge.** Commits, tests, receipts and reviews cannot diff --git a/README.md b/README.md index 5f5647da9..5239fffe6 100644 --- a/README.md +++ b/README.md @@ -84,6 +84,21 @@ For full proof texts, use **[Public mathematics](docs/PUBLIC_MATHEMATICS.md)**. - Numerical or floating-point work is labeled non-certifying when it is not a proof. - Independent review is recorded separately from same-author checks. - A merge, green CI run, hash match, publication, or model agreement does not promote mathematical status. +- A kernel-checked Lean lemma verifies exactly its own statement; it does not verify the analytic argument around it or promote a Layer 0 status. + +## Verification stack + +| Layer | What it checks | Where | +|---|---|---| +| **Layer 0 — provenance, scope, review** | Exact bytes (SHA-256, Git blobs), declared scope and "does not claim" statements, source-bound nonauthor review, fail-closed intake and landing gates | [`STATUS.md`](STATUS.md), [Math- proof index](https://github.com/d6g8k5htny-coder/Math-/blob/d6628da09384728992dcbe6e921cc28ba85aebb0/PROOF_INDEX.md), [public inventory](docs/public-math/sources.json), [museum](https://d6g8k5htny-coder.github.io/main/site/museum.html) | +| **Layer 1 — formal (Lean 4)** | Statements and proofs checked by the Lean kernel, bound by hash to Layer 0 bytes, with a per-claim formalization status (`none` / `specified` / `proved` / `kernel-checked`) and a statement-alignment review lane | [`formal/README.md`](formal/README.md), [`formal/registry.json`](formal/registry.json), [glossary](formal/GLOSSARY.md), [review lane](formal/REVIEW_LANE.md) | + +The pilot formalises the arithmetic skeleton of the SIDE24 coefficient note: 31 kernel-checked, axiom-free theorems. The coefficient bound itself and every analytic step remain Layer 0 prose with formalization status `none`. See the [rollout record](docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md) for what changed, why, and what each repository is asked to do next. + +```sh +python3 tools/formal_gate_check.py --run-lean # needs elan/lake; see formal/README.md +python3 -B -S -m unittest tests.test_formal_gate -v +``` ## Research still in progress diff --git a/docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md b/docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md new file mode 100644 index 000000000..3b38c9f3a --- /dev/null +++ b/docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md @@ -0,0 +1,168 @@ +# Formal verification rollout — 2026-09-27 + +Coordination record for all participating agents, current and future, across +`main`, `Math-`, `query-`, `meta-framework` and `Universal-Law-Workspace`. This +file explains **what** was added, **why**, **what it does not change**, and +**what each repository is asked to do next**. Read it before touching +`formal/`, `STATUS.md`, `PROOF_INDEX.md` or any acceptance workflow. + +## Owner instruction + +Dylan Roy, 2026-09-27, in the request that started this work (recorded verbatim +in the pull request that landed this file): + +> As we get closer to retrieving all the information for the github and +> following the intent behind what we're aiming to achieve I think it's time we +> incorporate the below so we further our goals. […] Read it and then understand +> how it will better our project and then implement anything and everything. Be +> sure to coordinate with all other agents and future agents for all +> repositories so they will be aware of the changes and why, I Dylan Roy pre +> approve any decision, request, or action needed to achieve this goal + +The "below" was a roadmap produced by another AI model in answer to Dylan's +question about how the project's proofs could be verified by Lean, Coq, +Metamath, AI provers and traditional peer review. Its core diagnosis: the +existing system has strong **provenance, scope discipline, a hard fail-closed +gate and a public verification museum**, but no **logical verification** — a +trusted kernel checking that each proof is valid. Its core proposal: keep all +of that as **Layer 0** and add a **Layer 1** of Lean 4 statements and proofs, +bound by hash to the Layer 0 bytes, with a per-claim **formalization status** +(`none` / `specified` / `proved` / `kernel-checked`), a **glossary** mapping +project terminology to standard mathematics, a **formalization review lane** +for statement alignment, an extended **hard gate** requiring Lean compilation +for anything promoted beyond author-side candidate, and an **AI-prover +cross-check lane**. This is consistent with the +[current owner instruction](../governance/OP-AUTONOMY-20260923-v2.1.md) and +with [AGENTS.md](../AGENTS.md): it extends the verification stack; it creates no +new permission queue. + +## What landed in `main` + +| Item | Where | State | +|---|---|---| +| Lean 4 project, pinned toolchain `v4.34.1`, no external dependencies | [`formal/`](../formal/README.md) | builds in < 1 s | +| Pilot: SIDE24 arithmetic skeleton — 31 theorems, all `kernel-checked`, zero axioms | `formal/UniversalLaw/Side24/*.lean` | done | +| Formalization registry with status levels, hashes, byte-pinned informal anchors, axiom allow/deny lists, alignment lane, cross-check lane | [`formal/registry.json`](../formal/registry.json) | 38 claims: 31 kernel-checked, 7 `none` | +| Byte copies of the exact sources the Lean text is attached to | `formal/sources/side24_v1/` | `Math-@9d7b6802…`, hashes pinned | +| Generated informal–formal alignment table | [`formal/ALIGNMENT.md`](../formal/ALIGNMENT.md) | regenerated by the gate | +| Glossary: project terms → standard objects → Lean | [`formal/GLOSSARY.md`](../formal/GLOSSARY.md) | first pass, D1/D5 entries say "read the source" | +| Formalization review lane and record template | [`formal/REVIEW_LANE.md`](../formal/REVIEW_LANE.md), `formal/reviews/` | lane defined; all pilot rows `open` | +| Fail-closed gate | [`tools/formal_gate_check.py`](../tools/formal_gate_check.py) | 38 controls in `tests/test_formal_gate.py`, 5 Lean mutants rejected | +| CI lane | `.github/workflows/formal-verification.yml` | installs elan, `lake build`, axiom audit, gate, controls | +| Front-door wiring | `README.md`, `CONTRIBUTING.md`, `AGENTS.md`, `docs/WORKSPACE.md`, `docs/RESEARCH_INDEX.md`, landing and navigation manifests | links added; `STATUS.md` untouched — it is a byte-pinned snapshot read by the museum and shop tests, so the formalization lane is described beside it in `README.md` rather than inside it | + +Verified locally: `lake build` succeeds; `lake env lean UniversalLaw/Audit.lean` +reports every registered declaration free of axioms; +`python3 tools/formal_gate_check.py --run-lean` returns `problems: []`; the 38 +controls pass in normal and `-O` interpreter modes; five tightened-bound mutants +of `Ledger.lean` are rejected by Lean with "proved that the proposition … is +false". The CI workflow was written but had not yet run on GitHub at the time +this file was written; its first run is the PR's own check. + +## What did not change + +- No row of `STATUS.md`, no line of `PROOF_INDEX.md`, no `LANDING_CLAIMS`, + `claims/`, prize or `lemma_closed` value. `formal/registry.json` declares + `scientific_status_authority: false` and the gate refuses a registry that says + otherwise. +- No Layer 0 review verdict. The SIDE24 coefficient bound is still "ACCEPT — + scoped" by source-bound review and **`none`** in formalization status: the + kernel checked its arithmetic skeleton, not its analysis. +- No parent theorem became accepted, no AMEND item closed. +- AI authorship labels: the Lean text is author-side (Anthropic / Claude, + Cursor cloud agent) until a distinct reviewer records alignment. + +## Why this design, in this order + +- **Core Lean first, Mathlib second.** Everything statable about the pilot in + core Lean is now checked, with a sub-second build and no cache. Statements + that need `ℝ`, `Real.Gamma`, `Real.exp`, `Real.pi`, Gaussian measures or + matrices are listed as `none` with their blockers, not hidden. Adding Mathlib + changes CI cost (multi-GB cache, longer timeouts) and is its own reviewable + step. +- **Status is per claim, granular.** One registry row per Lean declaration, + each with a verbatim anchor and a `does_not_claim`. Coarse "SIDE24 is + formalised" labels would be exactly the kind of unearned promotion the + existing gate exists to prevent. +- **Anchors before Blueprint.** Lean Blueprint needs LaTeX + plasTeX tooling. + The registry's verbatim-substring anchors give a checkable informal–formal + link now and are the seed text for a Blueprint document later. +- **Kernel audit, not build success, is the criterion.** A green `lake build` + admits `sorry` warnings and `native_decide`. The gate parses `#print axioms` + and fails on `sorryAx`, `Lean.ofReduceBool`, or any axiom outside + `propext`, `Classical.choice`, `Quot.sound` for `kernel-checked` rows. + +## Requests to each repository and to future agents + +These are coordination requests under the same owner instruction; they need no +further permission. Discuss overlaps in the existing +[downstream-first queue #86](https://github.com/d6g8k5htny-coder/main/issues/86) +or on the PR that landed this file. + +**`main` (this repository)** +- Keep `formal/registry.json` the single formalization-status register. Do not + add a second one in another repository. +- When you add Lean text: register every file (the gate refuses unregistered + `.lean` files), run `--refresh-hashes`, then `--write-alignment`, then the gate. +- Nonauthor agents: pick up the alignment review of the 31 `open` pilot rows + using `formal/REVIEW_LANE.md`. Different-provider reviewers earn independence + credit; same-provider reviewers do not. +- Next formalization targets, in the order the pilot suggests: (1) Mathlib lane + bootstrap as a separate PR; (2) D6 Theorem F constant `ρ* = 1/(3 − log(3e − 2))` + and its 20-digit enclosure and `ρ* < 6/7` (`specified`, then `kernel-checked` + via `Real.log` bounds); (3) `c_{d,ref}` as a `specified` definition; (4) the + `coefficient.py` interval enclosures re-derived in Lean. +- Museum / shop: a "formalization" lane in `docs/site/` is a natural follow-up; + it must read the registry, display `scientific_status_authority: false`, and + never merge the two status vocabularies. + +**`Math-`** +- Add one line to `PROOF_INDEX.md` under the D3 entry pointing to + `main/formal/registry.json` and stating that the arithmetic skeleton is + kernel-checked and the analytic content is not. Do not change the D3 verdict. +- New proof notes should carry a `Formalization:` line in their header + (`none` by default) so the status is visible at the source, and should keep + exact decimal or rational constants displayed so anchors can quote them. +- Frozen bodies stay frozen; a formalisation attaches to bytes by hash and + never edits them. If formalisation finds a defect, it is an erratum successor, + as now. + +**`meta-framework`** +- Consider a `formalization` field per source entry in `registry.json` + (`none` / `specified` / `proved` / `kernel-checked`, with the `main` registry + commit). Keep it descriptive; the `main` registry remains authoritative. + +**`query-`** +- No change required. If the package later exposes Lean file identities, use + the same `repository + path + commit + blob + bytes + sha256` row shape. + +**`Universal-Law-Workspace`** +- Navigation only: link `main/formal/README.md`. It stays + `scientific_status_authority: false`. + +**All agents** +- A `kernel-checked` row is a kernel-checked row. It is not "verified" in the + Layer 0 sense and must not be written up as if the surrounding theorem were. +- A `none` row is a visible target, not a defect. +- Before claiming a formal result, run the gate with the kernel lane + (`--run-lean` or `--axioms-output`), not `--static-only`, and quote the output. + +## Cross-repository capability note + +This cloud agent could push only to `main` in this session; the `Math-`, +`meta-framework`, `query-` and `Universal-Law-Workspace` requests above are +recorded here and in the PR for other agents to pick up. Posting to issue #86 +was not possible from this agent (its GitHub CLI is read-only); an agent with +write access should link this file there. These are capability limits of this +session, reported as such; they are not requests for permission. + +## Uncertain or not verified + +- Whether GitHub Actions can download the Lean toolchain within the workflow's + timeout on the first run (expected: yes, ~200 MB). +- Whether the informal anchors chosen for the four `Endpoints.lean` theorems + are the best pairing; two of them anchor to `ENCLOSURE.json` metadata rather + than to a mathematical sentence, because the JSON has no prose. An alignment + reviewer should say whether that is acceptable. +- The glossary mappings for D1 (matrix cap, marked cylinder, elder selection) + and the D5 region names were not extracted from their sources in this session. diff --git a/docs/LANDING_MANIFEST.json b/docs/LANDING_MANIFEST.json index 159d68d65..c0fa86692 100644 --- a/docs/LANDING_MANIFEST.json +++ b/docs/LANDING_MANIFEST.json @@ -8,7 +8,12 @@ "docs/WORKSPACE.md", "docs/RESEARCH_INDEX.md", "docs/REPRODUCE.md", - "history/2025/README.md" + "history/2025/README.md", + "docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md", + "formal/README.md", + "formal/GLOSSARY.md", + "formal/REVIEW_LANE.md", + "formal/ALIGNMENT.md" ], "historical_files": [ { diff --git a/docs/NAVIGATION.json b/docs/NAVIGATION.json index 4190e7e21..61f18bc89 100644 --- a/docs/NAVIGATION.json +++ b/docs/NAVIGATION.json @@ -24,7 +24,11 @@ "docs/notebooks/README.md", "docs/PUBLIC_SHOP_SETUP.md", "docs/rn_d5_shrinking_witness_20260926.md", - "docs/QUEUE_RECONCILIATION_20260927.md" + "docs/QUEUE_RECONCILIATION_20260927.md", + "docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md", + "formal/README.md", + "formal/GLOSSARY.md", + "formal/REVIEW_LANE.md" ], "public_targets": [ { diff --git a/docs/RESEARCH_INDEX.md b/docs/RESEARCH_INDEX.md index 901c3ddbc..cb8f8918a 100644 --- a/docs/RESEARCH_INDEX.md +++ b/docs/RESEARCH_INDEX.md @@ -63,6 +63,7 @@ The full-range successor removes the probability ceiling, not the demand or real | RN fixed-remote successor | Review the extra-pin count proof, evaluate its kernel, and control the remaining shrinking-exclusion/collision regions | [#76](https://github.com/d6g8k5htny-coder/main/issues/76) | | RN shrinking witness pairs | Divided-difference `m=2` upper bound at fixed distance from the pins; sharp order and kernel still open | [Note](rn_d5_shrinking_witness_20260926.md) | | P15 | Review full-range hazard transfer and sharpness; extend beyond the realized-family hypotheses | [#74](https://github.com/d6g8k5htny-coder/main/issues/74), [#67](https://github.com/d6g8k5htny-coder/main/issues/67) | +| Formalization (Layer 1) | Alignment-review the 31 `open` SIDE24 pilot declarations; bootstrap a Mathlib lane in its own PR; state D6 Theorem F's constant `ρ*` and the SIDE24 reference coefficient as `specified` Lean statements | [Formal README](../formal/README.md), [review lane](../formal/REVIEW_LANE.md), [rollout record](FORMAL_VERIFICATION_ROLLOUT_20260927.md) | Check current claims before writing and release completed work. Offered reviews are not accepted tasks or evidence of active agents. This table is a route to current discussions, not a duplicate status database. diff --git a/docs/WORKSPACE.md b/docs/WORKSPACE.md index 76b5fec8f..ae05e62e7 100644 --- a/docs/WORKSPACE.md +++ b/docs/WORKSPACE.md @@ -57,5 +57,21 @@ research code into `main` should bring its relevant verification with it; a gree landing check is not full research CI. Agents may replace or expand this workflow as the workspace changes. +## Formal layer check + +The `formal-verification` workflow builds the Lean 4 library in [`formal/`](../formal/README.md), +audits axioms, and runs the fail-closed formalization gate. Locally, after installing +elan (see the formal README): + +```sh +python3 tools/formal_gate_check.py --run-lean +python3 -B -S -m unittest tests.test_formal_gate -v +``` + +A green run means the registered declarations are kernel-checked with allowed axioms +only and the registry, hashes and informal anchors agree. It is formalization status, +not mathematical acceptance; the [rollout record](FORMAL_VERIFICATION_ROLLOUT_20260927.md) +explains the boundary. + [Current authority](../governance/OP-AUTONOMY-20260923-v2.1.md) · [Home](../README.md) · [Historical material](../history/2025/README.md) diff --git a/formal/GLOSSARY.md b/formal/GLOSSARY.md new file mode 100644 index 000000000..25d05c0f5 --- /dev/null +++ b/formal/GLOSSARY.md @@ -0,0 +1,79 @@ +# Formal glossary — project terms → standard mathematics → Lean + +Every non-standard term used in the project's proofs must map to a standard +mathematical object before it can be formalised. If a term cannot be mapped, it +is either ill-defined or genuinely novel, and novelty has to be justified by +comparison with the literature (see the +[reconnaissance memo](../docs/RECON_NOVELTY_20260925.md)). This table is the +mapping. It is descriptive — it reports how the pinned sources use each term — +and it does not accept or reject any result. + +Sources read for these entries: the SIDE24 note +([`sources/side24_v1/PROOF.md`](sources/side24_v1/PROOF.md)), the D2 remainder +note (`Math-` `frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md`), the D4 +remote-window proof (`frontiers/remote_window_20260924/PROOF.md`), the D6 +full-price proof (`frontiers/full_price_20260924/PROOF.md`) and +[STATUS.md](../STATUS.md). Where an entry says "read the source", the standard +mapping still has to be extracted by whoever formalises that object. + +Lean column: `—` means no Lean object yet; `core` means statable in core Lean; +`Mathlib` means the standard object exists in Mathlib and a Mathlib lane is +needed to state it. + +## Gaussian persistence (D1, D2, D3) + +| Project term | Standard object | Lean | +|---|---|---| +| **Periodized field**, `K_L`, `K_24` | Centred, variance-one stationary Gaussian random field on the flat torus `X = ℝ^d/(LZ^d)` whose covariance is the normalised theta-function periodisation of the Gaussian kernel `exp(−|z|²/2)`. `SIDE24` is the case `L = 24`. | Mathlib: `MeasureTheory` Gaussian measures, `AddCircle`; the covariance kernel itself is statable in core as a series but not usable | +| **Reference / CONTACT covariance**, `K_∞` | The unperiodised kernel `exp(−|z|²/2)` used only to define the reference coefficient `c_{d,ref}`; no infinite-volume theorem is claimed | Mathlib: `Real.exp` | +| **Pins** `M = −ru/2`, `S = ru/2` | Two conditioning points on the axis `u` at separation `r`, with prescribed heights `b`, `b − k r³` and zero gradients | — | +| **Continuous Gaussian regression** `Q`, `Q_r` | Conditional law of a Gaussian field given finitely many linear observations (conditional Gaussian measure) | Mathlib (partial) | +| **Endpoint weight** `W`, **FULL normalizer** `Z = E_Q W` | Kac–Rice Jacobian weight `|det H_M| · |det H_S|` times index indicators, and its expectation under the regression law | — | +| **Candidate** pair, **candidate density** `ν_cand(ℓ)` | Ordered (maximum, index-`(d−1)` saddle) critical-point pair with height gap `ℓ`; its density is the intensity of the corresponding marked critical-point-pair process (first-moment / Kac–Rice density) | — | +| **Elder** pair, **elder density** `ν_eld(ℓ)` | Critical-point pair actually paired by the elder rule of superlevel-set `H₀` persistent homology (a finite `H₀` bar of length `ℓ`); density = intensity of finite `H₀` persistence pairs | — | +| **Lifetime** `ℓ` | Persistence (birth minus death height) of an `H₀` bar | core (`ℝ` needs Mathlib) | +| **Lifetime coefficient** `c = c_{d,L}` | The constant in the leading term `c ℓ^{−1/3}` of the small-lifetime density asymptotics; defined by equation (15.2) of the parent note | — | +| **Reference coefficient** `c_{d,ref}` | `Γ(7/6)·(3/2)^{1/3}·D_{d−1} / (2√3·π^{d−1}·√π)`, display (1) of the SIDE24 note | Mathlib: `Real.Gamma`, `Real.pi`, `Real.sqrt`, rpow | +| **Cone moment** `D_m` | `E[det(A)² · 1{A ≺ 0}]` for a specified Gaussian symmetric `m×m` matrix `A`; a moment of the squared determinant over the negative-definite cone. `D_1 = 4/3`, `D_2 = 29/6 − √6` | Arithmetic parts: core (`cone_moment_m1_thirds`, `cone_moment_m2_algebra`); the integrals: Mathlib | +| **Image ledger**, **omitted periodic image** | Deterministic bound on the difference between derivatives of the periodised and unperiodised kernels at `0`, i.e. on the Poisson-summation image terms `n ≠ 0` | Arithmetic parts: core (`image_constant_value`, `covariance_relative_bound`, `exp_taylor_partial_sum_gt_ten`) | +| **Outward arithmetic** | Rational interval arithmetic with outward rounding to a fixed grid (`10^-80`), containment unconditional | — (would be Mathlib `Set.Icc` over `ℚ`) | +| **Matrix cap**, **marked cylinder**, **elder selection** (D1) | Read the parent source (`imports/lifetime_parent_20260925/`); the D1 selection chain is itself AMEND at Layer 0 and has no agreed standard mapping yet | — | +| **RN / JETMOD / 24-jet obligations** | Historical downstream proof obligations tracked in `frontiers/downstream_gate_20260925/GRAPH.json`; not a single mathematical object | — | + +## RN counting (D4, D5) + +| Project term | Standard object | Lean | +|---|---|---| +| **Remote critical point** | Critical point `x` with `dist_X(x, 0) ≥ ρ`, i.e. outside a fixed neighbourhood of the two pins | — | +| **Height window** (between-pin) | The height interval `(b − k r³, b)` between the pinned saddle and maximum | — | +| **RN count** `N_{r,j}(E)` | Number of critical points of Morse index `j` in a Borel set `E` with height in the window; its expectation is a Kac–Rice integral | — | +| **Three determinant factors** | The Kac–Rice integrand factors `|det H|` at the two pins and at the counted point, under the regression law | — | +| **Contact kernel** | The positive mean kernel identified in the D4 proof for the counted point's conditional Hessian; read the source (section on the contact mean kernel) | — | +| **Fixed-remote** vs **shrinking** `ρ`, `η` | Whether the spatial exclusion radius `ρ` and witness separation `η` are held fixed as `r → 0` or allowed to shrink with `r` | — | +| **Pin neighbourhood**, **microdisk**, **collar**, **annulus** | Regions at distance `≲ r²`, `≪ r`, between scales, and at fixed scaled radius from the pins respectively (D5 decomposition); read the D5 sources | — | +| **Witness collision** | Two counted critical points whose mutual separation tends to zero (factorial-moment / second-moment regime) | — | + +## P15 combinatorics (D6) + +| Project term | Standard object | Lean | +|---|---|---| +| **Realized family** | The decreasing (downward-closed) set family `D` on disjoint coordinate blocks `X_i` with `|X_i| = a_i d_i + 1`, `|U ∩ X_i| ≤ a_i`, whose occupied-block support contains no edge of the clutter `H` | Mathlib: `Finset`, downsets; statable | +| **Clutter** `H` | Finite antichain of subsets (a Sperner family / simple hypergraph) of block indices | Mathlib: `Finset` antichain | +| **Palette** `K`, `K_H(d)` | Number of colour classes; `K_H(d)` the least `K` admitting classes `P_i` with `|P_i| ≥ d_i` and empty intersection over every `H`-edge | Mathlib: statable | +| **Capacity / demand** `d_i` | Per-block integer parameter; `d_i ≥ 2` is an essential hypothesis (demand one has an exact counterexample) | core | +| **Price** `c_v`, **transformed price** `φ(p) = min(1, −log(1−p))` | A weight per coordinate bounded by the hazard transform of its probability | Mathlib: `Real.log` | +| **Cover cost** `covercost_c(O_K(D))` | Minimum total generator price of a family covering the sets not partitionable into `K` members of `D` | Mathlib: statable | +| **Global hazard** `−log μ_p(D)` | Negative log of the product-measure probability of `D` | Mathlib: `Real.log`, finite product measure | +| **Sharp factor** `ρ* = 1/h*`, `h* = 3 − log(3e − 2)` | The constant in Theorem F; published enclosure `0.84547981724898672067 < ρ* < 0.84547981724898672068 < 6/7` | Mathlib: `Real.log`, `Real.exp`; a good `norm_num`/`Real.log` bound target | + +## Governance / process terms + +| Project term | Meaning here | +|---|---| +| **Layer 0** | Existing provenance, scope, review and CI system (hashes, `STATUS.md`, `PROOF_INDEX.md`, source-bound review, public-intake guard) | +| **Layer 1** | This Lean layer: statements and proofs checked by the Lean kernel and bound to Layer 0 bytes | +| **Author-side** | Produced by the author (human or model) and not yet checked by a distinct reviewer; applies equally to AI-generated Lean text | +| **Alignment review** | A distinct reviewer's check that a Lean statement says what the informal statement says at the stated scope; it does not re-prove the theorem (the kernel did) | +| **Informal anchor** | A verbatim quote from the pinned source bytes that a Lean declaration is attached to; verified as a substring by the gate | +| **Kernel-checked** | Compiles with only `propext`, `Classical.choice`, `Quot.sound` (or no axioms); see `registry.json` `status_levels` | +| **Cross-check lane** | An independent AI prover producing a proof of the same Lean statement; extra evidence, same kernel, still author-side | diff --git a/formal/README.md b/formal/README.md new file mode 100644 index 000000000..c94514416 --- /dev/null +++ b/formal/README.md @@ -0,0 +1,153 @@ +# Formal verification layer (Layer 1) + +This directory adds machine-checked logic to the existing provenance-and-review +system without replacing any of it. The existing system — SHA-256 and Git-object +provenance, explicit scope and "does not claim" statements, fail-closed CI, and +source-bound nonauthor review — is **Layer 0**. This directory is **Layer 1**: Lean 4 +statements and proofs that the Lean kernel checks, bound by hash to the exact +Layer 0 bytes they formalise. + +Adopted under the [current owner instruction](../governance/OP-AUTONOMY-20260923-v2.1.md); +the rollout record is [docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md](../docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md). + +## What is in this directory + +| Path | Role | +|---|---| +| `lean-toolchain`, `lakefile.toml`, `lake-manifest.json` | Pinned Lean 4 toolchain (`v4.34.1`) and a dependency-free Lake project | +| `UniversalLaw.lean`, `UniversalLaw/**/*.lean` | The library. Every theorem is kernel-checked by `lake build` | +| `UniversalLaw/Audit.lean` | `#print axioms` for every registered declaration | +| `registry.json` | Per-claim **formalization status**, Lean file hashes, byte-pinned informal anchors, axiom allow/deny lists, alignment-review lane, AI-prover cross-check lane | +| `ALIGNMENT.md` | Generated informal–formal pairing table (from the registry; never hand-edited) | +| `sources/` | Byte copies of the exact Layer 0 sources the Lean text is attached to, pinned by commit, size and SHA-256 | +| `GLOSSARY.md` | Project terminology mapped to standard mathematical objects and (where they exist) Lean names | +| `REVIEW_LANE.md`, `reviews/` | The formalization (statement-alignment) review lane and its records | + +## Formalization status levels + +Each claim in `registry.json` carries exactly one of: + +| Status | Meaning | +|---|---| +| `none` | No Lean object. The claim lives only in Layer 0 prose. | +| `specified` | A Lean statement compiles; no proof is offered. Its hypotheses are the exact claimed scope. | +| `proved` | A Lean proof compiles but depends on project-declared axioms (an unformalised parent taken as an explicit `axiom` with a scope note) or on axioms outside the allow-list. | +| `kernel-checked` | A Lean proof compiles and `#print axioms` reports only `propext`, `Classical.choice`, `Quot.sound` — or nothing. No `sorry`, no `native_decide`, no project axioms. | + +Separately, each Lean statement carries an **alignment review** status: `open` +(author-side; nobody but the author has checked that the Lean statement says +what the informal text says) or `reviewed` (a distinct reviewer recorded that +check under `reviews/`). The kernel guarantees the proof; the alignment review +guarantees the statement is the intended one. Both are needed; neither changes +a Layer 0 review outcome. + +## Current pilot: SIDE24 arithmetic skeleton + +Pilot object: the [SIDE24 coefficient note](sources/side24_v1/PROOF.md) +(`Math-@9d7b6802…`, SHA-256 `c06dacc…`), the D3 row of [STATUS.md](../STATUS.md). + +**Kernel-checked (31 declarations, zero axioms):** every exact integer or rational +identity and inequality that sections 1–4 of the note rely on, stated as +cross-multiplied integer facts because core Lean has no rational type. Examples: +the pairing count `76`; the image constant `1458·(76·24^6+15) = 21175738586478`; +`60E < 10^-108` as `60·21175738586478 < 10^17`; the degree-20 Taylor partial sum of +`exp(288/125)` exceeding `10`; the odd-block minors `2/3`, `7/9` and +`8 − √58 > 1/3` as `23² > 58·9`; the section-4 exponent bounds `a+2b<14`, `2a+b<13` +for `d = 2, 3` (the `d = 3` case is `77 < 78`, so this is tight); the shared trace +variance `5/3`, `E s⁴ = 25/3`, the `D_2 = 29/6 − √6` algebra, and the cube-root +simplification `6^(2/3)/24^(1/3) = (3/2)^(1/3)`; the adjacency of the published +20-digit endpoints. + +**Not formalised (status `none`):** the coefficient bound itself, +`0.07340691930603427103 < c_{2,24} < 0.07340691930603427104`, and every analytic +step — Gaussian conditioning, the cone integral, the derivative bound on +`exp(−|x|²/2)`, the positive-semidefinite covariance comparison, the Stirling +remainder for `Γ(7/6)`, and the `π`, `log`, `exp` enclosures in `coefficient.py`. +Those remain Layer 0 prose under nonauthor review. A kernel-checked arithmetic +skeleton is **not** acceptance of the argument built on it. + +Every kernel-checked declaration is paired in `registry.json` with a verbatim +quote (`informal_anchor`) from the pinned source bytes; the gate fails if the +quote is not a substring of those bytes. This is the alignment mechanism until +a Lean Blueprint build is adopted (see below). + +## Run it + +Toolchain (once; ~200 MB, no Mathlib): + +```sh +curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none +export PATH="$HOME/.elan/bin:$PATH" +``` + +Build, audit, gate, controls (from the repository root): + +```sh +(cd formal && lake build && lake env lean UniversalLaw/Audit.lean > ../audit.txt) +python3 tools/formal_gate_check.py --axioms-output audit.txt +python3 -B -S -m unittest tests.test_formal_gate -v +``` + +`python3 tools/formal_gate_check.py --run-lean` does the build and audit itself. +`--static-only` skips the kernel lane and says so in its output. Without one of +the three the gate refuses to run: the axiom lane is required by default. + +The gate fails closed on: a Lean file whose SHA-256 differs from the registry; a +Lean file present but not registered; `sorry`, `native_decide`, or an `axiom` not +listed in `project_axioms` with a scope note (comments are stripped first — the +kernel's `sorryAx` check is the authoritative guard); a pinned source whose local +copy differs; an informal anchor that is not a verbatim substring; a declaration +missing from its file; a `kernel-checked` declaration missing from the audit or +depending on a non-allowed axiom; any declaration depending on `sorryAx` or +`Lean.ofReduceBool`; an alignment table that drifted from the registry; a +`reviewed` alignment without a reviewer and an existing record file. + +Maintenance commands (these write): `--refresh-hashes` after editing Lean files; +`--write-alignment` after editing the registry. + +## Why core Lean and not Mathlib yet + +The arithmetic skeleton needs only `Nat`/`Int` and `decide`; the kernel evaluates +these with GMP-backed literals in well under a second, so the whole formal lane +adds seconds, not minutes, to CI and needs no multi-gigabyte cache. Mathlib is +required the moment a statement mentions `ℝ`, `Real.Gamma`, `Real.exp`, `Real.pi`, +Gaussian measures or matrices; that is the next expansion and it changes the CI +cost profile (cache download, longer timeouts), so it is a separate, reviewable +step rather than something bundled into the pilot. + +## Expansion path + +1. **Mathlib lane.** Add `mathlib` to `lakefile.toml` at a pinned revision, use + `lake exe cache get` in CI, and move the toolchain to Mathlib's. First targets + that become *statable*: the reference coefficient `c_{d,ref}` (display (1) of + the note); the P15 constant `ρ* = 1/(3 − log(3e − 2))` with its published + 20-digit enclosure and `ρ* < 6/7` (Theorem F, D6 — finite combinatorics plus one + `Real.log`, so the most tractable full-theorem target); the interval-arithmetic + enclosures of `coefficient.py` re-derived with `norm_num`/`interval_cases`. +2. **`specified` statements before proofs.** State D6 Theorem F and the SIDE24 + coefficient bound as Lean `def … : Prop` with hypotheses that are exactly the + Layer 0 scope. Anything not in the hypotheses is not claimed. +3. **Parent dependencies as explicit axioms.** Where a proof needs an unreviewed + parent (for example the D1 selection chain), state it as an `axiom` listed in + `project_axioms` with a scope note. The result is then `proved`, never + `kernel-checked`, until the parent is itself formalised. +4. **Lean Blueprint.** Replace the anchor-substring mechanism with a + `leanblueprint` document (LaTeX prose + `\lean{}` references, dependency graph, + `\leanok` flags). The registry's `informal_anchor` fields are the seed text. +5. **AI-prover cross-check lane.** Run Goedel-Prover / AlphaProof-style systems + on `specified` statements. A success is recorded in `registry.json` under + `cross_checks` with prover, version, date, declaration and record path. It is + still checked by the same kernel, is still author-side until aligned, and does + not replace the alignment review. +6. **External validation.** Papers written in the standard vocabulary of + [GLOSSARY.md](GLOSSARY.md), with the Lean files as supplementary material. + +## What this layer does not do + +It does not change `STATUS.md`, `PROOF_INDEX.md`, `LANDING_CLAIMS`, or any +ACCEPT/AMEND outcome. It does not turn a hash match, a green build, or a +kernel-checked lemma into mathematical acceptance of a theorem. It does not +verify the Python enclosure code. It does not make AI-authored Lean text +independent: the author label stays until a distinct reviewer records the +alignment check. It cannot verify the Mathlib-dependent statements it lists as +`none`; it names them so they are visible targets, not silent gaps. diff --git a/formal/REVIEW_LANE.md b/formal/REVIEW_LANE.md new file mode 100644 index 000000000..69cbe75f7 --- /dev/null +++ b/formal/REVIEW_LANE.md @@ -0,0 +1,64 @@ +# Formalization review lane (statement alignment) + +The Lean kernel checks that a proof is valid. It cannot check that the theorem +proved is the theorem the informal text claims. That check is a human or model +review task with its own lane, distinct from Layer 0 analytic review and from +the author-side act of writing the Lean text. + +## What the reviewer does + +For each Lean declaration under review: + +1. Read the `informal_anchor` in `registry.json` and locate it in the pinned + local source copy (`formal/sources/...`); confirm the surrounding context. +2. Read the Lean statement (not the proof). Decide whether the Lean statement is + the informal statement at the stated scope — the same constants, the same + quantifiers, the same direction of inequality, the same units or scaling + (many pilot statements are cross-multiplied integer forms of rational + identities; the docstring states the rational form — check that the + cross-multiplication is right). +3. Read the `does_not_claim` field. Confirm the Lean statement does not + silently claim more than the anchor, and that what it omits is named. +4. Record the verdict per declaration: `ALIGNED`, `ALIGNED AT NARROWER SCOPE` + (say what is narrower), or `MISALIGNED` (say exactly how). Do **not** grade + the proof; the kernel already did. Do not grade the Layer 0 mathematics; + that is a different lane. + +The reviewer does not need to run Lean to review alignment, but should confirm +the gate is green at the reviewed commit and quote that run. + +## What the reviewer records + +Copy [`reviews/TEMPLATE.md`](reviews/TEMPLATE.md) to +`reviews/__.md`. Record: + +- Reviewer identity and provider. **Same-provider reviewers earn zero + organizational-independence credit** whatever the verdict (this repository's + existing rule; it applies to Lean text exactly as to prose). +- Source exposure: whether the reviewer read the author's Lean proof text or + docstrings before forming a view of the statement. Reading the proof first is + the weakest form of review and must be stated. +- The exact registry commit, Lean file SHA-256 values, and the gate output. +- One row per declaration with the verdict. + +Then, in `registry.json`, set that claim's `alignment_review` to +`{"status": "reviewed", "author": ..., "reviewer": ..., "record": "formal/reviews/.md"}`. +The gate refuses `reviewed` without a reviewer and an existing record file. +A `MISALIGNED` verdict leaves the status `open` and is corrected at the source: +fix the Lean statement (a new hash, a re-run kernel check) or fix the anchor. + +## What this lane cannot do + +- It cannot promote a Layer 0 status. `STATUS.md` and `PROOF_INDEX.md` move only + through their own source-bound review. +- It cannot make an author-side proof independent by relabelling; independence + is recorded from the reviewer's actual identity. +- It cannot substitute for formalising the analytic content. An aligned + arithmetic lemma remains an arithmetic lemma. + +## Current state + +All 31 pilot declarations are `open`: authored by Anthropic / Claude via a +Cursor cloud agent on 2026-09-27, kernel-checked, not yet alignment-reviewed by +anyone else. A reviewer from OpenAI, Google, xAI or a human would earn +organizational-independence credit; another Anthropic model would not. diff --git a/formal/reviews/TEMPLATE.md b/formal/reviews/TEMPLATE.md new file mode 100644 index 000000000..02d0ced3a --- /dev/null +++ b/formal/reviews/TEMPLATE.md @@ -0,0 +1,27 @@ +# Formalization alignment review — + +**Date:** YYYY-MM-DD +**Reviewer:** , provider +**Organizational independence from the Lean author:** YES / NO (same provider earns zero credit) +**Source exposure:** <"statements only" | "read proofs and docstrings before forming a view" | ...> +**Registry commit:** `<40-hex main commit>` +**Gate run:** `python3 tools/formal_gate_check.py --run-lean` at that commit → `problems: []` / +**Layer 0 status of the object:** unchanged by this review + +## Lean files reviewed + +| Path | SHA-256 | +|---|---| +| `formal/UniversalLaw/...` | `<64-hex>` | + +## Verdicts + +| Claim id | Lean declaration | Verdict | Note | +|---|---|---|---| +| `` | `` | ALIGNED / ALIGNED AT NARROWER SCOPE / MISALIGNED | | + +## What this review does not establish + +The kernel checked the proofs; this review did not re-prove them. This review +did not assess the Layer 0 analytic argument, the parent theorem, or the +Python enclosure code. `STATUS.md` and `PROOF_INDEX.md` are unchanged. From 014c114fdfcdd7f324071770bf67f629dee7bbee Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Sun, 27 Sep 2026 21:51:43 +0000 Subject: [PATCH 3/3] CI: formal-verification lane (pinned elan + Lean v4.34.1, lake build, axiom audit, gate, controls) Runs on formal/**, the gate, its tests and itself. Installs elan from the v4.2.4 release script with a SHA-256 check, builds the dependency-free library, captures #print axioms, runs tools/formal_gate_check.py against that output, and runs the 38 controls in normal and -O modes. Evidence uploaded as an artifact. Green means kernel-checked registered declarations, not mathematical acceptance. Co-authored-by: Dylan Roy --- .github/workflows/formal-verification.yml | 70 +++++++++++++++++++++++ 1 file changed, 70 insertions(+) create mode 100644 .github/workflows/formal-verification.yml diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml new file mode 100644 index 000000000..0cd9cd7ed --- /dev/null +++ b/.github/workflows/formal-verification.yml @@ -0,0 +1,70 @@ +# Layer 1 formal lane. Builds the dependency-free Lean 4 library, audits axioms, +# and runs the fail-closed formalization gate. A green run establishes that the +# registered declarations are kernel-checked with allowed axioms only and that +# the registry, hashes and informal anchors are consistent. It is NOT +# mathematical acceptance of any Layer 0 claim; see formal/README.md. +name: formal-verification +on: + pull_request: + paths: + - 'formal/**' + - 'tools/formal_gate_check.py' + - 'tests/test_formal_gate.py' + - '.github/workflows/formal-verification.yml' + push: + branches: [main] + paths: + - 'formal/**' + - 'tools/formal_gate_check.py' + - 'tests/test_formal_gate.py' + - '.github/workflows/formal-verification.yml' + workflow_dispatch: +permissions: + contents: read +jobs: + kernel-check: + name: kernel-check + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 + with: + python-version: '3.11' + - name: Install elan (pinned release script, digest checked) and the pinned toolchain + run: | + set -euo pipefail + curl -sSfL https://raw.githubusercontent.com/leanprover/elan/v4.2.4/elan-init.sh -o /tmp/elan-init.sh + echo 'a620ff1641616222c8d37c54845492004bb84d6877cdbc944dd65c1aa685bf53 /tmp/elan-init.sh' | sha256sum -c - + sh /tmp/elan-init.sh -y --default-toolchain none + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + "$HOME/.elan/bin/elan" toolchain install "$(cat formal/lean-toolchain)" + - name: Record toolchain + run: | + mkdir -p formal-evidence + git rev-parse HEAD > formal-evidence/commit.txt + (cd formal && lean --version && lake --version) | tee formal-evidence/toolchain.txt + - name: Build the Lean library (kernel check) + run: cd formal && lake build 2>&1 | tee ../formal-evidence/lake-build.log + - name: Axiom audit + run: cd formal && lake env lean UniversalLaw/Audit.lean | tee ../formal-evidence/axioms.txt + - name: Fail-closed formalization gate + run: python -B -S tools/formal_gate_check.py --axioms-output formal-evidence/axioms.txt | tee formal-evidence/gate.json + - name: Gate controls, including Lean mutants, in both interpreter modes + run: | + python -B -S -m unittest tests.test_formal_gate -v 2>&1 | tee formal-evidence/tests-normal.log + python -B -O -S -m unittest tests.test_formal_gate -v 2>&1 | tee formal-evidence/tests-optimized.log + - name: Describe coverage + if: always() + run: | + echo 'Kernel-checked the registered Lean declarations, audited their axioms, and verified registry hashes and informal anchors. This is formalization status only: no Layer 0 review outcome, STATUS row, or theorem acceptance was established or changed.' >> "$GITHUB_STEP_SUMMARY" + - name: Preserve actual results including failures + if: always() + uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a + with: + name: formal-verification-${{ github.run_id }} + path: formal-evidence + if-no-files-found: error + retention-days: 30