IndisputableMonolith.Gravity.D2QuadratureInstances
IndisputableMonolith/Gravity/D2QuadratureInstances.lean · 321 lines · 12 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.D2DampedScheduleClosure
2
3/-!
4# D2 Quadrature Instances: the Flat Sector Closes, the Curved Sector Reduces
5
6## Status: THEOREM (0 sorry, 0 RS-internal axiom)
7
8## What this module adds on top of `D2DampedScheduleClosure`
9
10The damped-schedule closure discharged the uniform-residual input of the D2
11reduction. The remaining analytic input is the cross-cardinality quadrature
12limit (`D2QuadratureConvergenceTarget`). This module does two things to it.
13
14**1. The flat sector closes unconditionally.** Flattening a family
15(replacing every tetrahedron probe by the zero potential) makes every slice
16quadrature proxy exactly zero, because the canonical Dirichlet energy of the
17zero potential vanishes. The quadrature target then holds at the flat
18continuum integral `0` with no hypothesis, and combining with the damped
19residual closure gives `dampedFlat_fullReggeProduct_tendsto_zero`: the full
20nonlinear Regge aggregate of the damped flat family converges to the flat
21Einstein-Hilbert value on the product filter, with **both** former analytic
22fields proved. `dampedFlatProductFilterData` is the first D2 master datum in
23the library whose `quadrature_tendsto` and `uniform_residual` fields are both
24theorems, consuming only the Track 1.B local-correspondence data that every
25slice carries by definition.
26
27**2. The curved sector reduces to a scalar Dirichlet limit.** For a slice
28whose tetrahedron probes are all equal to one global potential `ξ`, the
29quadrature proxy collapses by translation counting to
30
31 `(card tets) · (V/6) · (½ · DirichletEnergy ξ)`,
32
33so the cross-cardinality quadrature target is equivalent, for uniform-probe
34families, to convergence of an explicit scalar sequence of scaled Dirichlet
35energies (`quadrature_target_iff_of_proxy_eq` +
36`quadratureIntegral_of_uniform_probe`). The open D2 quadrature input is
37thereby no longer an abstract `Tendsto` of opaque proxies: it is a concrete
38numerical limit of finite graph-Dirichlet energies.
39
40## What remains open
41
42* The scalar Dirichlet limit itself for curvature-bearing probe families
43 (the genuine Riemann-sum content of D2).
44* The Track 1.B local correspondence at each cardinality (`hLocal`), carried
45 by slices as before.
46* Non-product, non-flat admissible triangulations.
47-/
48
49namespace IndisputableMonolith
50namespace Gravity
51namespace D2QuadratureInstances
52
53open PhysicalSixTetCubicDirichletInstance
54open D2DampedScheduleClosure
55open Geometry.ReggeTriangulation3D
56open Geometry.ReggeHessian3D
57open Geometry.Triangulation3DConsistency
58open Geometry.ReggeActionConcrete
59open Geometry.PeriodicFreudenthalTorus
60
61noncomputable section
62
63/-! ## §1. The canonical Dirichlet energy of the zero potential vanishes -/
64
65theorem canonicalDirichletEnergy_zero
66 (K : Triangulation3D) (hK : IncidenceConsistent K) :
67 canonicalDirichletEnergy K hK (zeroPotential K) = 0 := by
68 unfold canonicalDirichletEnergy zeroPotential
69 simp
70
71/-! ## §2. Flattening a slice: zero probes, everything else unchanged -/
72
73/-- The flattened slice: same cardinality, local correspondence, cell-volume
74and spacing schedules; every tetrahedron probe replaced by the zero
75potential. -/
76noncomputable def flattenSlice
77 {α : Type*} {l : Filter α}
78 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
79 CanonicalPeriodicTetSixTetVolumeQuadratureSlice l :=
80 { Nx := S.Nx
81 Ny := S.Ny
82 Nz := S.Nz
83 instNx := S.instNx
84 instNy := S.instNy
85 instNz := S.instNz
86 hx := S.hx
87 hy := S.hy
88 hz := S.hz
89 hLocal := S.hLocal
90 data :=
91 letI : NeZero S.Nx := S.instNx
92 letI : NeZero S.Ny := S.instNy
93 letI : NeZero S.Nz := S.instNz
94 { limitCellVolume := S.data.limitCellVolume
95 cellVolume := S.data.cellVolume
96 cellVolume_tendsto := S.data.cellVolume_tendsto
97 tetProbe := fun _ =>
98 zeroPotential
99 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
100 spacing := S.data.spacing
101 spacing_tendsto_zero := S.data.spacing_tendsto_zero
102 spacing_eventually_ne_zero := S.data.spacing_eventually_ne_zero } }
103
104/-- The flattened slice's quadrature proxy is exactly zero. -/
105theorem flattenSlice_quadratureIntegral
106 {α : Type*} {l : Filter α}
107 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
108 (flattenSlice S).quadratureIntegral = 0 := by
109 letI : NeZero S.Nx := S.instNx
110 letI : NeZero S.Ny := S.instNy
111 letI : NeZero S.Nz := S.instNz
112 have h : (flattenSlice S).quadratureIntegral =
113 ∑ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
114 canonicalPeriodicFreudenthalTetVolumeWeight S.Nx S.Ny S.Nz
115 S.data.limitCellVolume (tetFinEquiv S.Nx S.Ny S.Nz τ) *
116 ((1 / 2) *
117 canonicalDirichletEnergy
118 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
119 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
120 (zeroPotential
121 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K)) :=
122 rfl
123 rw [h]
124 simp [canonicalDirichletEnergy_zero]
125
126/-! ## §3. The flattened family and its quadrature target at zero -/
127
128/-- Flatten every slice of a family. -/
129noncomputable def flatFamily
130 {α ρ : Type*} {l : Filter α}
131 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ) :
132 CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ where
133 slice := fun r => flattenSlice (F.slice r)
134
135/-- **The flat-sector quadrature target holds with no hypothesis.** The
136flattened family's quadrature proxies are identically zero, so they converge
137to the flat continuum Einstein-Hilbert value `0` along every refinement
138filter. -/
139theorem flatFamily_quadrature_target
140 {α ρ : Type*} {l : Filter α}
141 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
142 (refinementFilter : Filter ρ) :
143 CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
144 (flatFamily F) refinementFilter 0 := by
145 unfold CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
146 have h : (fun r : ρ => ((flatFamily F).slice r).quadratureIntegral) =
147 fun _ : ρ => (0 : ℝ) := by
148 funext r
149 exact flattenSlice_quadratureIntegral (F.slice r)
150 rw [h]
151 exact tendsto_const_nhds
152
153/-- The flat-sector quadrature target in the audit's vocabulary. -/
154theorem d2_quadrature_target_flat
155 {α ρ : Type*} {l : Filter α}
156 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
157 (refinementFilter : Filter ρ) :
158 D2ScopingAudit.D2QuadratureConvergenceTarget l (flatFamily F) refinementFilter 0 :=
159 flatFamily_quadrature_target F refinementFilter
160
161/-! ## §4. The unconditional flat-sector closure -/
162
163/-- **FLAT-SECTOR D2 CLOSURE (no supplied analytic inputs).** For every
164slice family and every universal schedule, the full nonlinear Regge aggregate
165of the damped flattened family converges to the flat continuum value `0` on
166the product filter. Both former analytic inputs are theorems here: the
167quadrature target by §3, the uniform residual by the damped-schedule
168closure. The only data consumed are the slices themselves, including the
169Track 1.B local correspondence they carry by definition. -/
170theorem dampedFlat_fullReggeProduct_tendsto_zero
171 {α ρ : Type*} {l : Filter α}
172 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
173 (σ : α → ℝ)
174 (hσ0 : Filter.Tendsto σ l (nhds 0))
175 (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
176 (refinementFilter : Filter ρ) :
177 Filter.Tendsto
178 (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
179 (α := α) (ρ := ρ) (dampedFamily (flatFamily F) σ hσ0 hσne))
180 (refinementFilter ×ˢ l : Filter (ρ × α))
181 (nhds 0) :=
182 dampedFamily_fullReggeProduct_tendsto_continuum (flatFamily F) σ hσ0 hσne
183 refinementFilter 0 (flatFamily_quadrature_target F refinementFilter)
184
185/-- The first D2 master datum whose `quadrature_tendsto` and
186`uniform_residual` fields are both proved rather than supplied. -/
187noncomputable def dampedFlatProductFilterData
188 {α ρ : Type*} {l : Filter α}
189 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
190 (σ : α → ℝ)
191 (hσ0 : Filter.Tendsto σ l (nhds 0))
192 (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
193 (refinementFilter : Filter ρ) :
194 CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l :=
195 dampedProductFilterData (flatFamily F) σ hσ0 hσne refinementFilter 0
196 (flatFamily_quadrature_target F refinementFilter)
197
198/-- The flat datum satisfies the Track 1.B-PHY concrete product-filter target
199consumed by the quantum-gravity master theorem. -/
200theorem dampedFlatProductFilterData_satisfies_master_target
201 {α ρ : Type*} {l : Filter α}
202 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
203 (σ : α → ℝ)
204 (hσ0 : Filter.Tendsto σ l (nhds 0))
205 (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
206 (refinementFilter : Filter ρ) :
207 Track1BCPhysicalResidual.PhysicalReggeEHConcreteProductFilterTarget
208 (dampedFlatProductFilterData F σ hσ0 hσne refinementFilter) :=
209 Track1BCPhysicalResidual.physicalReggeEHConcreteProductFilterTarget_holds
210 (dampedFlatProductFilterData F σ hσ0 hσne refinementFilter)
211
212/-! ## §5. Uniform-probe slices: the quadrature proxy is a scaled Dirichlet
213energy -/
214
215/-- For a slice whose tetrahedron probes are all the same global potential,
216the quadrature proxy collapses to tetrahedron count times limiting cell
217weight times the Dirichlet limit action of that potential. -/
218theorem quadratureIntegral_of_uniform_probe
219 {α : Type*} {l : Filter α}
220 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
221 letI : NeZero S.Nx := S.instNx
222 letI : NeZero S.Ny := S.instNy
223 letI : NeZero S.Nz := S.instNz
224 ∀ ξ : VertexPotential
225 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K,
226 (∀ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
227 S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ) = ξ) →
228 S.quadratureIntegral =
229 (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz) : ℝ) *
230 (S.data.limitCellVolume / 6) *
231 ((1 / 2) *
232 canonicalDirichletEnergy
233 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
234 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
235 ξ) := by
236 letI : NeZero S.Nx := S.instNx
237 letI : NeZero S.Ny := S.instNy
238 letI : NeZero S.Nz := S.instNz
239 intro ξ hξ
240 have h : S.quadratureIntegral =
241 ∑ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
242 canonicalPeriodicFreudenthalTetVolumeWeight S.Nx S.Ny S.Nz
243 S.data.limitCellVolume (tetFinEquiv S.Nx S.Ny S.Nz τ) *
244 ((1 / 2) *
245 canonicalDirichletEnergy
246 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
247 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
248 (S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ))) := rfl
249 rw [h]
250 have hterm : ∀ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
251 canonicalPeriodicFreudenthalTetVolumeWeight S.Nx S.Ny S.Nz
252 S.data.limitCellVolume (tetFinEquiv S.Nx S.Ny S.Nz τ) *
253 ((1 / 2) *
254 canonicalDirichletEnergy
255 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
256 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
257 (S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ))) =
258 S.data.limitCellVolume / 6 *
259 ((1 / 2) *
260 canonicalDirichletEnergy
261 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
262 (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
263 ξ) := by
264 intro τ
265 rw [hξ τ]
266 simp only [canonicalPeriodicFreudenthalTetVolumeWeight]
267 rw [Finset.sum_congr rfl fun τ _ => hterm τ]
268 rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
269 ring
270
271/-- Transport the cross-cardinality quadrature target along any explicit
272formula for the slice proxies. Together with
273`quadratureIntegral_of_uniform_probe`, this turns the open D2 quadrature
274input for uniform-probe families into a scalar limit of scaled Dirichlet
275energies. -/
276theorem quadrature_target_iff_of_proxy_eq
277 {α ρ : Type*} {l : Filter α}
278 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
279 (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
280 (g : ρ → ℝ)
281 (hg : ∀ r : ρ, (F.slice r).quadratureIntegral = g r) :
282 CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
283 F refinementFilter continuumIntegral ↔
284 Filter.Tendsto g refinementFilter (nhds continuumIntegral) := by
285 unfold CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
286 exact Filter.tendsto_congr hg
287
288/-! ## §6. One-statement bundle -/
289
290/-- **D2 status after this module, in one statement.** For every slice
291family `F` and universal schedule `σ`: the flattened family's quadrature
292target holds at the flat value `0` with no hypothesis; the damped flattened
293family's residual target holds with no hypothesis; and the full nonlinear
294Regge aggregate of the damped flattened family converges to `0` on the
295product filter. The flat sector of D2 is closed end to end on the canonical
296route, with no supplied analytic field anywhere. -/
297theorem d2_flat_sector_one_statement
298 {α ρ : Type*} {l : Filter α}
299 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
300 (σ : α → ℝ)
301 (hσ0 : Filter.Tendsto σ l (nhds 0))
302 (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
303 (refinementFilter : Filter ρ) :
304 D2ScopingAudit.D2QuadratureConvergenceTarget l (flatFamily F) refinementFilter 0 ∧
305 D2ScopingAudit.D2ResidualVanishingTarget l (dampedFamily (flatFamily F) σ hσ0 hσne)
306 refinementFilter ∧
307 Filter.Tendsto
308 (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
309 (α := α) (ρ := ρ) (dampedFamily (flatFamily F) σ hσ0 hσne))
310 (refinementFilter ×ˢ l : Filter (ρ × α))
311 (nhds 0) :=
312 ⟨d2_quadrature_target_flat F refinementFilter,
313 d2_residual_vanishing_target_damped (flatFamily F) σ hσ0 hσne refinementFilter,
314 dampedFlat_fullReggeProduct_tendsto_zero F σ hσ0 hσne refinementFilter⟩
315
316end
317
318end D2QuadratureInstances
319end Gravity
320end IndisputableMonolith
321