IndisputableMonolith.Gravity.D2DampedScheduleClosure
IndisputableMonolith/Gravity/D2DampedScheduleClosure.lean · 738 lines · 31 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.D2ScopingAudit
2
3/-!
4# D2 Damped-Schedule Closure: the Uniform Residual Is Derived, Not Supplied
5
6## Status: THEOREM (0 sorry, 0 RS-internal axiom)
7
8## What this module closes (D2 open item 2 of `D2ScopingAudit`)
9
10`D2ScopingAudit` names two analytic inputs that the D2 product-filter datum
11had carried as supplied hypothesis fields:
12
131. `D2QuadratureConvergenceTarget` — quadrature proxies converge to the
14 continuum integral across cardinalities, and
152. `D2ResidualVanishingTarget` — the (full nonlinear Regge − quadrature)
16 residual vanishes uniformly on the product filter.
17
18This module **discharges item 2 from the primitive curvature bound**: every
19cardinality slice already carries the Track 1.B local correspondence
20(`hLocal`), i.e. the cubic Taylor bound
21
22 `‖R(ξ) − R(0) − ½·ES(ξ)‖ ≤ C·‖ξ‖³` for `‖ξ‖ < r`,
23
24and that local bound alone forces the two-scale residual to vanish once the
25within-slice refinement schedule is damped per slice. Concretely, for any
26varying-cardinality family `F` and any universal schedule `σ → 0` we build
27the **damped family** `dampedFamily F σ`: same cardinalities, same probes,
28same limiting cell volumes (hence the same quadrature proxies), but
29within-slice spacing `σ(t) · d_S` where the damping factor
30
31 `d_S = min (r_S / (1 + Σ_τ ‖ξ_τ‖)) (1 / (1 + K_S))`,
32 `K_S = (|V_S|/6) · C_S · Σ_τ ‖ξ_τ‖³`
33
34is computed from the slice's own local-correspondence witnesses `(r_S, C_S)`,
35its probe norms, and its limiting cell volume. The damping keeps every
36scaled probe inside the local-correspondence radius and shrinks the per-slice
37residual coefficient below a slice-independent envelope `|σ(t)|`. The
38product uniform residual target then holds for `dampedFamily F σ` with **no
39supplied analytic field** (`dampedFamily_uniformResidual`).
40
41Consequently the full nonlinear Regge → continuum product-filter convergence
42for the damped family needs only the quadrature limit
43(`dampedFamily_fullReggeProduct_tendsto_continuum`), and the master-theorem
44D2 datum for the damped family is constructed with `uniform_residual`
45**proved** (`dampedProductFilterData`).
46
47## What remains open after this module
48
49* `D2QuadratureConvergenceTarget` (item 1): convergence of the explicit
50 finite quadrature sums across cardinalities. This is family-specific
51 geometric data and remains the supplied input.
52* The local correspondence `hLocal` itself: it is a field of every slice
53 (Track 1.B), exactly as it was for the prior reduction; this module adds
54 no new hypothesis beyond what slices already carry.
55* Non-product, non-flat admissible triangulations (item 3 of the audit).
56-/
57
58namespace IndisputableMonolith
59namespace Gravity
60namespace D2DampedScheduleClosure
61
62open PhysicalSixTetCubicDirichletInstance
63open Geometry.ReggeTriangulation3D
64open Geometry.ReggeHessian3D
65open Geometry.Triangulation3DConsistency
66open Geometry.ReggeActionConcrete
67open Geometry.PeriodicFreudenthalTorus
68
69noncomputable section
70
71/-! ## §1. Quadratic homogeneity of the canonical Dirichlet energy -/
72
73/-- The canonical graph-Dirichlet energy is quadratically homogeneous under
74scalar rescaling of the vertex potential. -/
75theorem canonicalDirichletEnergy_smul
76 (K : Triangulation3D) (hK : IncidenceConsistent K)
77 (a : ℝ) (ξ : VertexPotential K) :
78 canonicalDirichletEnergy K hK (a • ξ) =
79 a ^ (2 : ℕ) * canonicalDirichletEnergy K hK ξ := by
80 unfold canonicalDirichletEnergy
81 have h : ∀ i j : Fin K.nV,
82 canonicalDualWeight K hK i j * ((a • ξ) i - (a • ξ) j) ^ (2 : ℕ) =
83 a ^ (2 : ℕ) * (canonicalDualWeight K hK i j * (ξ i - ξ j) ^ (2 : ℕ)) := by
84 intro i j
85 have hsm : (a • ξ) i - (a • ξ) j = a * (ξ i - ξ j) := by
86 simp [Pi.smul_apply, smul_eq_mul, mul_sub]
87 rw [hsm, mul_pow]
88 ring
89 calc (1 / 2) * ∑ i : Fin K.nV, ∑ j : Fin K.nV,
90 canonicalDualWeight K hK i j * ((a • ξ) i - (a • ξ) j) ^ (2 : ℕ)
91 = (1 / 2) * ∑ i : Fin K.nV, ∑ j : Fin K.nV,
92 a ^ (2 : ℕ) * (canonicalDualWeight K hK i j * (ξ i - ξ j) ^ (2 : ℕ)) := by
93 congr 1
94 exact Finset.sum_congr rfl fun i _ =>
95 Finset.sum_congr rfl fun j _ => h i j
96 _ = a ^ (2 : ℕ) *
97 ((1 / 2) * ∑ i : Fin K.nV, ∑ j : Fin K.nV,
98 canonicalDualWeight K hK i j * (ξ i - ξ j) ^ (2 : ℕ)) := by
99 simp only [← Finset.mul_sum]
100 ring
101
102/-! ## §2. Local-correspondence witnesses carried by a slice -/
103
104/-- The local-correspondence radius carried by a cardinality slice. -/
105noncomputable def localRadius
106 {α : Type*} {l : Filter α}
107 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) : ℝ :=
108 letI : NeZero S.Nx := S.instNx
109 letI : NeZero S.Ny := S.instNy
110 letI : NeZero S.Nz := S.instNz
111 S.hLocal.choose
112
113/-- The local-correspondence cubic constant carried by a cardinality slice. -/
114noncomputable def localConstant
115 {α : Type*} {l : Filter α}
116 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) : ℝ :=
117 letI : NeZero S.Nx := S.instNx
118 letI : NeZero S.Ny := S.instNy
119 letI : NeZero S.Nz := S.instNz
120 S.hLocal.choose_spec.choose
121
122theorem localRadius_pos
123 {α : Type*} {l : Filter α}
124 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
125 0 < localRadius S := by
126 letI : NeZero S.Nx := S.instNx
127 letI : NeZero S.Ny := S.instNy
128 letI : NeZero S.Nz := S.instNz
129 exact S.hLocal.choose_spec.choose_spec.1
130
131theorem localConstant_nonneg
132 {α : Type*} {l : Filter α}
133 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
134 0 ≤ localConstant S := by
135 letI : NeZero S.Nx := S.instNx
136 letI : NeZero S.Ny := S.instNy
137 letI : NeZero S.Nz := S.instNz
138 exact S.hLocal.choose_spec.choose_spec.2.1
139
140/-- The cubic Taylor bound carried by a slice, stated for its canonical
141encoded periodic Freudenthal torus. -/
142theorem local_bound
143 {α : Type*} {l : Filter α}
144 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
145 letI : NeZero S.Nx := S.instNx
146 letI : NeZero S.Ny := S.instNy
147 letI : NeZero S.Nz := S.instNz
148 ∀ ξ : VertexPotential
149 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K,
150 ‖ξ‖ < localRadius S →
151 ‖reggeAction
152 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
153 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
154 ξ -
155 reggeAction
156 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
157 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
158 (zeroPotential
159 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K) -
160 (1 / 2) *
161 periodicEdgeStencilDirichletAction
162 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz) ξ‖ ≤
163 localConstant S * ‖ξ‖ ^ (3 : ℕ) := by
164 letI : NeZero S.Nx := S.instNx
165 letI : NeZero S.Ny := S.instNy
166 letI : NeZero S.Nz := S.instNz
167 exact S.hLocal.choose_spec.choose_spec.2.2
168
169/-! ## §3. Probe norms, residual coefficient, and the damping factor -/
170
171/-- Sum of probe norms across the slice's tetrahedra. -/
172noncomputable def probeNormSum
173 {α : Type*} {l : Filter α}
174 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) : ℝ :=
175 letI : NeZero S.Nx := S.instNx
176 letI : NeZero S.Ny := S.instNy
177 letI : NeZero S.Nz := S.instNz
178 ∑ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
179 ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖
180
181/-- Sum of cubed probe norms across the slice's tetrahedra. -/
182noncomputable def probeCubeSum
183 {α : Type*} {l : Filter α}
184 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) : ℝ :=
185 letI : NeZero S.Nx := S.instNx
186 letI : NeZero S.Ny := S.instNy
187 letI : NeZero S.Nz := S.instNz
188 ∑ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
189 ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖ ^ (3 : ℕ)
190
191theorem probeNormSum_nonneg
192 {α : Type*} {l : Filter α}
193 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
194 0 ≤ probeNormSum S := by
195 letI : NeZero S.Nx := S.instNx
196 letI : NeZero S.Ny := S.instNy
197 letI : NeZero S.Nz := S.instNz
198 exact Finset.sum_nonneg fun τ _ => norm_nonneg _
199
200theorem probeCubeSum_nonneg
201 {α : Type*} {l : Filter α}
202 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
203 0 ≤ probeCubeSum S := by
204 letI : NeZero S.Nx := S.instNx
205 letI : NeZero S.Ny := S.instNy
206 letI : NeZero S.Nz := S.instNz
207 exact Finset.sum_nonneg fun τ _ => pow_nonneg (norm_nonneg _) _
208
209/-- The slice residual coefficient: limiting cell-volume weight times the
210local cubic constant times the cubed probe-norm sum. -/
211noncomputable def residualCoefficient
212 {α : Type*} {l : Filter α}
213 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) : ℝ :=
214 letI : NeZero S.Nx := S.instNx
215 letI : NeZero S.Ny := S.instNy
216 letI : NeZero S.Nz := S.instNz
217 |S.data.limitCellVolume| / 6 * localConstant S * probeCubeSum S
218
219theorem residualCoefficient_nonneg
220 {α : Type*} {l : Filter α}
221 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
222 0 ≤ residualCoefficient S :=
223 mul_nonneg
224 (mul_nonneg (div_nonneg (abs_nonneg _) (by norm_num)) (localConstant_nonneg S))
225 (probeCubeSum_nonneg S)
226
227/-- The per-slice damping factor. The first component keeps every damped
228probe inside the local-correspondence radius; the second shrinks the slice
229residual coefficient below one. -/
230noncomputable def dampingFactor
231 {α : Type*} {l : Filter α}
232 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) : ℝ :=
233 min (localRadius S / (1 + probeNormSum S)) (1 / (1 + residualCoefficient S))
234
235theorem one_add_probeNormSum_pos
236 {α : Type*} {l : Filter α}
237 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
238 0 < 1 + probeNormSum S := by
239 have := probeNormSum_nonneg S
240 linarith
241
242theorem one_add_residualCoefficient_pos
243 {α : Type*} {l : Filter α}
244 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
245 0 < 1 + residualCoefficient S := by
246 have := residualCoefficient_nonneg S
247 linarith
248
249theorem dampingFactor_pos
250 {α : Type*} {l : Filter α}
251 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
252 0 < dampingFactor S := by
253 unfold dampingFactor
254 exact lt_min
255 (div_pos (localRadius_pos S) (one_add_probeNormSum_pos S))
256 (div_pos one_pos (one_add_residualCoefficient_pos S))
257
258theorem dampingFactor_le_radius_quotient
259 {α : Type*} {l : Filter α}
260 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
261 dampingFactor S ≤ localRadius S / (1 + probeNormSum S) :=
262 min_le_left _ _
263
264theorem dampingFactor_mul_residualCoefficient_le_one
265 {α : Type*} {l : Filter α}
266 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
267 dampingFactor S * residualCoefficient S ≤ 1 := by
268 have hK := residualCoefficient_nonneg S
269 have h1K := one_add_residualCoefficient_pos S
270 have hd : dampingFactor S ≤ 1 / (1 + residualCoefficient S) := min_le_right _ _
271 calc dampingFactor S * residualCoefficient S
272 ≤ (1 / (1 + residualCoefficient S)) * residualCoefficient S := by
273 exact mul_le_mul_of_nonneg_right hd hK
274 _ ≤ 1 := by
275 rw [div_mul_eq_mul_div, one_mul, div_le_one h1K]
276 linarith
277
278/-! ## §4. The damped slice -/
279
280/-- The damped slice: same cardinality, probes, local correspondence, and
281limiting cell volume; the cell-volume schedule is frozen at its limit and the
282spacing schedule is the universal schedule `σ` damped by the slice's own
283`dampingFactor`. -/
284noncomputable def dampedSlice
285 {α : Type*} {l : Filter α}
286 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l)
287 (σ : α → ℝ)
288 (hσ0 : Filter.Tendsto σ l (nhds 0))
289 (hσne : ∀ᶠ t : α in l, σ t ≠ 0) :
290 CanonicalPeriodicTetSixTetVolumeQuadratureSlice l :=
291 { Nx := S.Nx
292 Ny := S.Ny
293 Nz := S.Nz
294 instNx := S.instNx
295 instNy := S.instNy
296 instNz := S.instNz
297 hx := S.hx
298 hy := S.hy
299 hz := S.hz
300 hLocal := S.hLocal
301 data :=
302 letI : NeZero S.Nx := S.instNx
303 letI : NeZero S.Ny := S.instNy
304 letI : NeZero S.Nz := S.instNz
305 { limitCellVolume := S.data.limitCellVolume
306 cellVolume := fun _ => S.data.limitCellVolume
307 cellVolume_tendsto := tendsto_const_nhds
308 tetProbe := S.data.tetProbe
309 spacing := fun u => σ u * dampingFactor S
310 spacing_tendsto_zero := by
311 simpa using hσ0.mul_const (dampingFactor S)
312 spacing_eventually_ne_zero :=
313 hσne.mono fun u hu => mul_ne_zero hu (dampingFactor_pos S).ne' } }
314
315/-- Damping does not change the slice's finite quadrature proxy. -/
316theorem dampedSlice_quadratureIntegral
317 {α : Type*} {l : Filter α}
318 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l)
319 (σ : α → ℝ)
320 (hσ0 : Filter.Tendsto σ l (nhds 0))
321 (hσne : ∀ᶠ t : α in l, σ t ≠ 0) :
322 (dampedSlice S σ hσ0 hσne).quadratureIntegral = S.quadratureIntegral := rfl
323
324/-! ## §5. The per-tetrahedron normalized residual bound -/
325
326/-- Normalized nonlinear Regge action minus the quadratic Dirichlet limit is
327bounded by the slice's cubic constant times `|s|` times the cubed probe norm,
328whenever the scaled probe sits inside the local-correspondence radius. This
329is the local cubic Taylor bound divided by `s²`. -/
330theorem normalized_regge_sub_limit_abs_le
331 {α : Type*} {l : Filter α}
332 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l)
333 (s : ℝ) (hs : s ≠ 0) :
334 letI : NeZero S.Nx := S.instNx
335 letI : NeZero S.Ny := S.instNy
336 letI : NeZero S.Nz := S.instNz
337 ∀ ξ : VertexPotential
338 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K,
339 ‖s • ξ‖ < localRadius S →
340 |reggeAction
341 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
342 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
343 (s • ξ) / s ^ (2 : ℕ) -
344 (1 / 2) *
345 canonicalDirichletEnergy
346 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
347 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
348 ξ| ≤
349 localConstant S * |s| * ‖ξ‖ ^ (3 : ℕ) := by
350 letI : NeZero S.Nx := S.instNx
351 letI : NeZero S.Ny := S.instNy
352 letI : NeZero S.Nz := S.instNz
353 intro ξ hsmall
354 have hb := local_bound S (s • ξ) hsmall
355 have h0 :
356 reggeAction
357 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
358 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
359 (zeroPotential
360 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K) = 0 :=
361 canonicalPeriodicReggeAction_zeroPotential_eq_zero_of_flatConfiguration
362 S.Nx S.Ny S.Nz S.hx S.hy S.hz
363 (canonicalPeriodicFlatConfiguration S.Nx S.Ny S.Nz S.hx S.hy S.hz)
364 have hES :
365 canonicalDirichletEnergy
366 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
367 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
368 (s • ξ) =
369 periodicEdgeStencilDirichletAction
370 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz) (s • ξ) :=
371 canonicalPeriodicEdgeStencilTarget S.Nx S.Ny S.Nz S.hx S.hy S.hz (s • ξ)
372 have hsm :
373 canonicalDirichletEnergy
374 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
375 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
376 (s • ξ) =
377 s ^ (2 : ℕ) *
378 canonicalDirichletEnergy
379 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
380 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
381 ξ :=
382 canonicalDirichletEnergy_smul _ _ s ξ
383 rw [h0, sub_zero, ← hES, hsm, Real.norm_eq_abs] at hb
384 have hs2 : (0 : ℝ) < s ^ (2 : ℕ) := by positivity
385 have key :
386 reggeAction
387 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
388 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
389 (s • ξ) / s ^ (2 : ℕ) -
390 (1 / 2) *
391 canonicalDirichletEnergy
392 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
393 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
394 ξ =
395 (reggeAction
396 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
397 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
398 (s • ξ) -
399 (1 / 2) *
400 (s ^ (2 : ℕ) *
401 canonicalDirichletEnergy
402 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
403 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
404 ξ)) / s ^ (2 : ℕ) := by
405 field_simp
406 rw [key, abs_div, abs_of_pos hs2]
407 have hnorm3 : ‖s • ξ‖ ^ (3 : ℕ) = |s| ^ (3 : ℕ) * ‖ξ‖ ^ (3 : ℕ) := by
408 rw [norm_smul, Real.norm_eq_abs, mul_pow]
409 have habs3 : |s| ^ (3 : ℕ) = |s| * s ^ (2 : ℕ) := by
410 rw [pow_succ, sq_abs, mul_comm]
411 have hdivle :
412 |reggeAction
413 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
414 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
415 (s • ξ) -
416 (1 / 2) *
417 (s ^ (2 : ℕ) *
418 canonicalDirichletEnergy
419 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
420 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
421 ξ)| / s ^ (2 : ℕ) ≤
422 (localConstant S * ‖s • ξ‖ ^ (3 : ℕ)) / s ^ (2 : ℕ) := by
423 gcongr
424 refine le_trans hdivle (le_of_eq ?_)
425 rw [hnorm3, habs3]
426 field_simp
427
428/-! ## §6. The damped-slice residual bound -/
429
430/-- The damped slice's full nonlinear Regge aggregate minus its quadrature
431proxy is bounded by `|σ t|`, uniformly in the slice, whenever `σ t ≠ 0` and
432`|σ t| ≤ 1`. The damping factor absorbs the slice's local radius, cubic
433constant, probe norms, and limiting cell volume. -/
434theorem dampedSlice_residual_abs_le
435 {α : Type*} {l : Filter α}
436 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l)
437 (σ : α → ℝ)
438 (hσ0 : Filter.Tendsto σ l (nhds 0))
439 (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
440 (t : α) (hne : σ t ≠ 0) (hle : |σ t| ≤ 1) :
441 |(dampedSlice S σ hσ0 hσne).fullReggeAggregate t -
442 (dampedSlice S σ hσ0 hσne).quadratureIntegral| ≤ |σ t| := by
443 letI : NeZero S.Nx := S.instNx
444 letI : NeZero S.Ny := S.instNy
445 letI : NeZero S.Nz := S.instNz
446 have hd_pos : 0 < dampingFactor S := dampingFactor_pos S
447 have hs_ne : σ t * dampingFactor S ≠ 0 := mul_ne_zero hne hd_pos.ne'
448 have habs_s : |σ t * dampingFactor S| = |σ t| * dampingFactor S := by
449 rw [abs_mul, abs_of_pos hd_pos]
450 have habs_s_le : |σ t * dampingFactor S| ≤ dampingFactor S := by
451 rw [habs_s]
452 exact mul_le_of_le_one_left hd_pos.le hle
453 -- The damped aggregate and quadrature proxy as explicit tetrahedron sums.
454 have hAgg : (dampedSlice S σ hσ0 hσne).fullReggeAggregate t =
455 ∑ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
456 canonicalPeriodicFreudenthalTetVolumeWeight S.Nx S.Ny S.Nz
457 S.data.limitCellVolume (tetFinEquiv S.Nx S.Ny S.Nz τ) *
458 (reggeAction
459 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
460 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
461 ((σ t * dampingFactor S) • S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)) /
462 (σ t * dampingFactor S) ^ (2 : ℕ)) := rfl
463 have hQuad : (dampedSlice S σ hσ0 hσne).quadratureIntegral =
464 ∑ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
465 canonicalPeriodicFreudenthalTetVolumeWeight S.Nx S.Ny S.Nz
466 S.data.limitCellVolume (tetFinEquiv S.Nx S.Ny S.Nz τ) *
467 ((1 / 2) *
468 canonicalDirichletEnergy
469 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
470 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
471 (S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ))) := rfl
472 rw [hAgg, hQuad, ← Finset.sum_sub_distrib]
473 simp only [canonicalPeriodicFreudenthalTetVolumeWeight, ← mul_sub]
474 -- Every damped probe sits inside the local-correspondence radius.
475 have hsmall : ∀ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
476 ‖(σ t * dampingFactor S) • S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖ <
477 localRadius S := by
478 intro τ
479 have hM : ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖ ≤ probeNormSum S :=
480 Finset.single_le_sum (f := fun τ' =>
481 ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ')‖)
482 (fun τ' _ => norm_nonneg _) (Finset.mem_univ τ)
483 have h1M : 0 < 1 + probeNormSum S := one_add_probeNormSum_pos S
484 have hM_lt : ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖ < 1 + probeNormSum S := by
485 linarith
486 have hq_pos : 0 < localRadius S / (1 + probeNormSum S) :=
487 div_pos (localRadius_pos S) h1M
488 calc ‖(σ t * dampingFactor S) • S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖
489 = |σ t * dampingFactor S| *
490 ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖ := by
491 rw [norm_smul, Real.norm_eq_abs]
492 _ ≤ (localRadius S / (1 + probeNormSum S)) *
493 ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖ := by
494 exact mul_le_mul_of_nonneg_right
495 (le_trans habs_s_le (dampingFactor_le_radius_quotient S)) (norm_nonneg _)
496 _ < (localRadius S / (1 + probeNormSum S)) * (1 + probeNormSum S) := by
497 exact mul_lt_mul_of_pos_left hM_lt hq_pos
498 _ = localRadius S := div_mul_cancel₀ _ h1M.ne'
499 -- Per-tetrahedron bound from the normalized cubic Taylor estimate.
500 have hper : ∀ τ ∈ (Finset.univ : Finset (Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)))),
501 |S.data.limitCellVolume / 6 *
502 (reggeAction
503 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
504 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
505 ((σ t * dampingFactor S) • S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)) /
506 (σ t * dampingFactor S) ^ (2 : ℕ) -
507 (1 / 2) *
508 canonicalDirichletEnergy
509 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
510 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
511 (S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)))| ≤
512 |S.data.limitCellVolume| / 6 *
513 (localConstant S * |σ t * dampingFactor S| *
514 ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖ ^ (3 : ℕ)) := by
515 intro τ _
516 rw [abs_mul]
517 have hwabs : |S.data.limitCellVolume / 6| = |S.data.limitCellVolume| / 6 := by
518 rw [abs_div, abs_of_pos (by norm_num : (0 : ℝ) < 6)]
519 rw [hwabs]
520 exact mul_le_mul_of_nonneg_left
521 (normalized_regge_sub_limit_abs_le S (σ t * dampingFactor S) hs_ne
522 (S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)) (hsmall τ))
523 (div_nonneg (abs_nonneg _) (by norm_num))
524 refine le_trans (Finset.abs_sum_le_sum_abs _ _) (le_trans (Finset.sum_le_sum hper) ?_)
525 -- Collapse the sum to the residual coefficient and absorb the damping.
526 have hrc : residualCoefficient S =
527 |S.data.limitCellVolume| / 6 * localConstant S *
528 (∑ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
529 ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖ ^ (3 : ℕ)) := rfl
530 have hsum_eq :
531 (∑ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
532 |S.data.limitCellVolume| / 6 *
533 (localConstant S * |σ t * dampingFactor S| *
534 ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖ ^ (3 : ℕ))) =
535 |σ t * dampingFactor S| * residualCoefficient S := by
536 rw [hrc]
537 simp only [Finset.mul_sum]
538 exact Finset.sum_congr rfl fun τ _ => by ring
539 rw [hsum_eq, habs_s]
540 calc |σ t| * dampingFactor S * residualCoefficient S
541 = |σ t| * (dampingFactor S * residualCoefficient S) := by ring
542 _ ≤ |σ t| * 1 :=
543 mul_le_mul_of_nonneg_left
544 (dampingFactor_mul_residualCoefficient_le_one S) (abs_nonneg _)
545 _ = |σ t| := mul_one _
546
547/-! ## §7. The damped family and the derived uniform residual -/
548
549/-- Damp every slice of a varying-cardinality family with the same universal
550schedule `σ`. Cardinalities, probes, and quadrature proxies are unchanged. -/
551noncomputable def dampedFamily
552 {α ρ : Type*} {l : Filter α}
553 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
554 (σ : α → ℝ)
555 (hσ0 : Filter.Tendsto σ l (nhds 0))
556 (hσne : ∀ᶠ t : α in l, σ t ≠ 0) :
557 CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ where
558 slice := fun r => dampedSlice (F.slice r) σ hσ0 hσne
559
560/-- **DERIVED UNIFORM RESIDUAL (D2 open item 2 discharged).** The damped
561family satisfies the product uniform-residual target for every refinement
562filter. No analytic residual field is supplied: the bound comes from each
563slice's own local cubic Taylor correspondence, the flat-action normalization,
564the edge-stencil Dirichlet identification, and the constructed damping. -/
565theorem dampedFamily_uniformResidual
566 {α ρ : Type*} {l : Filter α}
567 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
568 (σ : α → ℝ)
569 (hσ0 : Filter.Tendsto σ l (nhds 0))
570 (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
571 (refinementFilter : Filter ρ) :
572 CanonicalPeriodicTetSixTetVolumeQuadratureProductUniformResidualTarget
573 (dampedFamily F σ hσ0 hσne) refinementFilter := by
574 refine canonicalPeriodicTetSixTetVolumeQuadratureProductUniformResidualTarget_of_snd_abs_bound
575 (dampedFamily F σ hσ0 hσne) refinementFilter (fun t => |σ t|) ?_ ?_
576 · simpa using hσ0.abs
577 · have h1 : ∀ᶠ t : α in l, |σ t| ≤ 1 := by
578 have hball : Metric.closedBall (0 : ℝ) 1 ∈ nhds (0 : ℝ) :=
579 Metric.closedBall_mem_nhds 0 one_pos
580 have := hσ0.eventually_mem hball
581 simpa [Metric.mem_closedBall, Real.dist_eq] using this
582 refine ((hσne.and h1).prod_inr refinementFilter).mono ?_
583 rintro ⟨r, t⟩ ⟨ht_ne, ht_le⟩
584 exact dampedSlice_residual_abs_le (F.slice r) σ hσ0 hσne t ht_ne ht_le
585
586/-- The damped family inherits the cross-cardinality quadrature target from
587the base family, since damping preserves every quadrature proxy. -/
588theorem dampedFamily_quadrature_target
589 {α ρ : Type*} {l : Filter α}
590 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
591 (σ : α → ℝ)
592 (hσ0 : Filter.Tendsto σ l (nhds 0))
593 (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
594 (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
595 (hquad :
596 CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
597 F refinementFilter continuumIntegral) :
598 CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
599 (dampedFamily F σ hσ0 hσne) refinementFilter continuumIntegral := by
600 unfold CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget at hquad ⊢
601 simpa only [dampedFamily, dampedSlice_quadratureIntegral] using hquad
602
603/-! ## §8. The D2 datum with a proved residual field, and the closure -/
604
605/-- The master-theorem D2 product-filter datum for the damped family. The
606`uniform_residual` field is **proved**, not supplied; the only analytic input
607is the cross-cardinality quadrature limit. -/
608noncomputable def dampedProductFilterData
609 {α ρ : Type*} {l : Filter α}
610 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
611 (σ : α → ℝ)
612 (hσ0 : Filter.Tendsto σ l (nhds 0))
613 (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
614 (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
615 (hquad :
616 CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
617 F refinementFilter continuumIntegral) :
618 CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l where
619 family := dampedFamily F σ hσ0 hσne
620 refinementFilter := refinementFilter
621 continuumIntegral := continuumIntegral
622 quadrature_tendsto :=
623 dampedFamily_quadrature_target F σ hσ0 hσne refinementFilter continuumIntegral hquad
624 uniform_residual :=
625 dampedFamily_uniformResidual F σ hσ0 hσne refinementFilter
626
627/-- **D2 DAMPED-SCHEDULE CLOSURE.** For every varying-cardinality slice
628family and every universal schedule `σ → 0`, the full nonlinear Regge
629aggregate of the damped family converges to the continuum integral on the
630product filter, given only the cross-cardinality quadrature limit. The
631two-scale uniform residual is derived, not assumed. -/
632theorem dampedFamily_fullReggeProduct_tendsto_continuum
633 {α ρ : Type*} {l : Filter α}
634 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
635 (σ : α → ℝ)
636 (hσ0 : Filter.Tendsto σ l (nhds 0))
637 (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
638 (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
639 (hquad :
640 CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
641 F refinementFilter continuumIntegral) :
642 Filter.Tendsto
643 (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
644 (α := α) (ρ := ρ) (dampedFamily F σ hσ0 hσne))
645 (refinementFilter ×ˢ l : Filter (ρ × α))
646 (nhds continuumIntegral) :=
647 (dampedProductFilterData F σ hσ0 hσne refinementFilter continuumIntegral
648 hquad).fullReggeProduct_tendsto_continuum
649
650/-- The damped datum satisfies the Track 1.B-PHY concrete product-filter
651target consumed by the quantum-gravity master theorem. -/
652theorem dampedProductFilterData_satisfies_master_target
653 {α ρ : Type*} {l : Filter α}
654 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
655 (σ : α → ℝ)
656 (hσ0 : Filter.Tendsto σ l (nhds 0))
657 (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
658 (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
659 (hquad :
660 CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
661 F refinementFilter continuumIntegral) :
662 Track1BCPhysicalResidual.PhysicalReggeEHConcreteProductFilterTarget
663 (dampedProductFilterData F σ hσ0 hσne refinementFilter continuumIntegral hquad) :=
664 Track1BCPhysicalResidual.physicalReggeEHConcreteProductFilterTarget_holds
665 (dampedProductFilterData F σ hσ0 hσne refinementFilter continuumIntegral hquad)
666
667/-! ## §9. Restatement against the named D2 audit targets -/
668
669/-- **`D2ResidualVanishingTarget` holds for damped schedules.** Stated in the
670exact vocabulary of `D2ScopingAudit`: for every family, the residual target of
671the damped family is a theorem, with the bound built from each slice's local
672correspondence (the primitive curvature bound) and the constructed spacing
673damping. -/
674theorem d2_residual_vanishing_target_damped
675 {α ρ : Type*} {l : Filter α}
676 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
677 (σ : α → ℝ)
678 (hσ0 : Filter.Tendsto σ l (nhds 0))
679 (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
680 (refinementFilter : Filter ρ) :
681 D2ScopingAudit.D2ResidualVanishingTarget l (dampedFamily F σ hσ0 hσne)
682 refinementFilter :=
683 dampedFamily_uniformResidual F σ hσ0 hσne refinementFilter
684
685/-- **D2 reduced to one analytic input.** In the audit's vocabulary: the
686quadrature target alone implies the full nonlinear product-filter convergence
687for the damped family. Compare `D2ScopingAudit.d2_reduction_statement`,
688which consumed both targets. -/
689theorem d2_reduction_to_quadrature_only
690 {α ρ : Type*} {l : Filter α}
691 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
692 (σ : α → ℝ)
693 (hσ0 : Filter.Tendsto σ l (nhds 0))
694 (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
695 (refinementFilter : Filter ρ) (continuumIntegral : ℝ) :
696 D2ScopingAudit.D2QuadratureConvergenceTarget l F refinementFilter continuumIntegral →
697 Filter.Tendsto
698 (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
699 (α := α) (ρ := ρ) (dampedFamily F σ hσ0 hσne))
700 (refinementFilter ×ˢ l : Filter (ρ × α))
701 (nhds continuumIntegral) :=
702 fun hquad =>
703 dampedFamily_fullReggeProduct_tendsto_continuum F σ hσ0 hσne refinementFilter
704 continuumIntegral hquad
705
706/-- One-statement bundle for citation: damping preserves quadrature proxies,
707derives the uniform residual outright, and reduces full D2 convergence to the
708quadrature limit alone. -/
709theorem d2_damped_schedule_closure_one_statement
710 {α ρ : Type*} {l : Filter α}
711 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
712 (σ : α → ℝ)
713 (hσ0 : Filter.Tendsto σ l (nhds 0))
714 (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
715 (refinementFilter : Filter ρ) :
716 (∀ r : ρ,
717 ((dampedFamily F σ hσ0 hσne).slice r).quadratureIntegral =
718 (F.slice r).quadratureIntegral) ∧
719 D2ScopingAudit.D2ResidualVanishingTarget l (dampedFamily F σ hσ0 hσne)
720 refinementFilter ∧
721 (∀ continuumIntegral : ℝ,
722 D2ScopingAudit.D2QuadratureConvergenceTarget l F refinementFilter continuumIntegral →
723 Filter.Tendsto
724 (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
725 (α := α) (ρ := ρ) (dampedFamily F σ hσ0 hσne))
726 (refinementFilter ×ˢ l : Filter (ρ × α))
727 (nhds continuumIntegral)) :=
728 ⟨fun r => dampedSlice_quadratureIntegral (F.slice r) σ hσ0 hσne,
729 d2_residual_vanishing_target_damped F σ hσ0 hσne refinementFilter,
730 fun continuumIntegral hquad =>
731 d2_reduction_to_quadrature_only F σ hσ0 hσne refinementFilter continuumIntegral hquad⟩
732
733end
734
735end D2DampedScheduleClosure
736end Gravity
737end IndisputableMonolith
738