IndisputableMonolith.Gravity.Track1BCorrectedQuadratic
IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean · 440 lines · 17 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.D2DampedScheduleClosure
2import IndisputableMonolith.Gravity.FreudenthalAxisStencilCoeffCert
3
4/-!
5# Track 1.B Corrected Quadratic: the Axis-Stencil Local Correspondence
6
7## Status: THEOREM (0 sorry, 0 RS-internal axiom) for everything stated;
8## the corrected gate itself is named OPEN, not asserted.
9
10## Why this module exists (Session 202)
11
12The Track 1.B route to the local Regge/J-cost correspondence factors through
13the mixed hinge-deficit quadratic. The Session 202 exact finite audit showed
14the old identification was wrong-weighted: at the `N = 5` single-vertex bump
15the mixed quadratic evaluates to `12`, while the seven-class square-root edge
16stencil evaluates to `6 + 6√2 + 2√3`, and
17`canonicalPeriodicMixedLengthSingleVertexAudit_scalar_mismatch` proves those
18scalars differ. The corrected mixed identification
19(`CanonicalPeriodicMixedHingeDeficitAxisStencilTarget`: mixed quadratic =
20rational axis stencil) already exists. What did not exist was the corrected
21**endpoint**: the local correspondence with the axis stencil as quadratic,
22its algebra, and the theorem explaining why the correction is forced rather
23than aesthetic. This module supplies all three.
24
25## What is proved here
26
271. `ReggeLocalQuadraticCorrespondence K hK Q`: the local cubic-Taylor
28 correspondence with an arbitrary candidate quadratic `Q`, generalizing
29 the legacy seven-class definition (which is the instance
30 `Q = periodicEdgeStencilDirichletAction P`, proved as an `Iff`).
312. `CanonicalPeriodicAxisStencilLocalCorrespondence`: the corrected endpoint,
32 the instance at `Q = canonicalPeriodicMixedAxisStencilAction`.
333. Quadratic algebra for the axis stencil (nonnegativity, exact
34 `a²`-homogeneity) and transferred homogeneity for the legacy stencil.
354. **Rigidity** (`reggeLocalQuadraticCorrespondence_quadratic_unique`): two
36 homogeneous quadratics satisfying the correspondence on the same complex
37 are pointwise equal. Corollary: the legacy and corrected endpoints are
38 jointly satisfiable only if the two stencils coincide identically
39 (`not_both_correspondences_of_quadratics_differ`). Given the Session 202
40 mismatch witness, at most one of them can be the true Taylor coefficient;
41 the audit selects the axis stencil.
425. **D2 hook** (`normalized_regge_sub_half_quadratic_abs_le` and its axis
43 instance): the per-tetrahedron normalized residual bound used by the
44 damped-schedule closure, proved parametrically in `Q`, so the entire
45 damped D2 pipeline transfers to the corrected quadratic the day the
46 corrected gate closes, with quadrature limit action `½ · axis stencil`.
476. The corrected `N = 5` gate, stated exactly: stationarity at `N = 5` is
48 already a theorem, so the corrected closure at the certificate scale
49 reduces to one finite coefficient identity, the explicit-fiber axis
50 target (`CanonicalPeriodicCorrectedTrack1BGateAtN5`).
51
52## What remains open
53
54The `N = 5` gate itself is now CLOSED (2026-06-17): see
55`correctedTrack1BGateAtN5_closed`, discharged by the finite coefficient
56certificate in `FreudenthalAxisStencilCoeffCert` (with the `native_decide`
57axiom caveat noted there). What remains open is only the all-cardinality
58generalization (a single explicit-fiber coefficient identity for arbitrary
59`N`, not just `N = 5`). Everything else in this module is unconditional.
60-/
61
62namespace IndisputableMonolith
63namespace Gravity
64namespace Track1BCorrectedQuadratic
65
66open PhysicalSixTetCubicDirichletInstance
67open D2DampedScheduleClosure
68open Geometry.ReggeTriangulation3D
69open Geometry.ReggeHessian3D
70open Geometry.Triangulation3DConsistency
71open Geometry.ReggeActionConcrete
72open Geometry.PeriodicFreudenthalTorus
73
74noncomputable section
75
76/-! ## §1. The parametric local quadratic correspondence -/
77
78/-- Local cubic-Taylor correspondence for an arbitrary candidate quadratic
79`Q`: near the flat configuration, the full nonlinear Regge action equals its
80flat value plus one half of `Q`, up to a controlled cubic remainder. The
81legacy Track 1.B target is the instance `Q = periodicEdgeStencilDirichletAction`;
82the Session-202-corrected target is the instance
83`Q = canonicalPeriodicMixedAxisStencilAction`. -/
84def ReggeLocalQuadraticCorrespondence
85 (K : Triangulation3D) (hK : IncidenceConsistent K)
86 (Q : VertexPotential K → ℝ) : Prop :=
87 ∃ (r C : ℝ), 0 < r ∧ 0 ≤ C ∧
88 ∀ ξ : VertexPotential K, ‖ξ‖ < r →
89 ‖reggeAction K hK ξ -
90 reggeAction K hK (zeroPotential K) -
91 (1 / 2) * Q ξ‖ ≤
92 C * ‖ξ‖ ^ (3 : ℕ)
93
94/-- The legacy seven-class endpoint is the parametric correspondence at the
95edge-stencil quadratic. -/
96theorem edgeStencilLocalCorrespondence_iff
97 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
98 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz) :
99 CanonicalPeriodicEdgeStencilLocalCorrespondence Nx Ny Nz hx hy hz ↔
100 ReggeLocalQuadraticCorrespondence
101 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K
102 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).hK
103 (periodicEdgeStencilDirichletAction
104 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz)) :=
105 Iff.rfl
106
107/-- **The corrected Track 1.B endpoint.** The local correspondence with the
108Session-202-corrected quadratic: the rational axis stencil, which the exact
109finite audit identifies as the value of the mixed hinge-deficit quadratic. -/
110def CanonicalPeriodicAxisStencilLocalCorrespondence
111 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
112 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz) : Prop :=
113 ReggeLocalQuadraticCorrespondence
114 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K
115 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).hK
116 (canonicalPeriodicMixedAxisStencilAction Nx Ny Nz hx hy hz)
117
118/-! ## §2. Quadratic algebra of the two stencils -/
119
120/-- The axis stencil is nonnegative. -/
121theorem canonicalPeriodicMixedAxisStencilAction_nonneg
122 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
123 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
124 (ξ : VertexPotential
125 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K) :
126 0 ≤ canonicalPeriodicMixedAxisStencilAction Nx Ny Nz hx hy hz ξ := by
127 unfold canonicalPeriodicMixedAxisStencilAction
128 refine Finset.sum_nonneg fun base _ => Finset.sum_nonneg fun d _ => ?_
129 dsimp only
130 positivity
131
132/-- The axis stencil is exactly quadratically homogeneous. -/
133theorem canonicalPeriodicMixedAxisStencilAction_smul
134 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
135 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
136 (a : ℝ)
137 (ξ : VertexPotential
138 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K) :
139 canonicalPeriodicMixedAxisStencilAction Nx Ny Nz hx hy hz (a • ξ) =
140 a ^ (2 : ℕ) * canonicalPeriodicMixedAxisStencilAction Nx Ny Nz hx hy hz ξ := by
141 unfold canonicalPeriodicMixedAxisStencilAction
142 rw [Finset.mul_sum]
143 refine Finset.sum_congr rfl fun base _ => ?_
144 rw [Finset.mul_sum]
145 refine Finset.sum_congr rfl fun d _ => ?_
146 dsimp only
147 simp only [Pi.smul_apply, smul_eq_mul]
148 ring
149
150/-- Quadratic homogeneity transfers to the legacy edge stencil through the
151proved identification with the canonical Dirichlet energy. -/
152theorem periodicEdgeStencilDirichletAction_smul
153 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
154 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
155 (a : ℝ)
156 (ξ : VertexPotential
157 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K) :
158 periodicEdgeStencilDirichletAction
159 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz) (a • ξ) =
160 a ^ (2 : ℕ) *
161 periodicEdgeStencilDirichletAction
162 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz) ξ := by
163 rw [← canonicalPeriodicEdgeStencilTarget Nx Ny Nz hx hy hz (a • ξ),
164 ← canonicalPeriodicEdgeStencilTarget Nx Ny Nz hx hy hz ξ]
165 exact canonicalDirichletEnergy_smul
166 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K
167 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).hK a ξ
168
169/-! ## §3. Rigidity: the Taylor coefficient is unique -/
170
171/-- **RIGIDITY.** If two quadratically homogeneous candidates both satisfy
172the local correspondence on the same complex, they are pointwise equal. The
173quadratic coefficient of a cubic-Taylor expansion is unique, so at most one
174stencil can be the true second-order content of the Regge action. -/
175theorem reggeLocalQuadraticCorrespondence_quadratic_unique
176 (K : Triangulation3D) (hK : IncidenceConsistent K)
177 (Q₁ Q₂ : VertexPotential K → ℝ)
178 (hQ₁ : ∀ (a : ℝ) (ξ : VertexPotential K), Q₁ (a • ξ) = a ^ (2 : ℕ) * Q₁ ξ)
179 (hQ₂ : ∀ (a : ℝ) (ξ : VertexPotential K), Q₂ (a • ξ) = a ^ (2 : ℕ) * Q₂ ξ)
180 (h₁ : ReggeLocalQuadraticCorrespondence K hK Q₁)
181 (h₂ : ReggeLocalQuadraticCorrespondence K hK Q₂) :
182 ∀ ξ : VertexPotential K, Q₁ ξ = Q₂ ξ := by
183 obtain ⟨r₁, C₁, hr₁, hC₁, hb₁⟩ := h₁
184 obtain ⟨r₂, C₂, hr₂, hC₂, hb₂⟩ := h₂
185 intro ξ
186 by_contra hne
187 have hΔpos : 0 < |Q₁ ξ - Q₂ ξ| := abs_pos.mpr (sub_ne_zero.mpr hne)
188 set Δ : ℝ := |Q₁ ξ - Q₂ ξ| with hΔdef
189 -- Choose the probe scale `t`.
190 have hA : (0 : ℝ) < 1 + ‖ξ‖ := by positivity
191 have hB : (0 : ℝ) < 1 + 2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ) := by positivity
192 set t : ℝ :=
193 min (min r₁ r₂ / (1 + ‖ξ‖)) (Δ / (1 + 2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ)))
194 with ht_def
195 have ht_pos : 0 < t := by
196 refine lt_min (div_pos (lt_min hr₁ hr₂) hA) (div_pos hΔpos hB)
197 -- The scaled probe sits inside both radii.
198 have ht_norm : ‖t • ξ‖ = t * ‖ξ‖ := by
199 rw [norm_smul, Real.norm_eq_abs, abs_of_pos ht_pos]
200 have hsmall : t * ‖ξ‖ < min r₁ r₂ := by
201 have h1 : t ≤ min r₁ r₂ / (1 + ‖ξ‖) := min_le_left _ _
202 have h2 : ‖ξ‖ < 1 + ‖ξ‖ := by linarith [norm_nonneg ξ]
203 have hq_pos : 0 < min r₁ r₂ / (1 + ‖ξ‖) := div_pos (lt_min hr₁ hr₂) hA
204 calc t * ‖ξ‖ ≤ (min r₁ r₂ / (1 + ‖ξ‖)) * ‖ξ‖ :=
205 mul_le_mul_of_nonneg_right h1 (norm_nonneg ξ)
206 _ < (min r₁ r₂ / (1 + ‖ξ‖)) * (1 + ‖ξ‖) :=
207 mul_lt_mul_of_pos_left h2 hq_pos
208 _ = min r₁ r₂ := div_mul_cancel₀ _ hA.ne'
209 have hsmall₁ : ‖t • ξ‖ < r₁ := by
210 rw [ht_norm]; exact lt_of_lt_of_le hsmall (min_le_left _ _)
211 have hsmall₂ : ‖t • ξ‖ < r₂ := by
212 rw [ht_norm]; exact lt_of_lt_of_le hsmall (min_le_right _ _)
213 -- The two cubic bounds at the scaled probe.
214 have hb₁' := hb₁ (t • ξ) hsmall₁
215 have hb₂' := hb₂ (t • ξ) hsmall₂
216 rw [hQ₁ t ξ, Real.norm_eq_abs, ht_norm] at hb₁'
217 rw [hQ₂ t ξ, Real.norm_eq_abs, ht_norm] at hb₂'
218 -- Triangle inequality forces the quadratic gap below a linear-in-`t` bound.
219 have hdiff :
220 (reggeAction K hK (t • ξ) - reggeAction K hK (zeroPotential K) -
221 (1 / 2) * (t ^ (2 : ℕ) * Q₂ ξ)) -
222 (reggeAction K hK (t • ξ) - reggeAction K hK (zeroPotential K) -
223 (1 / 2) * (t ^ (2 : ℕ) * Q₁ ξ)) =
224 (1 / 2) * t ^ (2 : ℕ) * (Q₁ ξ - Q₂ ξ) := by ring
225 have hgap : (1 / 2) * t ^ (2 : ℕ) * Δ ≤ (C₁ + C₂) * (t * ‖ξ‖) ^ (3 : ℕ) := by
226 have htri :
227 |(1 / 2) * t ^ (2 : ℕ) * (Q₁ ξ - Q₂ ξ)| ≤
228 C₂ * (t * ‖ξ‖) ^ (3 : ℕ) + C₁ * (t * ‖ξ‖) ^ (3 : ℕ) := by
229 rw [← hdiff]
230 exact le_trans (abs_sub _ _) (add_le_add hb₂' hb₁')
231 have habs :
232 |(1 / 2) * t ^ (2 : ℕ) * (Q₁ ξ - Q₂ ξ)| =
233 (1 / 2) * t ^ (2 : ℕ) * Δ := by
234 rw [abs_mul, abs_of_nonneg (by positivity : (0:ℝ) ≤ (1/2) * t ^ (2:ℕ))]
235 rw [habs] at htri
236 linarith
237 -- Divide by `t²` and contradict the choice of `t`.
238 have ht2_pos : (0 : ℝ) < t ^ (2 : ℕ) := by positivity
239 have hΔle : Δ ≤ 2 * (C₁ + C₂) * t * ‖ξ‖ ^ (3 : ℕ) := by
240 have hexp : (t * ‖ξ‖) ^ (3 : ℕ) = t ^ (2 : ℕ) * (t * ‖ξ‖ ^ (3 : ℕ)) := by
241 ring
242 rw [hexp] at hgap
243 calc Δ = (1 / 2) * t ^ (2 : ℕ) * Δ * (2 / t ^ (2 : ℕ)) := by
244 field_simp
245 _ ≤ (C₁ + C₂) * (t ^ (2 : ℕ) * (t * ‖ξ‖ ^ (3 : ℕ))) * (2 / t ^ (2 : ℕ)) :=
246 mul_le_mul_of_nonneg_right hgap (by positivity)
247 _ = 2 * (C₁ + C₂) * t * ‖ξ‖ ^ (3 : ℕ) := by
248 field_simp
249 have ht_le : t ≤ Δ / (1 + 2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ)) := min_le_right _ _
250 have hfinal : Δ < Δ := by
251 have hC12 : 0 ≤ C₁ + C₂ := by linarith
252 have hfrac :
253 2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ) <
254 1 + 2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ) := by linarith
255 calc Δ ≤ 2 * (C₁ + C₂) * t * ‖ξ‖ ^ (3 : ℕ) := hΔle
256 _ = t * (2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ)) := by ring
257 _ ≤ (Δ / (1 + 2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ))) *
258 (2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ)) := by
259 refine mul_le_mul_of_nonneg_right ht_le ?_
260 positivity
261 _ < (Δ / (1 + 2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ))) *
262 (1 + 2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ)) := by
263 refine mul_lt_mul_of_pos_left hfrac ?_
264 exact div_pos hΔpos hB
265 _ = Δ := div_mul_cancel₀ _ hB.ne'
266 exact absurd hfinal (lt_irrefl Δ)
267
268/-- The legacy and corrected endpoints can both hold only if the two stencils
269are pointwise equal. -/
270theorem both_correspondences_force_equal_quadratics
271 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
272 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
273 (hLegacy : CanonicalPeriodicEdgeStencilLocalCorrespondence Nx Ny Nz hx hy hz)
274 (hCorrected : CanonicalPeriodicAxisStencilLocalCorrespondence Nx Ny Nz hx hy hz) :
275 ∀ ξ : VertexPotential
276 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K,
277 periodicEdgeStencilDirichletAction
278 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz) ξ =
279 canonicalPeriodicMixedAxisStencilAction Nx Ny Nz hx hy hz ξ :=
280 reggeLocalQuadraticCorrespondence_quadratic_unique
281 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K
282 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).hK
283 _ _
284 (periodicEdgeStencilDirichletAction_smul Nx Ny Nz hx hy hz)
285 (canonicalPeriodicMixedAxisStencilAction_smul Nx Ny Nz hx hy hz)
286 ((edgeStencilLocalCorrespondence_iff Nx Ny Nz hx hy hz).mp hLegacy)
287 hCorrected
288
289/-- The two stencils differ somewhere (the content of the Session 202 audit
290witness, stated as a named proposition). -/
291def AxisEdgeStencilQuadraticsDiffer
292 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
293 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz) : Prop :=
294 ∃ ξ : VertexPotential
295 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K,
296 periodicEdgeStencilDirichletAction
297 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz) ξ ≠
298 canonicalPeriodicMixedAxisStencilAction Nx Ny Nz hx hy hz ξ
299
300/-- **EXCLUSIVITY.** Given the audit witness, the legacy seven-class endpoint
301and the corrected axis endpoint are mutually exclusive: at most one of them is
302the true cubic-Taylor statement for the Regge action. -/
303theorem not_both_correspondences_of_quadratics_differ
304 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
305 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
306 (hdiff : AxisEdgeStencilQuadraticsDiffer Nx Ny Nz hx hy hz) :
307 ¬(CanonicalPeriodicEdgeStencilLocalCorrespondence Nx Ny Nz hx hy hz ∧
308 CanonicalPeriodicAxisStencilLocalCorrespondence Nx Ny Nz hx hy hz) := by
309 rintro ⟨hLegacy, hCorrected⟩
310 obtain ⟨ξ, hξ⟩ := hdiff
311 exact hξ (both_correspondences_force_equal_quadratics
312 Nx Ny Nz hx hy hz hLegacy hCorrected ξ)
313
314/-! ## §4. The D2 hook: the per-tetrahedron bound, parametric in the
315quadratic -/
316
317/-- The normalized per-tetrahedron residual bound, proved for an arbitrary
318homogeneous quadratic satisfying the cubic bound. This is the exact bound
319the damped-schedule D2 closure consumes, so the whole damped pipeline
320transfers to the corrected quadratic the day the corrected gate closes. -/
321theorem normalized_regge_sub_half_quadratic_abs_le
322 (K : Triangulation3D) (hK : IncidenceConsistent K)
323 (Q : VertexPotential K → ℝ)
324 (hQ : ∀ (a : ℝ) (ξ : VertexPotential K), Q (a • ξ) = a ^ (2 : ℕ) * Q ξ)
325 (h0 : reggeAction K hK (zeroPotential K) = 0)
326 (r C : ℝ)
327 (hb : ∀ ξ : VertexPotential K, ‖ξ‖ < r →
328 ‖reggeAction K hK ξ - reggeAction K hK (zeroPotential K) -
329 (1 / 2) * Q ξ‖ ≤ C * ‖ξ‖ ^ (3 : ℕ))
330 (s : ℝ) (hs : s ≠ 0)
331 (ξ : VertexPotential K) (hsmall : ‖s • ξ‖ < r) :
332 |reggeAction K hK (s • ξ) / s ^ (2 : ℕ) - (1 / 2) * Q ξ| ≤
333 C * |s| * ‖ξ‖ ^ (3 : ℕ) := by
334 have hb' := hb (s • ξ) hsmall
335 rw [h0, sub_zero, hQ s ξ, Real.norm_eq_abs] at hb'
336 have hs2 : (0 : ℝ) < s ^ (2 : ℕ) := by positivity
337 have key :
338 reggeAction K hK (s • ξ) / s ^ (2 : ℕ) - (1 / 2) * Q ξ =
339 (reggeAction K hK (s • ξ) - (1 / 2) * (s ^ (2 : ℕ) * Q ξ)) / s ^ (2 : ℕ) := by
340 field_simp
341 rw [key, abs_div, abs_of_pos hs2]
342 have hnorm3 : ‖s • ξ‖ ^ (3 : ℕ) = |s| ^ (3 : ℕ) * ‖ξ‖ ^ (3 : ℕ) := by
343 rw [norm_smul, Real.norm_eq_abs, mul_pow]
344 have habs3 : |s| ^ (3 : ℕ) = |s| * s ^ (2 : ℕ) := by
345 rw [pow_succ, sq_abs, mul_comm]
346 have hdivle :
347 |reggeAction K hK (s • ξ) - (1 / 2) * (s ^ (2 : ℕ) * Q ξ)| / s ^ (2 : ℕ) ≤
348 (C * ‖s • ξ‖ ^ (3 : ℕ)) / s ^ (2 : ℕ) := by
349 gcongr
350 refine le_trans hdivle (le_of_eq ?_)
351 rw [hnorm3, habs3]
352 field_simp
353
354/-- The corrected endpoint feeds the damped D2 pipeline: under the axis
355correspondence, the normalized nonlinear Regge action converges to one half
356of the axis stencil with the same constructive damping bound used by the
357damped-schedule closure. -/
358theorem axis_normalized_regge_bound_of_correspondence
359 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
360 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
361 (hCorr : CanonicalPeriodicAxisStencilLocalCorrespondence Nx Ny Nz hx hy hz) :
362 ∃ (r C : ℝ), 0 < r ∧ 0 ≤ C ∧
363 ∀ (s : ℝ), s ≠ 0 →
364 ∀ ξ : VertexPotential
365 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K,
366 ‖s • ξ‖ < r →
367 |reggeAction
368 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K
369 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).hK
370 (s • ξ) / s ^ (2 : ℕ) -
371 (1 / 2) *
372 canonicalPeriodicMixedAxisStencilAction Nx Ny Nz hx hy hz ξ| ≤
373 C * |s| * ‖ξ‖ ^ (3 : ℕ) := by
374 obtain ⟨r, C, hr, hC, hb⟩ := hCorr
375 refine ⟨r, C, hr, hC, fun s hs ξ hsmall => ?_⟩
376 exact normalized_regge_sub_half_quadratic_abs_le
377 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K
378 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).hK
379 (canonicalPeriodicMixedAxisStencilAction Nx Ny Nz hx hy hz)
380 (canonicalPeriodicMixedAxisStencilAction_smul Nx Ny Nz hx hy hz)
381 (canonicalPeriodicReggeAction_zeroPotential_eq_zero_of_flatConfiguration
382 Nx Ny Nz hx hy hz
383 (canonicalPeriodicFlatConfiguration Nx Ny Nz hx hy hz))
384 r C hb s hs ξ hsmall
385
386/-! ## §5. The corrected gate at the certificate scale -/
387
388/-- **The corrected Track 1.B gate at `N = 5`, stated exactly.** Second-order
389Schl\"afli stationarity at `N = 5` is already a theorem, so the corrected
390closure at the certificate scale reduces to this single finite coefficient
391identity: the explicit-fiber axis-stencil target. -/
392abbrev CanonicalPeriodicCorrectedTrack1BGateAtN5 : Prop :=
393 CanonicalPeriodicMixedHingeDeficitExplicitFiberAxisStencilTargetAtN5
394
395/-- **The corrected `N = 5` gate is closed** (2026-06-17). It is discharged by
396`FreudenthalAxisStencilCoeffCert.canonicalPeriodicMixedHingeDeficitExplicitFiberAxisStencilTargetAtN5`,
397which proves the explicit-fiber axis-stencil coefficient identity via a finite
398`native_decide` certificate over the 125 = 5³ vertex table. Honest caveat: that
399certificate's axiom basis includes `Lean.ofReduceBool` and `Lean.trustCompiler`
400(compiler trust) on top of `propext / Classical.choice / Quot.sound`. -/
401theorem correctedTrack1BGateAtN5_closed : CanonicalPeriodicCorrectedTrack1BGateAtN5 :=
402 FreudenthalAxisStencilCoeffCert.canonicalPeriodicMixedHingeDeficitExplicitFiberAxisStencilTargetAtN5
403
404/-- The gate discharges the corrected mixed identification at `N = 5`. -/
405theorem correctedMixedTargetAtN5_of_gate
406 (hGate : CanonicalPeriodicCorrectedTrack1BGateAtN5) :
407 CanonicalPeriodicMixedHingeDeficitAxisStencilTargetAtN5 :=
408 canonicalPeriodicMixedHingeDeficitAxisStencilTargetAtN5_of_explicitFiberAxis hGate
409
410/-! ## §6. Status record -/
411
412/-- Corrected Track 1.B scope after this module. -/
413structure CorrectedTrack1BStatus where
414 corrected_endpoint_formulated : Bool
415 axis_stencil_algebra_proved : Bool
416 rigidity_proved : Bool
417 exclusivity_with_legacy_proved : Bool
418 d2_hook_proved : Bool
419 stationarity_at_N5_proved : Bool
420 gate_open : Bool
421
422/-- The current corrected-quadratic scope: everything formulated and the
423supporting theorems proved. The `N = 5` explicit-fiber coefficient gate is now
424closed (`gate_open := false`, see `correctedTrack1BGateAtN5_closed`); only the
425all-cardinality generalization remains. -/
426def correctedTrack1BStatus : CorrectedTrack1BStatus where
427 corrected_endpoint_formulated := true
428 axis_stencil_algebra_proved := true
429 rigidity_proved := true
430 exclusivity_with_legacy_proved := true
431 d2_hook_proved := true
432 stationarity_at_N5_proved := true
433 gate_open := false
434
435end
436
437end Track1BCorrectedQuadratic
438end Gravity
439end IndisputableMonolith
440