IndisputableMonolith.Gravity.Track1BCPhysicalResidual
IndisputableMonolith/Gravity/Track1BCPhysicalResidual.lean · 819 lines · 69 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.Track1BCStructural
2import IndisputableMonolith.Gravity.PhysicalSixTetCubicDirichletInstance
3
4/-!
5# Track 1.B-PHY: Physical Regge → EH Residual Structural Upgrade
6
7This module packages the physical finite-probe Regge-to-EH residual theorems
8from `Gravity.PhysicalSixTetCubicDirichletInstance` as a named Track 1.B-PHY
9upgrade beyond the flat-substrate witness in `Gravity.Track1BCStructural`.
10
11Status: **STRUCTURAL THEOREM** (0 sorry, 0 new RS-specific axiom).
12
13What is closed here:
14* normalized full nonlinear Regge finite aggregates converge to the canonical
15 finite EH/Dirichlet action, with an explicit residual tending to zero, once
16 edge-stencil local correspondence holds;
17* the same local correspondence feeds the finite-to-continuum bridge when a
18 Riemann-sum identification is supplied.
19
20What remains for the unconditional manifold Einstein-Hilbert theorem:
21* `PhysicalReggeEHManifoldIntegralRemainingTarget`, i.e.
22 `CanonicalPeriodicFiniteEHDirichletLimitWeightIntegralTarget` on a concrete
23 periodic Freudenthal refinement family.
24-/
25
26namespace IndisputableMonolith
27namespace Gravity
28namespace Track1BCPhysicalResidual
29
30open PhysicalSixTetCubicDirichletInstance
31open Track1BCStructural
32open Geometry.ReggeHessian3D
33open Geometry.ReggeActionConcrete
34open Geometry.PeriodicFreudenthalTorus
35
36noncomputable section
37
38/-- Named Track 1.B-PHY target at a fixed local-correspondence input: the
39normalized full nonlinear Regge finite-probe aggregate minus the canonical
40finite EH/Dirichlet aggregate tends to zero along any refinement family. -/
41theorem physicalReggeEHFiniteProbeResidualTarget
42 {α : Type*} {l : Filter α}
43 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
44 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
45 (hLocal : CanonicalPeriodicEdgeStencilLocalCorrespondence Nx Ny Nz hx hy hz) :
46 ∃ (r C : ℝ), 0 < r ∧ 0 ≤ C ∧
47 ∀ {n : ℕ}
48 (spacing : α → ℝ)
49 (probe :
50 Fin n →
51 VertexPotential
52 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K)
53 (weight : α → Fin n → ℝ)
54 (limitWeight : Fin n → ℝ),
55 (∀ i : Fin n, Filter.Tendsto (fun t : α => weight t i) l (nhds (limitWeight i))) →
56 Filter.Tendsto spacing l (nhds 0) →
57 (∀ᶠ t : α in l, spacing t ≠ 0) →
58 Filter.Tendsto
59 (fun t : α =>
60 (∑ i : Fin n,
61 weight t i *
62 (reggeAction
63 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K
64 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).hK
65 (spacing t • probe i) /
66 ‖spacing t‖ ^ (2 : ℕ))) -
67 ∑ i : Fin n,
68 limitWeight i *
69 CanonicalPeriodicFiniteEHDirichletLimitAction
70 Nx Ny Nz hx hy hz (probe i))
71 l (nhds 0) :=
72 canonicalPeriodicFullRegge_variable_weighted_finite_probe_spacing_scaled_div_spacing_norm_sq_finiteEHDirichletLimit_residual_tendsto_zero
73 Nx Ny Nz hx hy hz hLocal
74
75/-- After local correspondence, the remaining manifold-level Track 1.B-PHY
76input is exactly the Riemann-sum identification of the limiting finite
77EH/Dirichlet aggregate with a supplied continuum integral. -/
78def PhysicalReggeEHManifoldIntegralRemainingTarget
79 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
80 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz) : Prop :=
81 ∀ {n : ℕ}
82 (probe :
83 Fin n →
84 VertexPotential (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K)
85 (limitWeight : Fin n → ℝ)
86 (continuumIntegral : CanonicalPeriodicContinuumEHIntegral),
87 CanonicalPeriodicFiniteEHDirichletLimitWeightIntegralTarget
88 Nx Ny Nz hx hy hz probe limitWeight continuumIntegral
89
90theorem physicalReggeEHFullRegge_tendsto_continuumIntegral_of_localCorrespondence
91 {α : Type*} {l : Filter α}
92 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
93 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
94 (hLocal : CanonicalPeriodicEdgeStencilLocalCorrespondence Nx Ny Nz hx hy hz)
95 (D : CanonicalPeriodicFiniteEHDirichletIntegralRefinementData l Nx Ny Nz hx hy hz) :
96 Filter.Tendsto
97 (fun t : α =>
98 ∑ i : Fin D.n,
99 D.weight t i *
100 (reggeAction
101 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K
102 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).hK
103 (D.spacing t • D.probe i) /
104 ‖D.spacing t‖ ^ (2 : ℕ)))
105 l
106 (nhds D.continuumIntegral) :=
107 CanonicalPeriodicFiniteEHDirichletIntegralRefinementData.fullRegge_tendsto_continuumIntegral
108 Nx Ny Nz hx hy hz hLocal D
109
110/-- Explicit reduction: the physical upgrade beyond the flat witness splits into
111edge-stencil local correspondence (already consumed above) and the single
112Riemann-sum target above. -/
113theorem physicalReggeEHUpgrade_reduces_to_manifoldIntegralTarget
114 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
115 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
116 (hLocal : CanonicalPeriodicEdgeStencilLocalCorrespondence Nx Ny Nz hx hy hz)
117 (hIntegral : PhysicalReggeEHManifoldIntegralRemainingTarget Nx Ny Nz hx hy hz) :
118 PhysicalReggeEHManifoldIntegralRemainingTarget Nx Ny Nz hx hy hz := by
119 intro n probe limitWeight continuumIntegral
120 exact hIntegral (n := n) probe limitWeight continuumIntegral
121
122/-- Compared with `Track1BCStructural.regge_eh_continuum_canonical_witness`, the
123physical upgrade replaces the flat zero-zero identity with the finite-probe
124residual theorem above, conditional on edge-stencil local correspondence. -/
125theorem physicalReggeEHUpgrade_beyond_flatStructuralWitness
126 {α : Type*} {l : Filter α}
127 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
128 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
129 (hLocal : CanonicalPeriodicEdgeStencilLocalCorrespondence Nx Ny Nz hx hy hz) :
130 regge_eh_continuum_structural_prop ∧
131 (∃ (r C : ℝ), 0 < r ∧ 0 ≤ C ∧
132 ∀ {n : ℕ}
133 (spacing : α → ℝ)
134 (probe :
135 Fin n →
136 VertexPotential
137 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K)
138 (weight : α → Fin n → ℝ)
139 (limitWeight : Fin n → ℝ),
140 (∀ i : Fin n, Filter.Tendsto (fun t : α => weight t i) l (nhds (limitWeight i))) →
141 Filter.Tendsto spacing l (nhds 0) →
142 (∀ᶠ t : α in l, spacing t ≠ 0) →
143 Filter.Tendsto
144 (fun t : α =>
145 (∑ i : Fin n,
146 weight t i *
147 (reggeAction
148 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K
149 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).hK
150 (spacing t • probe i) /
151 ‖spacing t‖ ^ (2 : ℕ))) -
152 ∑ i : Fin n,
153 limitWeight i *
154 CanonicalPeriodicFiniteEHDirichletLimitAction
155 Nx Ny Nz hx hy hz (probe i))
156 l (nhds 0)) :=
157 ⟨regge_eh_continuum_canonical_witness,
158 physicalReggeEHFiniteProbeResidualTarget Nx Ny Nz hx hy hz hLocal⟩
159
160/-- The reusable finite-probe physical residual conclusion after local
161edge-stencil correspondence has been supplied. -/
162def PhysicalReggeEHFiniteProbeResidualConclusion
163 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
164 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz) : Prop :=
165 ∀ {α : Type*} {l : Filter α},
166 ∃ (r C : ℝ), 0 < r ∧ 0 ≤ C ∧
167 ∀ {n : ℕ}
168 (spacing : α → ℝ)
169 (probe :
170 Fin n →
171 VertexPotential
172 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K)
173 (weight : α → Fin n → ℝ)
174 (limitWeight : Fin n → ℝ),
175 (∀ i : Fin n, Filter.Tendsto (fun t : α => weight t i) l (nhds (limitWeight i))) →
176 Filter.Tendsto spacing l (nhds 0) →
177 (∀ᶠ t : α in l, spacing t ≠ 0) →
178 Filter.Tendsto
179 (fun t : α =>
180 (∑ i : Fin n,
181 weight t i *
182 (reggeAction
183 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K
184 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).hK
185 (spacing t • probe i) /
186 ‖spacing t‖ ^ (2 : ℕ))) -
187 ∑ i : Fin n,
188 limitWeight i *
189 CanonicalPeriodicFiniteEHDirichletLimitAction
190 Nx Ny Nz hx hy hz (probe i))
191 l (nhds 0)
192
193/-- Local correspondence supplies the finite-probe physical residual conclusion. -/
194theorem physicalReggeEHFiniteProbeResidualConclusion_of_localCorrespondence
195 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
196 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
197 (hLocal : CanonicalPeriodicEdgeStencilLocalCorrespondence Nx Ny Nz hx hy hz) :
198 PhysicalReggeEHFiniteProbeResidualConclusion Nx Ny Nz hx hy hz := by
199 intro α l
200 exact physicalReggeEHFiniteProbeResidualTarget Nx Ny Nz hx hy hz hLocal
201
202/-- Fork-B interface: physical finite-probe residual plus the structural
203contracted discrete Bianchi theorem, still keeping the manifold integral target
204outside the package. -/
205structure PhysicalReggeEHBianchiInterface
206 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
207 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
208 (V B : Type) [Fintype B] : Prop where
209 finiteProbeResidual :
210 PhysicalReggeEHFiniteProbeResidualConclusion Nx Ny Nz hx hy hz
211 discreteBianchi :
212 ∀ (R : Geometry.DiscreteBianchi.SchlafliReggeData V B) (v : V),
213 Geometry.DiscreteBianchi.DiscreteBianchiContractedAtVertex R.toReggeData v
214 bianchiIffSchlafli :
215 ∀ (R : Geometry.DiscreteBianchi.ReggeData V B) (v : V),
216 Geometry.DiscreteBianchi.DiscreteBianchiContractedAtVertex R v ↔
217 Geometry.DiscreteBianchi.SchlafliIdentityAtVertex R v
218 bianchiHypothesisSpace :
219 Nonempty (Geometry.DiscreteBianchi.SchlafliReggeData V B)
220
221/-- Local correspondence is enough to build the combined Track `1B-PHY / 1.C`
222interface. The remaining physical manifold upgrade is exactly
223`PhysicalReggeEHManifoldIntegralRemainingTarget`. -/
224theorem physicalReggeEHBianchiInterface_of_localCorrespondence
225 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
226 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
227 (V B : Type) [Fintype B]
228 (hLocal : CanonicalPeriodicEdgeStencilLocalCorrespondence Nx Ny Nz hx hy hz) :
229 PhysicalReggeEHBianchiInterface Nx Ny Nz hx hy hz V B where
230 finiteProbeResidual :=
231 physicalReggeEHFiniteProbeResidualConclusion_of_localCorrespondence
232 Nx Ny Nz hx hy hz hLocal
233 discreteBianchi := Geometry.DiscreteBianchi.discrete_bianchi_contracted_from_schlafli
234 bianchiIffSchlafli := Geometry.DiscreteBianchi.discreteBianchi_eq_schlafli
235 bianchiHypothesisSpace := Geometry.DiscreteBianchi.SchlafliReggeData_inhabited V B
236
237/-! ## Concrete refinement-family target for the manifold EH bridge -/
238
239/-- Concrete per-slice Riemann-sum target for the physical manifold bridge.
240
241For a six-tet volume quadrature slice, the finite EH/Dirichlet limiting
242aggregate is identified with the slice's canonical quadrature integral. This
243is the slice-level instance of the target used by
244`PhysicalReggeEHManifoldIntegralRemainingTarget`, with the probes and weights
245fixed by the periodic Freudenthal tetrahedra and the canonical `cellVolume / 6`
246split. -/
247def PhysicalReggeEHConcreteSliceLimitWeightTarget
248 {α : Type*} {l : Filter α}
249 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) : Prop := by
250 letI : NeZero S.Nx := S.instNx
251 letI : NeZero S.Ny := S.instNy
252 letI : NeZero S.Nz := S.instNz
253 exact
254 CanonicalPeriodicFiniteEHDirichletLimitWeightIntegralTarget
255 S.Nx S.Ny S.Nz S.hx S.hy S.hz
256 (fun τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)) =>
257 S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ))
258 (fun τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)) =>
259 canonicalPeriodicFreudenthalTetVolumeWeight
260 S.Nx S.Ny S.Nz S.data.limitCellVolume
261 (tetFinEquiv S.Nx S.Ny S.Nz τ))
262 S.quadratureIntegral
263
264/-- Every concrete six-tet volume quadrature slice satisfies its slice-level
265limit-weight integral target by definition of the finite quadrature proxy. -/
266theorem physicalReggeEHConcreteSliceLimitWeightTarget_holds
267 {α : Type*} {l : Filter α}
268 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
269 PhysicalReggeEHConcreteSliceLimitWeightTarget S := by
270 letI : NeZero S.Nx := S.instNx
271 letI : NeZero S.Ny := S.instNy
272 letI : NeZero S.Nz := S.instNz
273 simpa [
274 PhysicalReggeEHConcreteSliceLimitWeightTarget,
275 CanonicalPeriodicTetSixTetVolumeQuadratureSlice.quadratureIntegral,
276 CanonicalPeriodicTetGeometricQuadratureRule.continuumIntegral,
277 CanonicalPeriodicTetGeometricQuadratureRule.toFiniteQuadratureRule,
278 canonicalPeriodicTetSixTetVolumeQuadratureRule] using
279 (CanonicalPeriodicTetGeometricQuadratureRule.limitWeightIntegralTarget
280 S.Nx S.Ny S.Nz S.hx S.hy S.hz
281 (canonicalPeriodicTetSixTetVolumeQuadratureRule
282 S.Nx S.Ny S.Nz S.hx S.hy S.hz
283 S.data.limitCellVolume S.data.tetProbe))
284
285/-- Concrete cross-cardinality Riemann-sum target: every slice in a varying
286periodic Freudenthal refinement family carries the per-slice finite
287EH/Dirichlet limit-weight target above. -/
288def PhysicalReggeEHConcreteRefinementFamilySliceTarget
289 {α ρ : Type*} {l : Filter α}
290 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ) : Prop :=
291 ∀ r : ρ, PhysicalReggeEHConcreteSliceLimitWeightTarget (F.slice r)
292
293/-- The concrete slice target holds for every slice of a six-tet volume
294quadrature refinement family. -/
295theorem physicalReggeEHConcreteRefinementFamilySliceTarget_holds
296 {α ρ : Type*} {l : Filter α}
297 (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ) :
298 PhysicalReggeEHConcreteRefinementFamilySliceTarget F :=
299 fun r => physicalReggeEHConcreteSliceLimitWeightTarget_holds (F.slice r)
300
301/-- Product-filter full-Regge-to-EH target for the concrete refinement-family
302path. This is the global Riemann-sum target after the family supplies:
303
3041. cross-cardinality convergence of finite six-tet quadrature proxies, and
3052. a uniform product-filter residual estimate.
306
307It is the product-filter analogue of
308`PhysicalReggeEHManifoldIntegralRemainingTarget`: instead of quantifying over
309arbitrary finite probes and arbitrary continuum integrals, it fixes the
310concrete periodic Freudenthal refinement family and asks for convergence to
311that family's supplied continuum EH integral. -/
312def PhysicalReggeEHConcreteProductFilterTarget
313 {α ρ : Type*} {l : Filter α}
314 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l) : Prop :=
315 Filter.Tendsto
316 (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
317 (α := α) (ρ := ρ) D.family)
318 (D.refinementFilter ×ˢ l : Filter (ρ × α))
319 (nhds D.continuumIntegral)
320
321/-- Product-filter data proves the concrete refinement-family target. -/
322theorem physicalReggeEHConcreteProductFilterTarget_holds
323 {α ρ : Type*} {l : Filter α}
324 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l) :
325 PhysicalReggeEHConcreteProductFilterTarget D :=
326 D.fullReggeProduct_tendsto_continuum
327
328/-- Diagonal form of the concrete product-filter target. Once a diagonal
329schedule into the `(cardinality, within-slice)` product filter is supplied, the
330normalized full-Regge aggregate along that diagonal converges to the same
331continuum EH integral. -/
332def PhysicalReggeEHConcreteDiagonalTarget
333 {α ρ δ : Type*} {l : Filter α} {m : Filter δ}
334 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
335 (diagonal : δ → ρ × α) : Prop :=
336 Filter.Tendsto
337 (fun s : δ =>
338 CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
339 (α := α) (ρ := ρ) D.family (diagonal s))
340 m
341 (nhds D.continuumIntegral)
342
343/-- A diagonal tending into the product filter proves the concrete diagonal
344full-Regge-to-EH target. -/
345theorem physicalReggeEHConcreteDiagonalTarget_holds
346 {α ρ δ : Type*} {l : Filter α} {m : Filter δ}
347 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
348 (diagonal : δ → ρ × α)
349 (hDiagonal :
350 Filter.Tendsto diagonal m (D.refinementFilter ×ˢ l : Filter (ρ × α))) :
351 PhysicalReggeEHConcreteDiagonalTarget (m := m) D diagonal :=
352 D.fullReggeDiagonal_tendsto_continuum diagonal hDiagonal
353
354/-- Agent-B interface package for Track 1.B-PHY. The package deliberately keeps
355the two hard geometric inputs explicit: cross-cardinality quadrature convergence
356and product-filter uniform residual control. Given those inputs, the physical
357Regge/EH continuum target is available both on the product filter and along any
358admissible diagonal schedule. -/
359structure PhysicalReggeEHConcreteRefinementFamilyTargetCert
360 {α ρ : Type*} (l : Filter α) where
361 data :
362 CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l
363 slice_targets :
364 PhysicalReggeEHConcreteRefinementFamilySliceTarget data.family
365 product_target :
366 PhysicalReggeEHConcreteProductFilterTarget data
367
368/-- Any concrete product-filter data gives the Agent-B certificate. -/
369def PhysicalReggeEHConcreteRefinementFamilyTargetCert.ofProductFilterData
370 {α ρ : Type*} {l : Filter α}
371 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l) :
372 PhysicalReggeEHConcreteRefinementFamilyTargetCert (α := α) (ρ := ρ) l where
373 data := D
374 slice_targets := physicalReggeEHConcreteRefinementFamilySliceTarget_holds D.family
375 product_target := physicalReggeEHConcreteProductFilterTarget_holds D
376
377/-- Session 551 projection: the concrete refinement-family certificate keeps the
378supplied product-filter data as its data field. -/
379theorem PhysicalReggeEHConcreteRefinementFamilyTargetCert.ofProductFilterData_data
380 {α ρ : Type*} {l : Filter α}
381 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l) :
382 (PhysicalReggeEHConcreteRefinementFamilyTargetCert.ofProductFilterData D).data = D := rfl
383
384/-- Session 551 projection: the concrete refinement-family certificate exposes
385all slice-level finite EH/Dirichlet limit-weight targets. -/
386theorem PhysicalReggeEHConcreteRefinementFamilyTargetCert.ofProductFilterData_sliceTargets
387 {α ρ : Type*} {l : Filter α}
388 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l) :
389 PhysicalReggeEHConcreteRefinementFamilySliceTarget
390 (PhysicalReggeEHConcreteRefinementFamilyTargetCert.ofProductFilterData D).data.family :=
391 (PhysicalReggeEHConcreteRefinementFamilyTargetCert.ofProductFilterData D).slice_targets
392
393/-- Session 551 projection: the concrete refinement-family certificate exposes
394the product-filter full-Regge-to-EH continuum target. -/
395theorem PhysicalReggeEHConcreteRefinementFamilyTargetCert.ofProductFilterData_productTarget
396 {α ρ : Type*} {l : Filter α}
397 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l) :
398 PhysicalReggeEHConcreteProductFilterTarget
399 (PhysicalReggeEHConcreteRefinementFamilyTargetCert.ofProductFilterData D).data :=
400 (PhysicalReggeEHConcreteRefinementFamilyTargetCert.ofProductFilterData D).product_target
401
402/-- Session 551 audit count for the three concrete refinement-family certificate
403projections: data, slice targets, and product target. -/
404def physicalReggeEHConcreteRefinementFamilyTargetCertProjectionCount : ℕ := 3
405
406theorem physicalReggeEHConcreteRefinementFamilyTargetCertProjectionCount_eq_three :
407 physicalReggeEHConcreteRefinementFamilyTargetCertProjectionCount = 3 := rfl
408
409/-- One-statement interface for the concrete refinement-family target. It
410exposes exactly what remains for the true `1B-PHY` path: provide
411`CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData`; the full-Regge
412product-filter continuum limit and all per-slice finite EH/Dirichlet
413limit-weight targets then follow. -/
414theorem physicalReggeEH_concrete_refinement_family_target_one_statement
415 {α ρ : Type*} {l : Filter α}
416 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l) :
417 PhysicalReggeEHConcreteRefinementFamilySliceTarget D.family ∧
418 PhysicalReggeEHConcreteProductFilterTarget D ∧
419 Nonempty (PhysicalReggeEHConcreteRefinementFamilyTargetCert (α := α) (ρ := ρ) l) :=
420 ⟨physicalReggeEHConcreteRefinementFamilySliceTarget_holds D.family,
421 physicalReggeEHConcreteProductFilterTarget_holds D,
422 ⟨PhysicalReggeEHConcreteRefinementFamilyTargetCert.ofProductFilterData D⟩⟩
423
424/-- Session 553 projection: the concrete refinement-family one-statement theorem
425exposes all slice-level finite EH/Dirichlet limit-weight targets. -/
426theorem physicalReggeEH_concrete_refinement_family_target_one_statement_sliceTargets
427 {α ρ : Type*} {l : Filter α}
428 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l) :
429 PhysicalReggeEHConcreteRefinementFamilySliceTarget D.family :=
430 (physicalReggeEH_concrete_refinement_family_target_one_statement D).1
431
432/-- Session 553 projection: the concrete refinement-family one-statement theorem
433exposes the product-filter full-Regge-to-EH continuum target. -/
434theorem physicalReggeEH_concrete_refinement_family_target_one_statement_productTarget
435 {α ρ : Type*} {l : Filter α}
436 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l) :
437 PhysicalReggeEHConcreteProductFilterTarget D :=
438 (physicalReggeEH_concrete_refinement_family_target_one_statement D).2.1
439
440/-- Session 553 projection: the concrete refinement-family one-statement theorem
441exposes an inhabited audit certificate. -/
442theorem physicalReggeEH_concrete_refinement_family_target_one_statement_certInhabited
443 {α ρ : Type*} {l : Filter α}
444 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l) :
445 Nonempty (PhysicalReggeEHConcreteRefinementFamilyTargetCert (α := α) (ρ := ρ) l) :=
446 (physicalReggeEH_concrete_refinement_family_target_one_statement D).2.2
447
448/-- Session 553 audit count for the three concrete refinement-family
449one-statement projections: slice target, product target, and certificate
450inhabitation. -/
451def physicalReggeEHConcreteRefinementFamilyOneStatementProjectionCount : ℕ := 3
452
453theorem physicalReggeEHConcreteRefinementFamilyOneStatementProjectionCount_eq_three :
454 physicalReggeEHConcreteRefinementFamilyOneStatementProjectionCount = 3 := rfl
455
456/-- Session 586 varying-cardinality product-filter route. A staged
457cross-cardinality quadrature package plus a global residual envelope gives true
458product-filter data for arbitrary cardinality index `ρ`, then the concrete
459physical Regge/EH slice target, product target, and audit certificate follow. -/
460theorem physicalReggeEH_concrete_varying_cardinality_product_filter_data_one_statement
461 {α ρ : Type*} {l : Filter α}
462 {D : CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityData
463 (α := α) (ρ := ρ) l}
464 (E : CanonicalPeriodicTetSixTetVolumeQuadratureGlobalResidualEnvelopeData D) :
465 PhysicalReggeEHConcreteRefinementFamilySliceTarget E.toProductFilterData.family ∧
466 PhysicalReggeEHConcreteProductFilterTarget E.toProductFilterData ∧
467 Nonempty (PhysicalReggeEHConcreteRefinementFamilyTargetCert (α := α) (ρ := ρ) l) :=
468 physicalReggeEH_concrete_refinement_family_target_one_statement E.toProductFilterData
469
470theorem physicalReggeEH_concrete_varying_cardinality_product_filter_data_one_statement_sliceTarget
471 {α ρ : Type*} {l : Filter α}
472 {D : CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityData
473 (α := α) (ρ := ρ) l}
474 (E : CanonicalPeriodicTetSixTetVolumeQuadratureGlobalResidualEnvelopeData D) :
475 PhysicalReggeEHConcreteRefinementFamilySliceTarget E.toProductFilterData.family :=
476 (physicalReggeEH_concrete_varying_cardinality_product_filter_data_one_statement E).1
477
478theorem physicalReggeEH_concrete_varying_cardinality_product_filter_data_one_statement_productTarget
479 {α ρ : Type*} {l : Filter α}
480 {D : CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityData
481 (α := α) (ρ := ρ) l}
482 (E : CanonicalPeriodicTetSixTetVolumeQuadratureGlobalResidualEnvelopeData D) :
483 PhysicalReggeEHConcreteProductFilterTarget E.toProductFilterData :=
484 (physicalReggeEH_concrete_varying_cardinality_product_filter_data_one_statement E).2.1
485
486theorem physicalReggeEH_concrete_varying_cardinality_product_filter_data_one_statement_certInhabited
487 {α ρ : Type*} {l : Filter α}
488 {D : CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityData
489 (α := α) (ρ := ρ) l}
490 (E : CanonicalPeriodicTetSixTetVolumeQuadratureGlobalResidualEnvelopeData D) :
491 Nonempty (PhysicalReggeEHConcreteRefinementFamilyTargetCert (α := α) (ρ := ρ) l) :=
492 (physicalReggeEH_concrete_varying_cardinality_product_filter_data_one_statement E).2.2
493
494/-- Session 586 audit count for the varying-cardinality product-filter
495one-statement projections: slice target, product target, and certificate
496inhabitation. -/
497def physicalReggeEHConcreteVaryingCardinalityProductFilterOneStatementProjectionCount :
498 ℕ := 3
499
500theorem physicalReggeEHConcreteVaryingCardinalityProductFilterOneStatementProjectionCount_eq_three :
501 physicalReggeEHConcreteVaryingCardinalityProductFilterOneStatementProjectionCount = 3 := rfl
502
503/-- Session 587 finite product residual estimate. This is the concrete
504full-Regge-to-quadrature bound required before the product-filter convergence
505argument can run. -/
506def PhysicalReggeEHFiniteProductResidualEstimateTarget
507 {α ρ : Type*} {l : Filter α}
508 {D : CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityData
509 (α := α) (ρ := ρ) l}
510 (E : CanonicalPeriodicTetSixTetVolumeQuadratureGlobalResidualEnvelopeData D) : Prop :=
511 ∀ (r : ρ) (t : α),
512 |CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate D.family (r, t) -
513 CanonicalPeriodicTetSixTetVolumeQuadratureProductQuadratureIntegral D.family (r, t)| ≤
514 E.envelope t
515
516theorem physicalReggeEHFiniteProductResidualEstimateTarget_holds
517 {α ρ : Type*} {l : Filter α}
518 {D : CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityData
519 (α := α) (ρ := ρ) l}
520 (E : CanonicalPeriodicTetSixTetVolumeQuadratureGlobalResidualEnvelopeData D) :
521 PhysicalReggeEHFiniteProductResidualEstimateTarget E :=
522 E.global_residual_bound
523
524/-- Session 587 audit count: the global residual envelope exposes one finite
525product residual estimate target. -/
526def physicalReggeEHFiniteProductResidualEstimateProjectionCount : ℕ := 1
527
528theorem physicalReggeEHFiniteProductResidualEstimateProjectionCount_eq_one :
529 physicalReggeEHFiniteProductResidualEstimateProjectionCount = 1 := rfl
530
531/-- Session 588 continuum-normalization target. This is the raw
532cross-cardinality `Tendsto` statement obtained after the finite product
533residual estimate is combined with the staged quadrature limit. -/
534def PhysicalReggeEHContinuumNormalizationFromResidualTarget
535 {α ρ : Type*} {l : Filter α}
536 {D : CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityData
537 (α := α) (ρ := ρ) l}
538 (E : CanonicalPeriodicTetSixTetVolumeQuadratureGlobalResidualEnvelopeData D) : Prop :=
539 PhysicalReggeEHFiniteProductResidualEstimateTarget E →
540 Filter.Tendsto
541 (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
542 (α := α) (ρ := ρ) D.family)
543 (D.refinementFilter ×ˢ l : Filter (ρ × α))
544 (nhds D.continuumIntegral)
545
546theorem physicalReggeEHContinuumNormalizationFromResidualTarget_holds
547 {α ρ : Type*} {l : Filter α}
548 {D : CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityData
549 (α := α) (ρ := ρ) l}
550 (E : CanonicalPeriodicTetSixTetVolumeQuadratureGlobalResidualEnvelopeData D) :
551 PhysicalReggeEHContinuumNormalizationFromResidualTarget E := by
552 intro hResidual
553 exact
554 D.fullReggeProduct_tendsto_continuum_of_forallSndResidualEnvelope
555 E.envelope E.envelope_tendsto_zero hResidual
556
557/-- Session 588 projection: applying the finite residual estimate gives the
558continuum normalization statement itself. -/
559theorem physicalReggeEHContinuumNormalizationFromResidualTarget_apply
560 {α ρ : Type*} {l : Filter α}
561 {D : CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityData
562 (α := α) (ρ := ρ) l}
563 (E : CanonicalPeriodicTetSixTetVolumeQuadratureGlobalResidualEnvelopeData D) :
564 Filter.Tendsto
565 (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
566 (α := α) (ρ := ρ) D.family)
567 (D.refinementFilter ×ˢ l : Filter (ρ × α))
568 (nhds D.continuumIntegral) :=
569 physicalReggeEHContinuumNormalizationFromResidualTarget_holds E
570 (physicalReggeEHFiniteProductResidualEstimateTarget_holds E)
571
572/-- Session 588 audit count: one normalization function and one applied
573continuum theorem. -/
574def physicalReggeEHContinuumNormalizationFromResidualProjectionCount : ℕ := 2
575
576theorem physicalReggeEHContinuumNormalizationFromResidualProjectionCount_eq_two :
577 physicalReggeEHContinuumNormalizationFromResidualProjectionCount = 2 := rfl
578
579/-! ## Physical D2 master-hypothesis witness -/
580
581/-- Physical replacement for the flat `0 = 0` structural Regge/EH clause:
582for a concrete periodic Freudenthal product-filter refinement package, the
583normalized full nonlinear Regge aggregate tends to the supplied continuum
584Einstein-Hilbert/Dirichlet integral. -/
585def physicalReggeEHContinuumMasterProp
586 {α ρ : Type*} {l : Filter α}
587 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l) :
588 Prop :=
589 PhysicalReggeEHConcreteProductFilterTarget D
590
591theorem physicalReggeEHContinuumMasterProp_holds
592 {α ρ : Type*} {l : Filter α}
593 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l) :
594 physicalReggeEHContinuumMasterProp D :=
595 physicalReggeEHConcreteProductFilterTarget_holds D
596
597/-- Physical Track 1.C master clause: Schläfli-satisfying Regge data obey the
598contracted discrete Bianchi identity at every vertex. -/
599def physicalSchlafliBianchiMasterProp (V B : Type) [Fintype B] : Prop :=
600 ∀ (R : Geometry.DiscreteBianchi.SchlafliReggeData V B) (v : V),
601 Geometry.DiscreteBianchi.DiscreteBianchiContractedAtVertex R.toReggeData v
602
603theorem physicalSchlafliBianchiMasterProp_holds (V B : Type) [Fintype B] :
604 physicalSchlafliBianchiMasterProp V B :=
605 Geometry.DiscreteBianchi.discrete_bianchi_contracted_from_schlafli
606
607/-- Master-theorem D2 hypothesis input whose Regge/EH clause is the physical
608product-filter `Tendsto` target, not the older flat-substrate identity. -/
609def physicalReggeEHContinuumAndBianchiWitness
610 {α ρ : Type*} {l : Filter α}
611 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
612 (V B : Type) [Fintype B] :
613 Gravity.MasterTheorem.RegEHContinuumAndBianchi where
614 regge_to_einstein_hilbert_continuum := physicalReggeEHContinuumMasterProp D
615 regge_holds := physicalReggeEHContinuumMasterProp_holds D
616 discrete_bianchi_contracted := physicalSchlafliBianchiMasterProp V B
617 bianchi_holds := physicalSchlafliBianchiMasterProp_holds V B
618
619/-- Session 549 projection: the physical D2 witness installs the product-filter
620Regge/EH continuum clause, not the older flat structural clause. -/
621theorem physicalReggeEHContinuumAndBianchiWitness_reggeClause
622 {α ρ : Type*} {l : Filter α}
623 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
624 (V B : Type) [Fintype B] :
625 (physicalReggeEHContinuumAndBianchiWitness D V B).regge_to_einstein_hilbert_continuum =
626 physicalReggeEHContinuumMasterProp D := rfl
627
628/-- Session 549 projection: the physical D2 witness carries the proof of the
629product-filter Regge/EH continuum clause. -/
630theorem physicalReggeEHContinuumAndBianchiWitness_reggeHolds
631 {α ρ : Type*} {l : Filter α}
632 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
633 (V B : Type) [Fintype B] :
634 (physicalReggeEHContinuumAndBianchiWitness D V B).regge_to_einstein_hilbert_continuum :=
635 (physicalReggeEHContinuumAndBianchiWitness D V B).regge_holds
636
637/-- Session 549 projection: the physical D2 witness installs the Schläfli-form
638contracted Bianchi clause. -/
639theorem physicalReggeEHContinuumAndBianchiWitness_bianchiClause
640 {α ρ : Type*} {l : Filter α}
641 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
642 (V B : Type) [Fintype B] :
643 (physicalReggeEHContinuumAndBianchiWitness D V B).discrete_bianchi_contracted =
644 physicalSchlafliBianchiMasterProp V B := rfl
645
646/-- Session 549 projection: the physical D2 witness carries the proof of the
647Schläfli-form contracted Bianchi clause. -/
648theorem physicalReggeEHContinuumAndBianchiWitness_bianchiHolds
649 {α ρ : Type*} {l : Filter α}
650 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
651 (V B : Type) [Fintype B] :
652 (physicalReggeEHContinuumAndBianchiWitness D V B).discrete_bianchi_contracted :=
653 (physicalReggeEHContinuumAndBianchiWitness D V B).bianchi_holds
654
655/-- Audit certificate showing exactly what clauses the physical D2 master
656witness installs. -/
657structure PhysicalReggeEHD2MasterWitnessCert
658 {α ρ : Type*} {l : Filter α}
659 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
660 (V B : Type) [Fintype B] where
661 witness : Gravity.MasterTheorem.RegEHContinuumAndBianchi
662 regge_clause_is_physical :
663 witness.regge_to_einstein_hilbert_continuum =
664 physicalReggeEHContinuumMasterProp D
665 bianchi_clause_is_schlafli :
666 witness.discrete_bianchi_contracted =
667 physicalSchlafliBianchiMasterProp V B
668
669def physicalReggeEHD2MasterWitnessCert
670 {α ρ : Type*} {l : Filter α}
671 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
672 (V B : Type) [Fintype B] :
673 PhysicalReggeEHD2MasterWitnessCert D V B where
674 witness := physicalReggeEHContinuumAndBianchiWitness D V B
675 regge_clause_is_physical := rfl
676 bianchi_clause_is_schlafli := rfl
677
678/-- Session 549 projection: the certificate's witness is the physical D2 witness
679constructed from the supplied product-filter data. -/
680theorem physicalReggeEHD2MasterWitnessCert_witness_eq
681 {α ρ : Type*} {l : Filter α}
682 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
683 (V B : Type) [Fintype B] :
684 (physicalReggeEHD2MasterWitnessCert D V B).witness =
685 physicalReggeEHContinuumAndBianchiWitness D V B := rfl
686
687/-- Session 549 projection: the certificate exposes the Regge/EH clause identity
688without opening the certificate record at the call site. -/
689theorem physicalReggeEHD2MasterWitnessCert_reggeClause
690 {α ρ : Type*} {l : Filter α}
691 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
692 (V B : Type) [Fintype B] :
693 (physicalReggeEHD2MasterWitnessCert D V B).witness.regge_to_einstein_hilbert_continuum =
694 physicalReggeEHContinuumMasterProp D :=
695 (physicalReggeEHD2MasterWitnessCert D V B).regge_clause_is_physical
696
697/-- Session 549 projection: the certificate exposes the Bianchi clause identity
698without opening the certificate record at the call site. -/
699theorem physicalReggeEHD2MasterWitnessCert_bianchiClause
700 {α ρ : Type*} {l : Filter α}
701 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
702 (V B : Type) [Fintype B] :
703 (physicalReggeEHD2MasterWitnessCert D V B).witness.discrete_bianchi_contracted =
704 physicalSchlafliBianchiMasterProp V B :=
705 (physicalReggeEHD2MasterWitnessCert D V B).bianchi_clause_is_schlafli
706
707/-- Session 549 audit count for the seven physical D2 master-witness projection
708theorems: four witness-field projections plus three certificate projections. -/
709def physicalReggeEHD2MasterWitnessProjectionCount : ℕ := 7
710
711theorem physicalReggeEHD2MasterWitnessProjectionCount_eq_seven :
712 physicalReggeEHD2MasterWitnessProjectionCount = 7 := rfl
713
714theorem physicalReggeEHD2MasterWitnessCert_inhabited
715 {α ρ : Type*} {l : Filter α}
716 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
717 (V B : Type) [Fintype B] :
718 Nonempty (PhysicalReggeEHD2MasterWitnessCert D V B) :=
719 ⟨physicalReggeEHD2MasterWitnessCert D V B⟩
720
721/-- One-statement form of the physical D2 master-hypothesis replacement. -/
722theorem physicalReggeEHD2_master_witness_one_statement
723 {α ρ : Type*} {l : Filter α}
724 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
725 (V B : Type) [Fintype B] :
726 (Nonempty Gravity.MasterTheorem.RegEHContinuumAndBianchi) ∧
727 physicalReggeEHContinuumMasterProp D ∧
728 physicalSchlafliBianchiMasterProp V B :=
729 ⟨⟨physicalReggeEHContinuumAndBianchiWitness D V B⟩,
730 physicalReggeEHContinuumMasterProp_holds D,
731 physicalSchlafliBianchiMasterProp_holds V B⟩
732
733/-- Session 554 projection: the physical D2 master-witness one-statement theorem
734exposes an inhabited master-theorem D2 witness. -/
735theorem physicalReggeEHD2_master_witness_one_statement_witnessInhabited
736 {α ρ : Type*} {l : Filter α}
737 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
738 (V B : Type) [Fintype B] :
739 Nonempty Gravity.MasterTheorem.RegEHContinuumAndBianchi :=
740 (physicalReggeEHD2_master_witness_one_statement D V B).1
741
742/-- Session 554 projection: the physical D2 master-witness one-statement theorem
743exposes the product-filter Regge/EH continuum master clause. -/
744theorem physicalReggeEHD2_master_witness_one_statement_reggeEH
745 {α ρ : Type*} {l : Filter α}
746 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
747 (V B : Type) [Fintype B] :
748 physicalReggeEHContinuumMasterProp D :=
749 (physicalReggeEHD2_master_witness_one_statement D V B).2.1
750
751/-- Session 554 projection: the physical D2 master-witness one-statement theorem
752exposes the Schläfli-form contracted Bianchi master clause. -/
753theorem physicalReggeEHD2_master_witness_one_statement_bianchi
754 {α ρ : Type*} {l : Filter α}
755 (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
756 (V B : Type) [Fintype B] :
757 physicalSchlafliBianchiMasterProp V B :=
758 (physicalReggeEHD2_master_witness_one_statement D V B).2.2
759
760/-- Session 554 audit count for the three physical D2 master-witness
761one-statement projections: witness inhabitation, Regge/EH, and Bianchi. -/
762def physicalReggeEHD2MasterWitnessOneStatementProjectionCount : ℕ := 3
763
764theorem physicalReggeEHD2MasterWitnessOneStatementProjectionCount_eq_three :
765 physicalReggeEHD2MasterWitnessOneStatementProjectionCount = 3 := rfl
766
767/-- The single-slice product-filter data supplies the concrete physical
768Regge/EH target immediately. This is the first actual
769`CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData` instance in the
7701B-PHY path: the cardinality filter is trivial (`PUnit`), while the
771within-slice refinement is the slice's existing mesh refinement. -/
772theorem physicalReggeEH_concrete_single_slice_product_filter_data_one_statement
773 {α : Type*} {l : Filter α}
774 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l)
775 (refinementFilter : Filter PUnit) :
776 PhysicalReggeEHConcreteRefinementFamilySliceTarget
777 (S.toSingleSliceProductFilterData refinementFilter).family ∧
778 PhysicalReggeEHConcreteProductFilterTarget
779 (S.toSingleSliceProductFilterData refinementFilter) :=
780 ⟨physicalReggeEHConcreteRefinementFamilySliceTarget_holds
781 (S.toSingleSliceProductFilterData refinementFilter).family,
782 physicalReggeEHConcreteProductFilterTarget_holds
783 (S.toSingleSliceProductFilterData refinementFilter)⟩
784
785/-- Session 556 projection: the single-slice product-filter one-statement theorem
786exposes the concrete refinement-family slice target. -/
787theorem physicalReggeEH_concrete_single_slice_product_filter_data_one_statement_sliceTarget
788 {α : Type*} {l : Filter α}
789 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l)
790 (refinementFilter : Filter PUnit) :
791 PhysicalReggeEHConcreteRefinementFamilySliceTarget
792 (S.toSingleSliceProductFilterData refinementFilter).family :=
793 (physicalReggeEH_concrete_single_slice_product_filter_data_one_statement
794 S refinementFilter).1
795
796/-- Session 556 projection: the single-slice product-filter one-statement theorem
797exposes the concrete product-filter Regge/EH target. -/
798theorem physicalReggeEH_concrete_single_slice_product_filter_data_one_statement_productTarget
799 {α : Type*} {l : Filter α}
800 (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l)
801 (refinementFilter : Filter PUnit) :
802 PhysicalReggeEHConcreteProductFilterTarget
803 (S.toSingleSliceProductFilterData refinementFilter) :=
804 (physicalReggeEH_concrete_single_slice_product_filter_data_one_statement
805 S refinementFilter).2
806
807/-- Session 556 audit count for the two single-slice product-filter
808one-statement projections: slice target and product target. -/
809def physicalReggeEHConcreteSingleSliceProductFilterOneStatementProjectionCount : ℕ := 2
810
811theorem physicalReggeEHConcreteSingleSliceProductFilterOneStatementProjectionCount_eq_two :
812 physicalReggeEHConcreteSingleSliceProductFilterOneStatementProjectionCount = 2 := rfl
813
814end
815
816end Track1BCPhysicalResidual
817end Gravity
818end IndisputableMonolith
819