From 0003ac651625124c81446b88fac3d63c62f33451 Mon Sep 17 00:00:00 2001 From: "Richard J. Reyes" Date: Thu, 20 Aug 2026 20:15:54 -0700 Subject: [PATCH 1/4] Add closure and DSI formalization batch --- WCTLean/Models/ClosureFormalization.lean | 141 +++++++++++++++++++++++ 1 file changed, 141 insertions(+) create mode 100644 WCTLean/Models/ClosureFormalization.lean diff --git a/WCTLean/Models/ClosureFormalization.lean b/WCTLean/Models/ClosureFormalization.lean new file mode 100644 index 0000000..528ec02 --- /dev/null +++ b/WCTLean/Models/ClosureFormalization.lean @@ -0,0 +1,141 @@ +import Mathlib +import WCTLean.Models.CompactDynamics + +namespace WCTLean + +/-! +Paper-level formalization targets from the August 2026 WCT closure and +compact-dynamics revisions. + +These theorems formalize exact algebraic pieces used by the papers. They do not +claim the full concentration-compactness theorem, nonlinear PDE well-posedness, +or physical validation. +-/ + +/-- DSI/WCT map: the scale ratio generated by harmonic index `m`, active +logarithmic interval `deltaLog`, and winding `n`. -/ +def dsiScaleRatio (m deltaLog n : ℝ) : ℝ := + Real.exp (m * deltaLog / n) + +/-- DSI/WCT map: the winding reconstructed from a positive scale ratio. -/ +def dsiWinding (m deltaLog lambda : ℝ) : ℝ := + m * deltaLog / Real.log lambda + +/-- The generated DSI scale ratio is always positive. -/ +theorem dsiScaleRatio_positive (m deltaLog n : ℝ) : + 0 < dsiScaleRatio m deltaLog n := by + unfold dsiScaleRatio + exact Real.exp_pos _ + +/-- Forward then inverse DSI/WCT mapping recovers the supplied nonzero winding, +provided the numerator and winding are nonzero. -/ +theorem dsiWinding_scaleRatio_roundtrip + (m deltaLog n : ℝ) + (hn : n ≠ 0) + (hmd : m * deltaLog ≠ 0) : + dsiWinding m deltaLog (dsiScaleRatio m deltaLog n) = n := by + unfold dsiWinding dsiScaleRatio + rw [Real.log_exp] + field_simp [hn, hmd] + +/-- Inverse then forward DSI/WCT mapping recovers a scale ratio greater than +one when the harmonic/interval numerator is nonzero. -/ +theorem dsiScaleRatio_winding_roundtrip + (m deltaLog lambda : ℝ) + (hmd : m * deltaLog ≠ 0) + (hlambda : 1 < lambda) : + dsiScaleRatio m deltaLog (dsiWinding m deltaLog lambda) = lambda := by + have hlambda_pos : 0 < lambda := lt_trans zero_lt_one hlambda + have hlog_pos : 0 < Real.log lambda := Real.log_pos hlambda + have hlog_ne : Real.log lambda ≠ 0 := ne_of_gt hlog_pos + have hinner : + m * deltaLog / (m * deltaLog / Real.log lambda) = Real.log lambda := by + field_simp [hmd, hlog_ne] + unfold dsiScaleRatio dsiWinding + rw [hinner, Real.exp_log hlambda_pos] + +/-- The WCT winding relation and the standard DSI harmonic frequency relation +are algebraically identical once `n = m*deltaLog/log(lambda)` is imposed. -/ +theorem dsi_wct_log_frequency_match + (m deltaLog lambda n : ℝ) + (hdelta : deltaLog ≠ 0) + (hlog : Real.log lambda ≠ 0) + (hn : n = m * deltaLog / Real.log lambda) : + 2 * Real.pi * n / deltaLog = 2 * Real.pi * m / Real.log lambda := by + rw [hn] + field_simp [hdelta, hlog] + <;> ring + +/-- Exact square completion behind the scalar quadratic-to-quartic absorption +used in the fixed-mass coercivity estimate. -/ +theorem quartic_absorption_identity + (eta r : ℝ) (heta : eta ≠ 0) : + eta * r ^ 4 - r ^ 2 + 1 / (4 * eta) = + (2 * eta * r ^ 2 - 1) ^ 2 / (4 * eta) := by + field_simp [heta] + <;> ring + +/-- For positive `eta`, the quartic completion remainder is nonnegative. This +is the scalar core of `r^2 <= eta*r^4 + 1/(4*eta)`. -/ +theorem quartic_absorption_remainder_nonnegative + (eta r : ℝ) (heta : 0 < eta) : + 0 ≤ eta * r ^ 4 - r ^ 2 + 1 / (4 * eta) := by + rw [quartic_absorption_identity eta r (ne_of_gt heta)] + have hden : 0 ≤ 4 * eta := le_of_lt (mul_pos (by norm_num) heta) + exact div_nonneg (sq_nonneg _) hden + +/-- A strict local contraction estimate propagates through the convex averaged +update with contraction factor `1 - mix*delta`. -/ +theorem averagedUpdate_contraction_norm_le + {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + (mix delta : ℝ) (average : E → E) (x : E) + (h0 : 0 ≤ mix) (h1 : mix ≤ 1) + (havg : ‖average x‖ ≤ (1 - delta) * ‖x‖) : + ‖averagedUpdate mix average x‖ ≤ (1 - mix * delta) * ‖x‖ := by + unfold averagedUpdate + calc + ‖(1 - mix) • x + mix • average x‖ + ≤ ‖(1 - mix) • x‖ + ‖mix • average x‖ := norm_add_le _ _ + _ = |1 - mix| * ‖x‖ + |mix| * ‖average x‖ := by + rw [norm_smul, norm_smul, Real.norm_eq_abs, Real.norm_eq_abs] + _ ≤ (1 - mix) * ‖x‖ + mix * ((1 - delta) * ‖x‖) := by + rw [abs_of_nonneg h0, abs_of_nonneg (sub_nonneg.mpr h1)] + exact add_le_add_left (mul_le_mul_of_nonneg_left havg h0) _ + _ = (1 - mix * delta) * ‖x‖ := by ring + +/-- Adding a perturbation bounded by `epsilon*||x||` changes the contraction +factor by at most `+epsilon`. -/ +theorem averagedUpdate_perturbation_factor + {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + (mix delta epsilon : ℝ) (average : E → E) (x perturbation : E) + (h0 : 0 ≤ mix) (h1 : mix ≤ 1) + (havg : ‖average x‖ ≤ (1 - delta) * ‖x‖) + (hpert : ‖perturbation‖ ≤ epsilon * ‖x‖) : + ‖averagedUpdate mix average x + perturbation‖ ≤ + (1 - mix * delta + epsilon) * ‖x‖ := by + have hbase := averagedUpdate_contraction_norm_le + mix delta average x h0 h1 havg + calc + ‖averagedUpdate mix average x + perturbation‖ + ≤ ‖averagedUpdate mix average x‖ + ‖perturbation‖ := norm_add_le _ _ + _ ≤ (1 - mix * delta) * ‖x‖ + epsilon * ‖x‖ := + add_le_add hbase hpert + _ = (1 - mix * delta + epsilon) * ‖x‖ := by ring + +/-- If `epsilon <= mix*delta`, the perturbed averaged update is still +norm-nonexpansive. -/ +theorem averagedUpdate_perturbation_nonexpansive + {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + (mix delta epsilon : ℝ) (average : E → E) (x perturbation : E) + (h0 : 0 ≤ mix) (h1 : mix ≤ 1) + (havg : ‖average x‖ ≤ (1 - delta) * ‖x‖) + (hpert : ‖perturbation‖ ≤ epsilon * ‖x‖) + (hmargin : epsilon ≤ mix * delta) : + ‖averagedUpdate mix average x + perturbation‖ ≤ ‖x‖ := by + have hbound := averagedUpdate_perturbation_factor + mix delta epsilon average x perturbation h0 h1 havg hpert + have hfactor : 1 - mix * delta + epsilon ≤ 1 := by + linarith + exact hbound.trans (mul_le_mul_of_nonneg_right hfactor (norm_nonneg x)) + +end WCTLean From 3c0fa63f7bf6f49a93fa5e84f41bdc86c243b83a Mon Sep 17 00:00:00 2001 From: "Richard J. Reyes" Date: Thu, 20 Aug 2026 20:16:03 -0700 Subject: [PATCH 2/4] Import closure formalization module --- WCTLean/Main.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/WCTLean/Main.lean b/WCTLean/Main.lean index 6ace72a..231c32c 100644 --- a/WCTLean/Main.lean +++ b/WCTLean/Main.lean @@ -27,6 +27,7 @@ import WCTLean.Models.Collider import WCTLean.Models.KoideDerivation import WCTLean.Models.UnifiedOperator import WCTLean.Models.CompactDynamics +import WCTLean.Models.ClosureFormalization import WCTLean.ResolvedAudit import WCTLean.DerivedAudit From 62e2805c0525e0810c1b3c210a2417d5bd64d324 Mon Sep 17 00:00:00 2001 From: "Richard J. Reyes" Date: Thu, 20 Aug 2026 20:16:37 -0700 Subject: [PATCH 3/4] Document closure formalization scope --- CLOSURE_FORMALIZATION_BATCH.md | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 CLOSURE_FORMALIZATION_BATCH.md diff --git a/CLOSURE_FORMALIZATION_BATCH.md b/CLOSURE_FORMALIZATION_BATCH.md new file mode 100644 index 0000000..033b303 --- /dev/null +++ b/CLOSURE_FORMALIZATION_BATCH.md @@ -0,0 +1,25 @@ +# WCT closure formalization batch + +This batch adds kernel targets drawn from the August 2026 closure, compact-dynamics, and WCT-DSI revisions. + +## Added theorem targets + +`WCTLean/Models/ClosureFormalization.lean` adds: + +- `dsiScaleRatio_positive` +- `dsiWinding_scaleRatio_roundtrip` +- `dsiScaleRatio_winding_roundtrip` +- `dsi_wct_log_frequency_match` +- `quartic_absorption_identity` +- `quartic_absorption_remainder_nonnegative` +- `averagedUpdate_contraction_norm_le` +- `averagedUpdate_perturbation_factor` +- `averagedUpdate_perturbation_nonexpansive` + +The DSI statements formalize the exact positive-log-coordinate map between scale ratio and winding. The coercivity statements formalize the square completion behind the quadratic-to-quartic absorption estimate. The compact-dynamics statements formalize the contraction factor `1-L*delta`, its perturbation correction, and the sufficient margin `epsilon <= L*delta` for norm nonexpansion. + +## Boundary + +This batch does **not** formalize Lions concentration-compactness, prove the full free-space minimizer theorem, prove the full complex quotient first variation, establish nonlinear PDE well-posedness, or provide physical/empirical validation. + +These are paper-level theorem additions. They do not automatically change the canonical `80 / 142` equation-specific coverage count unless a theorem is separately mapped to a canonical registry object with matching scope. From d8a847dd860fd69a37e976f0a1f7be354d66aa74 Mon Sep 17 00:00:00 2001 From: "Richard J. Reyes" Date: Thu, 20 Aug 2026 20:20:16 -0700 Subject: [PATCH 4/4] Fix Lean closure formalization build --- WCTLean/Models/ClosureFormalization.lean | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/WCTLean/Models/ClosureFormalization.lean b/WCTLean/Models/ClosureFormalization.lean index 528ec02..a3bf534 100644 --- a/WCTLean/Models/ClosureFormalization.lean +++ b/WCTLean/Models/ClosureFormalization.lean @@ -14,11 +14,11 @@ or physical validation. /-- DSI/WCT map: the scale ratio generated by harmonic index `m`, active logarithmic interval `deltaLog`, and winding `n`. -/ -def dsiScaleRatio (m deltaLog n : ℝ) : ℝ := +noncomputable def dsiScaleRatio (m deltaLog n : ℝ) : ℝ := Real.exp (m * deltaLog / n) /-- DSI/WCT map: the winding reconstructed from a positive scale ratio. -/ -def dsiWinding (m deltaLog lambda : ℝ) : ℝ := +noncomputable def dsiWinding (m deltaLog lambda : ℝ) : ℝ := m * deltaLog / Real.log lambda /-- The generated DSI scale ratio is always positive. -/ @@ -37,6 +37,7 @@ theorem dsiWinding_scaleRatio_roundtrip unfold dsiWinding dsiScaleRatio rw [Real.log_exp] field_simp [hn, hmd] + exact div_self hmd /-- Inverse then forward DSI/WCT mapping recovers a scale ratio greater than one when the harmonic/interval numerator is nonzero. -/ @@ -51,6 +52,7 @@ theorem dsiScaleRatio_winding_roundtrip have hinner : m * deltaLog / (m * deltaLog / Real.log lambda) = Real.log lambda := by field_simp [hmd, hlog_ne] + exact div_self hmd unfold dsiScaleRatio dsiWinding rw [hinner, Real.exp_log hlambda_pos] @@ -64,7 +66,6 @@ theorem dsi_wct_log_frequency_match 2 * Real.pi * n / deltaLog = 2 * Real.pi * m / Real.log lambda := by rw [hn] field_simp [hdelta, hlog] - <;> ring /-- Exact square completion behind the scalar quadratic-to-quartic absorption used in the fixed-mass coercivity estimate. -/ @@ -73,7 +74,7 @@ theorem quartic_absorption_identity eta * r ^ 4 - r ^ 2 + 1 / (4 * eta) = (2 * eta * r ^ 2 - 1) ^ 2 / (4 * eta) := by field_simp [heta] - <;> ring + ring /-- For positive `eta`, the quartic completion remainder is nonnegative. This is the scalar core of `r^2 <= eta*r^4 + 1/(4*eta)`. -/ @@ -136,6 +137,7 @@ theorem averagedUpdate_perturbation_nonexpansive mix delta epsilon average x perturbation h0 h1 havg hpert have hfactor : 1 - mix * delta + epsilon ≤ 1 := by linarith - exact hbound.trans (mul_le_mul_of_nonneg_right hfactor (norm_nonneg x)) + have hmul := mul_le_mul_of_nonneg_right hfactor (norm_nonneg x) + simpa using hbound.trans hmul end WCTLean