Formalize closure, DSI, and contraction identities

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.

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
 

WCTLean/Models/ClosureFormalization.lean

@@ -0,0 +1,143 @@
+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`. -/
+noncomputable def dsiScaleRatio (m deltaLog n : ℝ) : ℝ :=
+  Real.exp (m * deltaLog / n)
+
+/-- DSI/WCT map: the winding reconstructed from a positive scale ratio. -/
+noncomputable 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]
+  exact div_self 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]
+    exact div_self hmd
+  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]
+
+/-- 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
+  have hmul := mul_le_mul_of_nonneg_right hfactor (norm_nonneg x)
+  simpa using hbound.trans hmul
+
+end WCTLean