IndisputableMonolith.Gravity.Analysis.ReggeTTAlgebraicCloser
IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean · 441 lines · 26 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumLimit
2import IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridge
3
4/-!
5# Regge TT algebraic closer: the C8 closed form `(1/2)·xᵀ·adj(E)·x` and the
6# TT isotropy value `-(1/4)`
7
8QG full-theory campaign, Paper C / Pillar 1, production stage C-DAG3 of the
9panel-locked D-dag order (`ReggeTTBlochAssembly → ReggeTTContinuumLimit →
10ReggeTTAlgebraicCloser → ReggeTTContinuumCloser`). This is the SOLE
11production importer of the committed algebraic certificate spike (through
12the Gate B bridge chain); no other production stage may import it.
13
14## What this module proves (all THEOREM)
15
16* `continuumMoment_eq_half_adjugate` — **the C8 closed form as a kernel
17 equation**: for every SYMMETRIC polarization matrix `E` and every real
18 direction `x`, the continuum-limit bucket moment fold of the production
19 chain (the exact limit object of P1.1a,
20 `reggeTTMoment rawCosineSupport (rawPhaseQuadratic x)
21 (rawBucketAmplitude E)`) equals `(1/2) · xᵀ · adj(E) · x`, with
22 `Matrix.adjugate` the actual Mathlib adjugate. Route: the kernel
23 identification of the production-chain fold with the Gate B bridge fold
24 (same geometry-derived tables), the proved bridge equality
25 `rawMoment_eq_committedSpikeLHS`, the committed spike block collapses
26 `tetBlock*_eq` (block DATA only; the spike's own TT certificate
27 `tt_continuum_certificate` is never invoked), and one
28 `linear_combination` certificate over the three symmetry generators.
29* `adjugateQuadraticForm_tt` — the TT adjugate step: for symmetric,
30 traceless, `x`-transverse `E`, `xᵀ·adj(E)·x = -(1/2)·|x|²·⟨E,E⟩`.
31 This is the kernel form of the eigenvalue argument (on the TT variety
32 `x` is a null eigenvector of `E`, so `adj(E)x = λ₁λ₂x` with
33 `λ₁ + λ₂ = 0`), discharged as an explicit cofactor certificate over the
34 seven TT generators via `linear_combination`.
35* `reggeTTMoment_tt_value` — **P1.1b, the isotropy value**: for every
36 nonzero integer mode `m` and every TT polarization
37 (`IsTTPolarization`), the P1.1a limit moment at the normalized real
38 direction equals exactly `reggeTTContinuumCoefficient = -(1/4)`.
39* `canonicalFiniteH_div_momentumNormSq_tendsto_isotropy` — P1.1a + P1.1b
40 composed: the normalized finite reduced symbol converges to `-(1/4)`
41 for every nonzero mode and TT polarization.
42
43## Disclosures (binding)
44
45* SYMMETRY SCOPE. The closed form `(1/2)·xᵀ·adj(E)·x` holds under the
46 three matrix-symmetry hypotheses and NOT identically in all nine free
47 entries: the free-entry difference is the exact rotational square
48 `-(1/8)·(E₀₁x₂ − E₀₂x₁ − E₁₀x₂ + E₁₂x₀ + E₂₀x₁ − E₂₁x₀)²`, which
49 vanishes on symmetric `E`. This matches the C8 certificate's own
50 statement ("identically for every symmetric E").
51* ALIASING NON-REPAIR. The finite assembly identity feeding P1.1a holds
52 only at non-aliased side lengths (`∃ i, ¬ N ∣ 2·mᵢ`); at the finitely
53 many aliased small `N` the finite reduced symbol is NOT identified with
54 the bucket fold and no repair is attempted. The production chain
55 consumes the identity through the eventual-filter form, which is all
56 the continuum limit needs. Unrepaired and disclosed.
57* ANSWER KEY. The exact C8 contraction
58 (`state/qg_full_theory/isotropy_contraction/isotropy_certificate.py`)
59 is the convention anchor for both `linear_combination` certificates;
60 the Lean proofs stand independently of it (the kernel re-verifies every
61 identity from the committed block data and Mathlib's adjugate).
62
63No `sorry`, no `admit`, no new axioms, no `native_decide`, no `: True` or
64`Nonempty`-only headline in this file. Everything here is finite algebra;
65expected axiom footprint of every theorem is the standard trio
66`[propext, Classical.choice, Quot.sound]`. Receipts at end of file.
67-/
68
69namespace IndisputableMonolith
70namespace Gravity
71namespace Analysis
72namespace ReggeTTAlgebraicCloser
73
74open ReggeTTSymbolPreflight
75open ReggeTTBlochInterfaceAudit
76
77noncomputable section
78
79/-! ## §1. Kernel identification of the production fold with the bridge fold
80
81The production chain (`ReggeTTBlochAssembly` / `ReggeTTContinuumLimit`)
82derives its bucket tables from the periodic geometry; the Gate B bridge
83(`ReggeTTGateBBridge`) uses the literal core tables, grounded there against
84the same geometry. These lemmas identify the two folds object by object,
85so the bridge equality can be consumed by the production limit.
86
87PROVENANCE (critic-requested disclosure): the two table families are NOT
88co-seeded from one transcription. The assembly side is DERIVED
89(`slotBaseBit`/`slotDispBit` through `cubeVertexBit ∘ cubeEdgeBase ∘
90localEdgeOf` on the actual Freudenthal cube triangulation); the core side
91is a literal table that the bridge independently GROUNDS against the same
92geometric objects (`edgeMidpointPhase_grounded`, `coreWeight_eq_raw`,
93`corePolEdgeCoeff_eq`, `slotDispCore_eq`). The 216-case kernel equality
94below is therefore a genuine cross-check of derivation against grounded
95transcription, not a comparison of one source with itself. -/
96
97/-- The geometry-derived doubled-midpoint table of the production assembly
98equals the literal core table of the Gate B bridge, entry by entry. -/
99theorem slotMidTwice_eq_core (t f : Fin 6) (i : Fin 3) :
100 ReggeTTBlochAssembly.slotMidTwice t f i =
101 ReggeTTGateBBridgeCore.slotMidTwice t f i := by
102 fin_cases t <;> fin_cases f <;> fin_cases i <;> rfl
103
104/-- The production bucket key map equals the bridge bucket key map. -/
105theorem bucketKeyOf_eq :
106 ReggeTTBlochAssembly.bucketKeyOf = ReggeTTGateBBridge.bucketKeyOf := by
107 funext p
108 unfold ReggeTTBlochAssembly.bucketKeyOf ReggeTTGateBBridge.bucketKeyOf
109 congr 1
110 funext i
111 rw [slotMidTwice_eq_core, slotMidTwice_eq_core]
112
113/-- The production cosine support is the bridge moment support. -/
114theorem rawCosineSupport_eq_rawMomentSupport :
115 ReggeTTBlochAssembly.rawCosineSupport =
116 ReggeTTGateBBridge.rawMomentSupport := by
117 unfold ReggeTTBlochAssembly.rawCosineSupport
118 ReggeTTGateBBridge.rawMomentSupport
119 rw [bucketKeyOf_eq]
120
121/-- The signed raw triple weights coincide (both are
122`-(J_fg/(2√a*_f))·c_{d(t,f)}·c_{d(t,g)}` over the same kernel objects). -/
123theorem rawTripleWeight_eq :
124 ReggeTTBlochAssembly.rawTripleWeight =
125 ReggeTTGateBBridge.rawTripleWeight := rfl
126
127/-- The bucket-fiber-aggregated amplitudes coincide. -/
128theorem rawBucketAmplitude_eq (E : Fin 3 → Fin 3 → ℝ) :
129 ReggeTTBlochAssembly.rawBucketAmplitude E =
130 ReggeTTGateBBridge.rawBucketAmplitude E := by
131 funext b
132 unfold ReggeTTBlochAssembly.rawBucketAmplitude
133 ReggeTTGateBBridge.rawBucketAmplitude
134 rw [bucketKeyOf_eq, rawTripleWeight_eq]
135
136/-- The midpoint phase quadratics coincide. -/
137theorem rawPhaseQuadratic_eq (x : Fin 3 → ℝ) :
138 ReggeTTContinuumLimit.rawPhaseQuadratic x =
139 ReggeTTGateBBridge.rawPhaseQuadratic x := rfl
140
141/-- The production continuum moment fold IS the Gate B bridge moment fold. -/
142theorem continuumMoment_eq_bridgeMoment (E : Fin 3 → Fin 3 → ℝ)
143 (x : Fin 3 → ℝ) :
144 reggeTTMoment ReggeTTBlochAssembly.rawCosineSupport
145 (ReggeTTContinuumLimit.rawPhaseQuadratic x)
146 (ReggeTTBlochAssembly.rawBucketAmplitude E) =
147 reggeTTMoment ReggeTTGateBBridge.rawMomentSupport
148 (ReggeTTGateBBridge.rawPhaseQuadratic x)
149 (ReggeTTGateBBridge.rawBucketAmplitude E) := by
150 rw [rawCosineSupport_eq_rawMomentSupport, rawBucketAmplitude_eq,
151 rawPhaseQuadratic_eq]
152
153/-! ## §2. The adjugate quadratic form and its explicit entries -/
154
155/-- The C8 closed-form object: `xᵀ · adj(E) · x` with `Matrix.adjugate`
156the actual Mathlib adjugate of the polarization matrix. -/
157def adjugateQuadraticForm (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ) : ℝ :=
158 ∑ i : Fin 3, ∑ j : Fin 3,
159 x i * Matrix.adjugate (Matrix.of E) i j * x j
160
161private theorem adjugate00 (E : Fin 3 → Fin 3 → ℝ) :
162 Matrix.adjugate (Matrix.of E) 0 0 = E 1 1 * E 2 2 - E 1 2 * E 2 1 := by
163 rw [Matrix.adjugate_fin_three]; rfl
164
165private theorem adjugate01 (E : Fin 3 → Fin 3 → ℝ) :
166 Matrix.adjugate (Matrix.of E) 0 1 = -(E 0 1 * E 2 2) + E 0 2 * E 2 1 := by
167 rw [Matrix.adjugate_fin_three]; rfl
168
169private theorem adjugate02 (E : Fin 3 → Fin 3 → ℝ) :
170 Matrix.adjugate (Matrix.of E) 0 2 = E 0 1 * E 1 2 - E 0 2 * E 1 1 := by
171 rw [Matrix.adjugate_fin_three]; rfl
172
173private theorem adjugate10 (E : Fin 3 → Fin 3 → ℝ) :
174 Matrix.adjugate (Matrix.of E) 1 0 = -(E 1 0 * E 2 2) + E 1 2 * E 2 0 := by
175 rw [Matrix.adjugate_fin_three]; rfl
176
177private theorem adjugate11 (E : Fin 3 → Fin 3 → ℝ) :
178 Matrix.adjugate (Matrix.of E) 1 1 = E 0 0 * E 2 2 - E 0 2 * E 2 0 := by
179 rw [Matrix.adjugate_fin_three]; rfl
180
181private theorem adjugate12 (E : Fin 3 → Fin 3 → ℝ) :
182 Matrix.adjugate (Matrix.of E) 1 2 = -(E 0 0 * E 1 2) + E 0 2 * E 1 0 := by
183 rw [Matrix.adjugate_fin_three]; rfl
184
185private theorem adjugate20 (E : Fin 3 → Fin 3 → ℝ) :
186 Matrix.adjugate (Matrix.of E) 2 0 = E 1 0 * E 2 1 - E 1 1 * E 2 0 := by
187 rw [Matrix.adjugate_fin_three]; rfl
188
189private theorem adjugate21 (E : Fin 3 → Fin 3 → ℝ) :
190 Matrix.adjugate (Matrix.of E) 2 1 = -(E 0 0 * E 2 1) + E 0 1 * E 2 0 := by
191 rw [Matrix.adjugate_fin_three]; rfl
192
193private theorem adjugate22 (E : Fin 3 → Fin 3 → ℝ) :
194 Matrix.adjugate (Matrix.of E) 2 2 = E 0 0 * E 1 1 - E 0 1 * E 1 0 := by
195 rw [Matrix.adjugate_fin_three]; rfl
196
197/-- Fully explicit scalar form of the adjugate quadratic form. -/
198theorem adjugateQuadraticForm_explicit (E : Fin 3 → Fin 3 → ℝ)
199 (x : Fin 3 → ℝ) :
200 adjugateQuadraticForm E x =
201 x 0 * (E 1 1 * E 2 2 - E 1 2 * E 2 1) * x 0 +
202 x 0 * (-(E 0 1 * E 2 2) + E 0 2 * E 2 1) * x 1 +
203 x 0 * (E 0 1 * E 1 2 - E 0 2 * E 1 1) * x 2 +
204 (x 1 * (-(E 1 0 * E 2 2) + E 1 2 * E 2 0) * x 0 +
205 x 1 * (E 0 0 * E 2 2 - E 0 2 * E 2 0) * x 1 +
206 x 1 * (-(E 0 0 * E 1 2) + E 0 2 * E 1 0) * x 2) +
207 (x 2 * (E 1 0 * E 2 1 - E 1 1 * E 2 0) * x 0 +
208 x 2 * (-(E 0 0 * E 2 1) + E 0 1 * E 2 0) * x 1 +
209 x 2 * (E 0 0 * E 1 1 - E 0 1 * E 1 0) * x 2) := by
210 unfold adjugateQuadraticForm
211 simp only [Fin.sum_univ_three]
212 rw [adjugate00, adjugate01, adjugate02, adjugate10, adjugate11,
213 adjugate12, adjugate20, adjugate21, adjugate22]
214
215/-! ## §3. Step (i): the committed spike block sum is the closed form -/
216
217/-- Definitional expansion of the committed spike LHS at a marshalled
218matrix/direction pair (structure-projection reduction only). -/
219theorem committedSpikeLHS_spikeInput_expand (E : Fin 3 → Fin 3 → ℝ)
220 (x : Fin 3 → ℝ) :
221 ReggeTTBlochConventionAudit.committedSpikeLHS
222 (ReggeTTBlochConventionAudit.spikeInput E x) =
223 ReggeTTContinuumCertificateSpike.tetBlock0 (E 0 0) (E 0 1) (E 0 2)
224 (E 1 0) (E 1 1) (E 1 2) (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2)
225 (Real.sqrt 2) (Real.sqrt 3) Real.pi +
226 ReggeTTContinuumCertificateSpike.tetBlock1 (E 0 0) (E 0 1) (E 0 2)
227 (E 1 0) (E 1 1) (E 1 2) (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2)
228 (Real.sqrt 2) (Real.sqrt 3) Real.pi +
229 ReggeTTContinuumCertificateSpike.tetBlock2 (E 0 0) (E 0 1) (E 0 2)
230 (E 1 0) (E 1 1) (E 1 2) (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2)
231 (Real.sqrt 2) (Real.sqrt 3) Real.pi +
232 ReggeTTContinuumCertificateSpike.tetBlock3 (E 0 0) (E 0 1) (E 0 2)
233 (E 1 0) (E 1 1) (E 1 2) (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2)
234 (Real.sqrt 2) (Real.sqrt 3) Real.pi +
235 ReggeTTContinuumCertificateSpike.tetBlock4 (E 0 0) (E 0 1) (E 0 2)
236 (E 1 0) (E 1 1) (E 1 2) (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2)
237 (Real.sqrt 2) (Real.sqrt 3) Real.pi +
238 ReggeTTContinuumCertificateSpike.tetBlock5 (E 0 0) (E 0 1) (E 0 2)
239 (E 1 0) (E 1 1) (E 1 2) (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2)
240 (Real.sqrt 2) (Real.sqrt 3) Real.pi := rfl
241
242set_option maxHeartbeats 3200000 in
243/-- **STEP (i) OF THE C8 CLOSED FORM (THEOREM): the committed spike block
244sum equals `(1/2)·xᵀ·adj(E)·x` for every symmetric `E` and every `x`.**
245The three symmetry hypotheses are consumed through an explicit rotational
246cofactor certificate (the free-entry difference is
247`-(1/8)·(E₀₁x₂ − E₀₂x₁ − E₁₀x₂ + E₁₂x₀ + E₂₀x₁ − E₂₁x₀)²`, disclosed in
248the module docstring). Only the spike block DATA (`tetBlock*_eq`) is
249used; the spike's own TT certificate is never invoked. -/
250theorem committedSpikeLHS_eq_half_adjugate (E : Fin 3 → Fin 3 → ℝ)
251 (x : Fin 3 → ℝ)
252 (hsym01 : E 0 1 = E 1 0) (hsym02 : E 0 2 = E 2 0)
253 (hsym12 : E 1 2 = E 2 1) :
254 ReggeTTBlochConventionAudit.committedSpikeLHS
255 (ReggeTTBlochConventionAudit.spikeInput E x) =
256 (1 / 2) * adjugateQuadraticForm E x := by
257 rw [committedSpikeLHS_spikeInput_expand, adjugateQuadraticForm_explicit]
258 rw [ReggeTTContinuumCertificateSpike.tetBlock0_eq,
259 ReggeTTContinuumCertificateSpike.tetBlock1_eq,
260 ReggeTTContinuumCertificateSpike.tetBlock2_eq,
261 ReggeTTContinuumCertificateSpike.tetBlock3_eq,
262 ReggeTTContinuumCertificateSpike.tetBlock4_eq,
263 ReggeTTContinuumCertificateSpike.tetBlock5_eq]
264 linear_combination
265 (-(1 / 8) * (E 0 1 * x 2 - E 0 2 * x 1 - E 1 0 * x 2 + E 1 2 * x 0 +
266 E 2 0 * x 1 - E 2 1 * x 0) * x 2) * hsym01 +
267 ((1 / 8) * (E 0 1 * x 2 - E 0 2 * x 1 - E 1 0 * x 2 + E 1 2 * x 0 +
268 E 2 0 * x 1 - E 2 1 * x 0) * x 1) * hsym02 +
269 (-(1 / 8) * (E 0 1 * x 2 - E 0 2 * x 1 - E 1 0 * x 2 + E 1 2 * x 0 +
270 E 2 0 * x 1 - E 2 1 * x 0) * x 0) * hsym12
271
272/-- The Gate B bridge moment fold equals the closed form for symmetric
273polarizations. -/
274theorem bridgeMoment_eq_half_adjugate (E : Fin 3 → Fin 3 → ℝ)
275 (x : Fin 3 → ℝ)
276 (hsym01 : E 0 1 = E 1 0) (hsym02 : E 0 2 = E 2 0)
277 (hsym12 : E 1 2 = E 2 1) :
278 reggeTTMoment ReggeTTGateBBridge.rawMomentSupport
279 (ReggeTTGateBBridge.rawPhaseQuadratic x)
280 (ReggeTTGateBBridge.rawBucketAmplitude E) =
281 (1 / 2) * adjugateQuadraticForm E x := by
282 rw [ReggeTTGateBBridge.rawMoment_eq_committedSpikeLHS,
283 committedSpikeLHS_eq_half_adjugate E x hsym01 hsym02 hsym12]
284
285/-- **THE C8 CLOSED FORM, PRODUCTION HEADLINE (THEOREM): the continuum
286bucket moment fold of the P1.1a limit equals `(1/2)·xᵀ·adj(E)·x` for every
287symmetric polarization matrix and every real direction.** -/
288theorem continuumMoment_eq_half_adjugate (E : Fin 3 → Fin 3 → ℝ)
289 (x : Fin 3 → ℝ)
290 (hsym01 : E 0 1 = E 1 0) (hsym02 : E 0 2 = E 2 0)
291 (hsym12 : E 1 2 = E 2 1) :
292 reggeTTMoment ReggeTTBlochAssembly.rawCosineSupport
293 (ReggeTTContinuumLimit.rawPhaseQuadratic x)
294 (ReggeTTBlochAssembly.rawBucketAmplitude E) =
295 (1 / 2) * adjugateQuadraticForm E x := by
296 rw [continuumMoment_eq_bridgeMoment]
297 exact bridgeMoment_eq_half_adjugate E x hsym01 hsym02 hsym12
298
299/-! ## §4. Step (ii): the adjugate step on the TT variety -/
300
301set_option maxHeartbeats 1600000 in
302/-- **STEP (ii) OF THE C8 CLOSED FORM (THEOREM): on the TT variety the
303adjugate quadratic form collapses to `-(1/2)·|x|²·⟨E,E⟩`.** Kernel form
304of the eigenvalue argument (`x` is a null eigenvector of `E`, so
305`adj(E)x = λ₁λ₂x` with `λ₁ + λ₂ = 0`), discharged as an explicit cofactor
306certificate over the seven TT generators. -/
307theorem adjugateQuadraticForm_tt (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ)
308 (hsym01 : E 0 1 = E 1 0) (hsym02 : E 0 2 = E 2 0)
309 (hsym12 : E 1 2 = E 2 1)
310 (htr : E 0 0 + E 1 1 + E 2 2 = 0)
311 (htrans0 : x 0 * E 0 0 + x 1 * E 1 0 + x 2 * E 2 0 = 0)
312 (htrans1 : x 0 * E 0 1 + x 1 * E 1 1 + x 2 * E 2 1 = 0)
313 (htrans2 : x 0 * E 0 2 + x 1 * E 1 2 + x 2 * E 2 2 = 0) :
314 adjugateQuadraticForm E x =
315 -(1 / 2) * (x 0 ^ 2 + x 1 ^ 2 + x 2 ^ 2) *
316 (E 0 0 * E 0 0 + E 0 1 * E 0 1 + E 0 2 * E 0 2 + E 1 0 * E 1 0 +
317 E 1 1 * E 1 1 + E 1 2 * E 1 2 + E 2 0 * E 2 0 + E 2 1 * E 2 1 +
318 E 2 2 * E 2 2) := by
319 rw [adjugateQuadraticForm_explicit]
320 linear_combination
321 (E 0 0 * x 0 * x 1 - E 0 1 * x 0 ^ 2 / 2 + E 0 1 * x 1 ^ 2 / 2 +
322 E 0 1 * x 2 ^ 2 / 2 - E 1 0 * x 0 ^ 2 / 2 - E 1 0 * x 1 ^ 2 / 2 -
323 E 1 0 * x 2 ^ 2 / 2 - E 2 1 * x 0 * x 2 + E 2 2 * x 0 * x 1) *
324 hsym01 +
325 (E 0 0 * x 0 * x 2 - E 0 2 * x 0 ^ 2 / 2 + E 0 2 * x 1 ^ 2 / 2 +
326 E 0 2 * x 2 ^ 2 / 2 + E 1 1 * x 0 * x 2 - E 1 2 * x 0 * x 1 -
327 E 2 0 * x 0 ^ 2 / 2 - E 2 0 * x 1 ^ 2 / 2 - E 2 0 * x 2 ^ 2 / 2) *
328 hsym02 +
329 (E 0 0 * x 1 * x 2 - E 0 2 * x 0 * x 1 + E 1 1 * x 1 * x 2 +
330 E 1 2 * x 0 ^ 2 / 2 - E 1 2 * x 1 ^ 2 / 2 + E 1 2 * x 2 ^ 2 / 2 -
331 E 2 1 * x 0 ^ 2 / 2 - E 2 1 * x 1 ^ 2 / 2 - E 2 1 * x 2 ^ 2 / 2) *
332 hsym12 +
333 (-(E 0 0 * x 0 ^ 2) / 2 + E 0 0 * x 1 ^ 2 / 2 + E 0 0 * x 2 ^ 2 / 2 -
334 2 * E 0 1 * x 0 * x 1 - E 0 2 * x 0 * x 2 + E 1 1 * x 0 ^ 2 / 2 -
335 E 1 1 * x 1 ^ 2 / 2 + E 1 1 * x 2 ^ 2 / 2 - E 1 2 * x 1 * x 2 +
336 E 2 2 * x 0 ^ 2 / 2 + E 2 2 * x 1 ^ 2 / 2 + E 2 2 * x 2 ^ 2 / 2) *
337 htr +
338 (E 0 0 * x 0 + E 0 1 * x 1 + E 0 2 * x 2) * htrans0 +
339 (E 0 1 * x 0 + E 1 1 * x 1 + E 1 2 * x 2) * htrans1 +
340 (-(E 0 0 * x 2) + E 0 2 * x 0 - E 1 1 * x 2 + E 1 2 * x 1) * htrans2
341
342/-! ## §5. P1.1b: the isotropy value `-(1/4)` -/
343
344/-- The moment value at unit-normalized real TT data: the fold equals
345exactly `reggeTTContinuumCoefficient = -(1/4)`. -/
346theorem reggeTTMoment_tt_real (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ)
347 (hsym01 : E 0 1 = E 1 0) (hsym02 : E 0 2 = E 2 0)
348 (hsym12 : E 1 2 = E 2 1)
349 (htr : E 0 0 + E 1 1 + E 2 2 = 0)
350 (htrans0 : x 0 * E 0 0 + x 1 * E 1 0 + x 2 * E 2 0 = 0)
351 (htrans1 : x 0 * E 0 1 + x 1 * E 1 1 + x 2 * E 2 1 = 0)
352 (htrans2 : x 0 * E 0 2 + x 1 * E 1 2 + x 2 * E 2 2 = 0)
353 (hxnorm : x 0 ^ 2 + x 1 ^ 2 + x 2 ^ 2 = 1)
354 (hEnorm : (∑ i : Fin 3, ∑ j : Fin 3, E i j * E i j) = 1) :
355 reggeTTMoment ReggeTTBlochAssembly.rawCosineSupport
356 (ReggeTTContinuumLimit.rawPhaseQuadratic x)
357 (ReggeTTBlochAssembly.rawBucketAmplitude E) =
358 reggeTTContinuumCoefficient := by
359 have hEnorm' := hEnorm
360 simp only [Fin.sum_univ_three] at hEnorm'
361 have hcoeff : reggeTTContinuumCoefficient = -(1 / 4 : ℝ) := rfl
362 rw [continuumMoment_eq_half_adjugate E x hsym01 hsym02 hsym12,
363 adjugateQuadraticForm_tt E x hsym01 hsym02 hsym12 htr htrans0 htrans1
364 htrans2, hcoeff]
365 linear_combination
366 (-(1 / 4 : ℝ) * (x 0 ^ 2 + x 1 ^ 2 + x 2 ^ 2)) * hEnorm' +
367 (-(1 / 4 : ℝ)) * hxnorm
368
369/-- **P1.1b HEADLINE (THEOREM): for every nonzero integer mode and every
370TT polarization, the P1.1a continuum moment at the normalized real
371direction equals exactly `reggeTTContinuumCoefficient = -(1/4)`.** -/
372theorem reggeTTMoment_tt_value (m : Fin 3 → ℤ) (E : Fin 3 → Fin 3 → ℝ)
373 (hm : ∃ i : Fin 3, m i ≠ 0) (hTT : IsTTPolarization m E) :
374 reggeTTMoment ReggeTTBlochAssembly.rawCosineSupport
375 (ReggeTTContinuumLimit.rawPhaseQuadratic
376 (ReggeTTContinuumLimit.normalizedRealMode m))
377 (ReggeTTBlochAssembly.rawBucketAmplitude E) =
378 reggeTTContinuumCoefficient := by
379 obtain ⟨hsymm, htrace, htrans, hnorm⟩ := hTT
380 have hs : 0 < ReggeTTContinuumLimit.realModeNormSq (fun i => (m i : ℝ)) :=
381 ReggeTTContinuumLimit.realModeNormSq_intCast_pos m hm
382 have hxval : ∀ i : Fin 3,
383 ReggeTTContinuumLimit.normalizedRealMode m i =
384 (m i : ℝ) /
385 Real.sqrt (ReggeTTContinuumLimit.realModeNormSq
386 (fun j => (m j : ℝ))) := fun i => rfl
387 have htr : E 0 0 + E 1 1 + E 2 2 = 0 := by
388 have h := htrace
389 rwa [Fin.sum_univ_three] at h
390 have hxtrans : ∀ j : Fin 3,
391 ReggeTTContinuumLimit.normalizedRealMode m 0 * E 0 j +
392 ReggeTTContinuumLimit.normalizedRealMode m 1 * E 1 j +
393 ReggeTTContinuumLimit.normalizedRealMode m 2 * E 2 j = 0 := by
394 intro j
395 have h := htrans j
396 rw [Fin.sum_univ_three] at h
397 rw [hxval 0, hxval 1, hxval 2, div_mul_eq_mul_div, div_mul_eq_mul_div,
398 div_mul_eq_mul_div, div_add_div_same, div_add_div_same, h, zero_div]
399 have hxnorm :
400 ReggeTTContinuumLimit.normalizedRealMode m 0 ^ 2 +
401 ReggeTTContinuumLimit.normalizedRealMode m 1 ^ 2 +
402 ReggeTTContinuumLimit.normalizedRealMode m 2 ^ 2 = 1 := by
403 have hsum : (m 0 : ℝ) ^ 2 + (m 1 : ℝ) ^ 2 + (m 2 : ℝ) ^ 2 =
404 ReggeTTContinuumLimit.realModeNormSq (fun j => (m j : ℝ)) := by
405 simp only [ReggeTTContinuumLimit.realModeNormSq, Fin.sum_univ_three]
406 rw [hxval 0, hxval 1, hxval 2, div_pow, div_pow, div_pow,
407 div_add_div_same, div_add_div_same, Real.sq_sqrt hs.le, hsum,
408 div_self hs.ne']
409 exact reggeTTMoment_tt_real E (ReggeTTContinuumLimit.normalizedRealMode m)
410 (hsymm 0 1) (hsymm 0 2) (hsymm 1 2) htr (hxtrans 0) (hxtrans 1)
411 (hxtrans 2) hxnorm hnorm
412
413/-- **P1.1a + P1.1b COMPOSED (THEOREM): the normalized finite reduced
414Regge TT symbol converges to exactly `-(1/4)` for every nonzero integer
415mode and every TT polarization.** -/
416theorem canonicalFiniteH_div_momentumNormSq_tendsto_isotropy
417 (m : Fin 3 → ℤ) (E : Fin 3 → Fin 3 → ℝ)
418 (hm : ∃ i : Fin 3, m i ≠ 0) (hTT : IsTTPolarization m E) :
419 Filter.Tendsto
420 (fun j : ℕ =>
421 @canonicalFiniteH (j + 3) (instNeZeroAddThree j) E m /
422 momentumNormSq (j + 3) m)
423 Filter.atTop (nhds reggeTTContinuumCoefficient) := by
424 have h :=
425 ReggeTTContinuumLimit.canonicalFiniteH_div_momentumNormSq_tendsto E m hm
426 rwa [reggeTTMoment_tt_value m E hm hTT] at h
427
428end
429
430end ReggeTTAlgebraicCloser
431end Analysis
432end Gravity
433end IndisputableMonolith
434
435#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTAlgebraicCloser.continuumMoment_eq_bridgeMoment
436#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTAlgebraicCloser.committedSpikeLHS_eq_half_adjugate
437#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTAlgebraicCloser.continuumMoment_eq_half_adjugate
438#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTAlgebraicCloser.adjugateQuadraticForm_tt
439#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTAlgebraicCloser.reggeTTMoment_tt_value
440#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTAlgebraicCloser.canonicalFiniteH_div_momentumNormSq_tendsto_isotropy
441