IndisputableMonolith.Gravity.Analysis.ReggeTTSymbolPreflight
IndisputableMonolith/Gravity/Analysis/ReggeTTSymbolPreflight.lean · 801 lines · 55 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.FreudenthalStencilPreflight
3import IndisputableMonolith.Gravity.PhysicalSixTetCubicDirichletInstance
4
5/-!
6# Regge TT symbol preflight: the true nonlinear action, its flat point, the
7# frozen-model identification, and the TT Bloch symbol object
8
9QG full-theory campaign, `ReggeTTContinuumSymbol` program, Stage 1 (unlocked
10by critic sign-off on the C10 probe, receipt commit 1e38531ee2).
11
12## Tier tags (binding, per-claim)
13
14* THEOREM: everything proved in this file (kernel-checked here; no sorry, no
15 admit, no new axioms, no native_decide, no `: True` shells).
16* NUMERICAL EVIDENCE (never proof): the C10 provenance-gated numerics probe
17 (`state/qg_full_theory/true_regge_tt_probe/`, commit f1d44266e5, critic
18 sign-off with independent reproduction at 1e38531ee2) reports that the TT
19 Bloch symbol of the true nonlinear Regge action on this lattice is
20 ISOTROPIC in the continuum limit with value `K(0) = -(1/4)·I_TT` on all 14
21 preregistered directions, and that `-1/4` is exactly the linearized
22 Einstein-Hilbert TT coefficient in those conventions. Nothing in this
23 file proves that; the corresponding Lean statement is the named OPEN
24 target `ReggeTTContinuumIsotropyTarget` below, and its status flag is
25 `false`.
26* OPEN: `ReggeTTContinuumIsotropyTarget` (existence and value of the
27 continuum TT symbol).
28
29## What this module defines (a, c)
30
31* `trueReggeAction`: the TRUE nonlinear 3D Regge action on the canonical
32 periodic Freudenthal torus as a function of an ARBITRARY edge
33 squared-length field `ℓ : PeriodicEdge N N N → ℝ`:
34 `S(ℓ) = Σ_e √(ℓ_e) · (2π − Σ_{incident tets} θ)`, with the dihedral
35 angles computed by the existing Cayley-Menger machinery
36 (`dihedralAngle3Sq`, i.e. `arccos` of the `cmCofactor3` ratio) on the
37 local squared-edge tuples read off the field through the canonical
38 edge-slot lookup `canonicalEdgeSlot?`. The deficit machinery is REUSED,
39 not re-derived: the per-slot angle is literally
40 `DihedralDerivatives.dihedralAngle3Sq`, and at conformal fields the whole
41 action is proved equal to the existing
42 `ReggeActionConcrete.reggeAction` (see `reggeAction_conformal_eq`).
43* `planeWaveEdgeField`, `ttSecondDifference`, `TTBlochSymbolIs`,
44 `ReggeTTContinuumSymbolIs`: the TT Bloch symbol object. For a
45 commensurate momentum `k = 2π·m/N` (`m : Fin 3 → ℤ`, so `k` is
46 commensurate on the side-`N` torus for every `N`) and a polarization
47 matrix `E`, the perturbation family is the midpoint-phase plane wave of
48 the C10 preregistration, `ℓ_e(t) = ℓ²_flat + t·(E·D_d·D_d)·cos(k·(x +
49 D_d/2))`; `ttSecondDifference` is its per-unit-cell second-difference
50 quadratic form `(2/N³)·(S(t) − 2S(0) + S(−t))/t²`;
51 `TTBlochSymbolIs N E m H` states (via `Filter.Tendsto` on `𝓝[≠] 0`)
52 that the amplitude second difference converges to `H`; and
53 `ReggeTTContinuumSymbolIs E m Λ` states that the `|k|²`-normalized
54 symbol values converge to `Λ` along the torus family `N = j + 3 → ∞`
55 (fixed integer wave vector, so `|k_N| → 0` at fixed direction). These
56 are DEFINITIONS ONLY: no existence or value of any of these limits is
57 claimed anywhere in this file.
58
59## What this module proves (b, d) — all THEOREM
60
61* Flat point (b): `deficitOfField_flatEdgeField` — at the flat edge
62 assignment (`ℓ_e = ℓ²` of the displacement class) every deficit vanishes
63 (reusing the certified periodic angle-sum chain
64 `canonicalPeriodicDirectTypedEdgeAngleSumTarget_holds`, not re-proved);
65 hence `trueReggeAction_flatEdgeField : S(flat) = 0` and
66 `planeWaveActionProfile_zero : S(plane wave at t = 0) = 0`.
67* Frozen-model identification (d), as kernel equations:
68 - `reggeAction_conformal_eq`: the existing conformal-ansatz action
69 `ReggeActionConcrete.reggeAction` is EXACTLY the true action evaluated
70 on the conformal edge fields
71 `ℓ_e = ℓ²_flat(e) · exp(ξ_u + ξ_v)` (`typedConformalEdgeField`). This
72 states precisely which restriction the frozen wave analyzed.
73 - `frozen_identification` / `frozen_identification_stencil`: along that
74 conformal family the true action decomposes as `S = (1/2)·Q_frozen + R`,
75 where `Q_frozen` is the quadratic form of the frozen graph-Laplacian
76 model `canonicalReggeHessian` and `R` is the remainder. HONESTY NOTE:
77 this decomposition is a DEFINITIONAL TAUTOLOGY and carries NO
78 mathematical content on its own — `reggeActionRemainder` is DEFINED as
79 `S − S(0) − (1/2)·Q`, so the equation holds for ANY quadratic form `Q`
80 and does NOT pin the graph-Laplacian in any way. It is here only to
81 NAME the frozen postulate explicitly and to expose `R` as the object a
82 later stage must expand. The genuine (non-tautological) content of
83 this file's frozen-model bridge lives in the two REAL equalities:
84 (1) `reggeAction_conformal_eq` — the existing conformal-ansatz action
85 equals the true action on conformal edge fields (a real identity of
86 two independently defined expressions), and (2) the stage-1 Test G
87 theorem `hessianQuadratic_canonical_eq_freudenthalStencil` — `Q_frozen`
88 equals the anisotropic seven-class stencil energy with moment tensor
89 `A₀ = (1+√2)I + (√2+√3)J`. So the identification that was FROZEN is:
90 (i) restrict the true action to vertex-conformal edge fields
91 (`reggeAction_conformal_eq`, real), and (ii) POSTULATE the graph-
92 Laplacian `canonicalReggeHessian` as its quadratic model (the postulate
93 itself, not a theorem). The TT plane-wave fields of the C10 probe are
94 not of that conformal form, which is how the frozen anisotropy and the
95 (numerically observed) true-TT isotropy coexist.
96 - `reggeAction_zeroPotential_eq_zero`: flat normalization of the
97 conformal action, obtained here as a corollary of the typed flat-point
98 theorem (no side-length hypothesis needed).
99* Symbol-object well-formedness and symmetry (d):
100 `planeWaveEdgeField_zero_amplitude` (the family passes through flat),
101 `ttSecondDifference_even` (evenness in the amplitude),
102 `ttSecondDifference_neg_polarization` (invariance under `E ↦ −E`, the
103 quadratic-form sign symmetry), `polEdgeCoeff_neg`.
104* Non-vacuity of the OPEN target's hypothesis class:
105 `axisTTPolarizationPlus_isTT` / `axisTTPolarizationCross_isTT` — the
106 preregistered axis direction carries two explicit TT polarizations
107 satisfying `IsTTPolarization` (symmetric, traceless, transverse,
108 Frobenius-normalized), so `ReggeTTContinuumIsotropyTarget` does not
109 quantify over an empty set.
110
111## Re-scoping disclosure (binding)
112
113Stage-1 scope was re-scoped DOWN in two places, disclosed here and in the
114status flags:
115
1161. First-order behavior of the action at the flat point (differentiability
117 of the arccos-of-Cayley-Menger-ratio compositions along the plane-wave
118 family) is NOT proved here. The flat VALUE is proved
119 (`trueReggeAction_flatEdgeField`); derivatives are not attempted.
1202. The existence and value of the TT Bloch symbol limits are NOT claimed.
121 `TTBlochSymbolIs`/`ReggeTTContinuumSymbolIs` are definitions;
122 `ReggeTTContinuumIsotropyTarget` (value `-(1/4)` on TT polarizations)
123 is a named OPEN target with status flag `false`. The C10 numbers stay
124 NUMERICAL EVIDENCE.
125
126No `sorry`, no `admit`, no new axioms, no `native_decide` in this file.
127
128## Inherited axiom footprint (disclosure)
129
130`#print axioms` on the flat-point theorems and everything downstream of
131them (`deficitOfField_flatEdgeField`, `trueReggeAction_flatEdgeField`,
132`reggeAction_zeroPotential_eq_zero`, `frozen_identification`,
133`frozen_identification_stencil`, `status_flags_grounded`) reports
134`[propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler,
135Quot.sound]`. The compiler-trust axioms `Lean.ofReduceBool` /
136`Lean.trustCompiler` are NOT introduced here: they enter through the
137inherited certified Freudenthal angle-sum chain
138(`PhysicalSixTetCubicDirichletInstance.canonicalPeriodicDirectTypedEdgeAngleSumTarget_holds`
139already carries exactly this footprint). The purely algebraic theorems of
140this file (`reggeAction_conformal_eq`, `ttSecondDifference_even`,
141`ttSecondDifference_neg_polarization`, `axisTTPolarizationPlus_isTT`,
142`axisTTPolarizationCross_isTT`) carry the standard footprint
143`[propext, Classical.choice, Quot.sound]`. Audited in
144`scripts/qg7_axiom_audit.lean`.
145-/
146
147namespace IndisputableMonolith
148namespace Gravity
149namespace Analysis
150namespace ReggeTTSymbolPreflight
151
152open Geometry.PeriodicFreudenthalTorus
153open Geometry.ReggeActionConcrete
154open Geometry.ReggeHessian3D
155open Geometry.DihedralDerivatives
156open PhysicalSixTetCubicDirichletInstance
157open FreudenthalStencilPreflight
158
159noncomputable section
160
161variable (N : ℕ) [NeZero N]
162
163/-! ## §1. The true Regge action on edge squared-length fields (a)
164
165The action is a function of an arbitrary per-edge squared-length field on
166the typed periodic Freudenthal torus. The Lean deficit machinery is reused
167verbatim: local squared-edge tuples are read off the field through the
168canonical edge-slot tables, and each dihedral angle is
169`DihedralDerivatives.dihedralAngle3Sq` (arccos of the Cayley-Menger
170cofactor ratio `dihedralCos3Sq`). -/
171
172/-- An edge squared-length field on the side-`N` periodic Freudenthal
173torus: one real number (a squared length) per positive-displacement
174periodic edge. -/
175abbrev EdgeField := PeriodicEdge N N N → ℝ
176
177/-- The flat background field: every edge carries the squared length of its
178displacement class (`1,1,1,2,2,2,3`). -/
179def flatEdgeField : EdgeField N := fun e => periodicDispSqEdge e.disp
180
181/-- The six local squared-edge coordinates of the tetrahedron
182`(cell, tet)`, read off an edge field through the canonical local-edge
183tables. -/
184def tetSqEdgesOfField (ℓ : EdgeField N) (cellTet : PeriodicTet N N N) :
185 Geometry.CayleyMengerPolynomial.SqEdges :=
186 fun f => ℓ (localEdgeOf cellTet.1 cellTet.2 f)
187
188/-- Dihedral angle at local edge slot `f` of tetrahedron `(cell, tet)`
189under an edge field: the existing Cayley-Menger `arccos` machinery applied
190to the field's local squared-edge tuple. -/
191def tetDihedralAngleOfField (ℓ : EdgeField N) (cellTet : PeriodicTet N N N)
192 (f : Fin 6) : ℝ :=
193 dihedralAngle3Sq (tetSqEdgesOfField N ℓ cellTet) f
194
195/-- Contribution of the tetrahedron `(cell, tet)` to the angle sum around a
196periodic edge, under an edge field. Mirrors
197`localDeficitAngleContribution` through the same `canonicalEdgeSlot?`
198lookup. -/
199def edgeAngleContributionOfField (ℓ : EdgeField N) (e : PeriodicEdge N N N)
200 (cellTet : PeriodicTet N N N) : ℝ :=
201 match canonicalEdgeSlot? e cellTet.1 cellTet.2 with
202 | some f => tetDihedralAngleOfField N ℓ cellTet f
203 | none => 0
204
205/-- Regge deficit angle at a periodic edge under an edge field:
206`2π` minus the incident dihedral-angle sum. -/
207def deficitOfField (ℓ : EdgeField N) (e : PeriodicEdge N N N) : ℝ :=
208 2 * Real.pi -
209 ∑ cellTet : PeriodicTet N N N, edgeAngleContributionOfField N ℓ e cellTet
210
211/-- THE TRUE NONLINEAR 3D REGGE ACTION on the side-`N` periodic Freudenthal
212torus, as a function of the edge squared-length field:
213`S(ℓ) = Σ_e √(ℓ_e) · deficit_e`. This is the object whose TT Bloch symbol
214the C10 probe measured. -/
215def trueReggeAction (ℓ : EdgeField N) : ℝ :=
216 ∑ e : PeriodicEdge N N N, Real.sqrt (ℓ e) * deficitOfField N ℓ e
217
218/-! ## §2. The flat point (b) — THEOREM -/
219
220/-- At the flat field, every tetrahedron sees exactly the canonical
221one-cube Freudenthal squared-edge tuple. -/
222theorem tetSqEdgesOfField_flat (cellTet : PeriodicTet N N N) :
223 tetSqEdgesOfField N (flatEdgeField N) cellTet =
224 Geometry.FreudenthalCubeTriangulation.freudenthalTetSqEdges := by
225 funext f
226 simp only [tetSqEdgesOfField, flatEdgeField]
227 exact (freudenthalTet_sqEdge_eq_periodicDispSqEdge_localEdgeOf
228 cellTet.1 cellTet.2 f).symm
229
230/-- At the flat field, the per-tetrahedron angle contribution is exactly
231the certified typed-edge angle contribution of the periodic angle-sum
232chain. -/
233theorem edgeAngleContributionOfField_flat (e : PeriodicEdge N N N)
234 (cellTet : PeriodicTet N N N) :
235 edgeAngleContributionOfField N (flatEdgeField N) e cellTet =
236 canonicalPeriodicTypedEdgeAngleContribution e cellTet := by
237 simp only [edgeAngleContributionOfField,
238 canonicalPeriodicTypedEdgeAngleContribution]
239 cases h : canonicalEdgeSlot? e cellTet.1 cellTet.2 with
240 | none => rfl
241 | some f =>
242 simp only [tetDihedralAngleOfField, tetSqEdgesOfField_flat,
243 freudenthalLocalDihedralAngle]
244
245/-- FLAT POINT, deficit form (THEOREM): at the flat edge assignment every
246deficit angle vanishes. Reuses the certified periodic angle-sum chain
247(`canonicalPeriodicDirectTypedEdgeAngleSumTarget_holds`); the geometry is
248not re-derived here. -/
249theorem deficitOfField_flatEdgeField (e : PeriodicEdge N N N) :
250 deficitOfField N (flatEdgeField N) e = 0 := by
251 unfold deficitOfField
252 have hsum :
253 (∑ cellTet : PeriodicTet N N N,
254 edgeAngleContributionOfField N (flatEdgeField N) e cellTet) =
255 2 * Real.pi := by
256 calc
257 (∑ cellTet : PeriodicTet N N N,
258 edgeAngleContributionOfField N (flatEdgeField N) e cellTet)
259 = ∑ cellTet : PeriodicTet N N N,
260 canonicalPeriodicTypedEdgeAngleContribution e cellTet :=
261 Finset.sum_congr rfl fun cellTet _ =>
262 edgeAngleContributionOfField_flat N e cellTet
263 _ = 2 * Real.pi :=
264 canonicalPeriodicDirectTypedEdgeAngleSumTarget_holds N N N e
265 rw [hsum]
266 ring
267
268/-- FLAT POINT, action form (THEOREM): the true Regge action vanishes at
269the flat edge assignment. -/
270theorem trueReggeAction_flatEdgeField :
271 trueReggeAction N (flatEdgeField N) = 0 := by
272 unfold trueReggeAction
273 refine Finset.sum_eq_zero fun e _ => ?_
274 rw [deficitOfField_flatEdgeField N e, mul_zero]
275
276/-! ## §3. The frozen-model identification (d) — THEOREM
277
278The frozen wave (Test G, `FreudenthalStencilPreflight` /
279`FreudenthalEnergyLimit`) analyzed `ReggeActionConcrete.reggeAction`, the
280vertex-conformal restriction of the true action, with the graph-Laplacian
281`canonicalReggeHessian` POSTULATED as its quadratic model. The next
282theorems state that identification as kernel equations. -/
283
284/-- The conformal edge field induced by a vertex potential `u`: edge `e`
285carries `ℓ²_flat(e) · exp(u(e₊) + u(e₋))`. This is EXACTLY the family of
286edge fields the frozen wave analyzed (through
287`ReggeActionConcrete.conformalLocalSqEdge`). -/
288def typedConformalEdgeField (u : Vertex N N N → ℝ) : EdgeField N :=
289 fun e =>
290 periodicDispSqEdge e.disp *
291 Real.exp (u e.endpoints.1 + u e.endpoints.2)
292
293theorem periodicDispSqEdge_nonneg (d : Fin 7) : 0 ≤ periodicDispSqEdge d := by
294 fin_cases d <;> norm_num [periodicDispSqEdge]
295
296/-- Definitional transparency of the canonical triangulation's local
297tetrahedron (proof is `rfl`). -/
298theorem canonical_tet_eq (τ : Fin (canonicalPeriodicTriangulation N N N).nT) :
299 (canonicalPeriodicTriangulation N N N).tet τ =
300 Geometry.FreudenthalCubeTriangulation.freudenthalTet := rfl
301
302/-- Definitional transparency of the canonical triangulation's tetrahedron
303vertex map (proof is `rfl`). -/
304theorem canonical_tetVerts_eq
305 (τ : Fin (canonicalPeriodicTriangulation N N N).nT) (k : Fin 4) :
306 (canonicalPeriodicTriangulation N N N).tetVerts τ k =
307 (vertexFinEquiv N N N).symm
308 (addVertexBits (tetFinEquiv N N N τ).1
309 (Geometry.FreudenthalCubeTriangulation.tetVerts
310 (tetFinEquiv N N N τ).2 k)) := rfl
311
312/-- Definitional transparency of the canonical triangulation's
313edge-in-tetrahedron lookup (proof is `rfl`). -/
314theorem canonical_edgeInTet_eq
315 (e : Fin (canonicalPeriodicTriangulation N N N).nE)
316 (τ : Fin (canonicalPeriodicTriangulation N N N).nT) :
317 (canonicalPeriodicTriangulation N N N).edgeInTet e τ =
318 canonicalEdgeSlot? (edgeFinEquiv N N N e)
319 (tetFinEquiv N N N τ).1 (tetFinEquiv N N N τ).2 := rfl
320
321/-- The conformal local squared-edge tuple of the frozen wave equals the
322typed conformal edge field read through the local-edge tables. -/
323theorem conformalTetSqEdges_eq_typedField (u : Vertex N N N → ℝ)
324 (τ : Fin (canonicalPeriodicTriangulation N N N).nT) :
325 conformalTetSqEdges (canonicalPeriodicTriangulation N N N)
326 (toPotential N u) τ =
327 tetSqEdgesOfField N (typedConformalEdgeField N u)
328 (tetFinEquiv N N N τ) := by
329 funext f
330 simp only [conformalTetSqEdges, conformalLocalSqEdge, tetSqEdgesOfField,
331 typedConformalEdgeField]
332 rw [canonical_tet_eq, canonical_tetVerts_eq, canonical_tetVerts_eq,
333 toPotential_symm_apply, toPotential_symm_apply]
334 rw [show Geometry.FreudenthalCubeTriangulation.freudenthalTet.sqEdge f =
335 periodicDispSqEdge
336 ((localEdgeOf (tetFinEquiv N N N τ).1 (tetFinEquiv N N N τ).2
337 f).disp) from
338 freudenthalTet_sqEdge_eq_periodicDispSqEdge_localEdgeOf
339 (tetFinEquiv N N N τ).1 (tetFinEquiv N N N τ).2 f]
340 rcases localEdgeOf_endpoints_match_tetVerts
341 (tetFinEquiv N N N τ).1 (tetFinEquiv N N N τ).2 f with
342 ⟨h1, h2⟩ | ⟨h1, h2⟩
343 · rw [h1, h2]
344 · have harg :
345 u (addVertexBits (tetFinEquiv N N N τ).1
346 (Geometry.FreudenthalCubeTriangulation.tetVerts
347 (tetFinEquiv N N N τ).2
348 (Geometry.ReggeRigorousFoundation.edgeVertices f).1)) +
349 u (addVertexBits (tetFinEquiv N N N τ).1
350 (Geometry.FreudenthalCubeTriangulation.tetVerts
351 (tetFinEquiv N N N τ).2
352 (Geometry.ReggeRigorousFoundation.edgeVertices f).2)) =
353 u ((localEdgeOf (tetFinEquiv N N N τ).1 (tetFinEquiv N N N τ).2
354 f).endpoints.1) +
355 u ((localEdgeOf (tetFinEquiv N N N τ).1 (tetFinEquiv N N N τ).2
356 f).endpoints.2) := by
357 rw [h1, h2, add_comm]
358 rw [harg]
359
360/-- The frozen wave's deficit angle at a conformal potential equals the
361true-action deficit at the corresponding conformal edge field. -/
362theorem deficitAngle_conformal_eq (u : Vertex N N N → ℝ)
363 (e : Fin (canonicalPeriodicTriangulation N N N).nE) :
364 deficitAngle (canonicalPeriodicTriangulation N N N) (toPotential N u) e =
365 deficitOfField N (typedConformalEdgeField N u)
366 (edgeFinEquiv N N N e) := by
367 unfold deficitAngle deficitOfField
368 congr 1
369 refine Fintype.sum_equiv (tetFinEquiv N N N) _ _ fun τ => ?_
370 simp only [localDeficitAngleContribution, edgeAngleContributionOfField]
371 rw [canonical_edgeInTet_eq]
372 cases h : canonicalEdgeSlot? (edgeFinEquiv N N N e)
373 (tetFinEquiv N N N τ).1 (tetFinEquiv N N N τ).2 with
374 | none => rfl
375 | some f =>
376 simp only [tetDihedralAngleUnderConformal, tetDihedralAngleOfField,
377 dihedralAngle3Sq]
378 rw [conformalTetSqEdges_eq_typedField]
379
380/-- The frozen wave's conformal hinge measure equals the square root of the
381conformal edge field. -/
382theorem hingeMeasure_conformal_eq (u : Vertex N N N → ℝ)
383 (e : Fin (canonicalPeriodicTriangulation N N N).nE) :
384 hingeMeasureUnderConformal (canonicalPeriodicTriangulation N N N)
385 (canonicalPeriodicIncidenceConsistent N N N) (toPotential N u) e =
386 Real.sqrt (typedConformalEdgeField N u (edgeFinEquiv N N N e)) := by
387 simp only [hingeMeasureUnderConformal, typedConformalEdgeField]
388 rw [canonical_edgeVerts_eq N e, canonical_globalSqEdge_eq N e]
389 rw [Real.sqrt_mul (periodicDispSqEdge_nonneg _), ← Real.exp_half,
390 toPotential_symm_apply, toPotential_symm_apply]
391
392/-- FROZEN-MODEL IDENTIFICATION, part 1 (THEOREM): the conformal-ansatz
393Regge action analyzed by the frozen wave is EXACTLY the true nonlinear
394Regge action evaluated on the conformal edge fields. This is the kernel
395equation stating which restriction of the true action the frozen model
396lives on. -/
397theorem reggeAction_conformal_eq (u : Vertex N N N → ℝ) :
398 reggeAction (canonicalPeriodicTriangulation N N N)
399 (canonicalPeriodicIncidenceConsistent N N N) (toPotential N u) =
400 trueReggeAction N (typedConformalEdgeField N u) := by
401 unfold reggeAction trueReggeAction
402 refine Fintype.sum_equiv (edgeFinEquiv N N N) _ _ fun e => ?_
403 rw [hingeMeasure_conformal_eq, deficitAngle_conformal_eq]
404
405/-- The zero potential induces the flat edge field. -/
406theorem typedConformalEdgeField_zero :
407 typedConformalEdgeField N (fun _ => 0) = flatEdgeField N := by
408 funext e
409 simp only [typedConformalEdgeField, flatEdgeField, add_zero,
410 Real.exp_zero, mul_one]
411
412/-- Flat normalization of the conformal action, derived here from the typed
413flat point (no side-length hypothesis needed). -/
414theorem reggeAction_zeroPotential_eq_zero :
415 reggeAction (canonicalPeriodicTriangulation N N N)
416 (canonicalPeriodicIncidenceConsistent N N N)
417 (zeroPotential (canonicalPeriodicTriangulation N N N)) = 0 := by
418 have h : toPotential N (fun _ => 0) =
419 zeroPotential (canonicalPeriodicTriangulation N N N) := rfl
420 rw [← h, reggeAction_conformal_eq, typedConformalEdgeField_zero,
421 trueReggeAction_flatEdgeField]
422
423/-- FROZEN-MODEL IDENTIFICATION, part 2 (THEOREM, but DEFINITIONALLY TRUE):
424along the conformal family the true action decomposes as
425`S = (1/2)·Q_frozen + remainder`, where `Q_frozen` is the quadratic form of
426the frozen graph-Laplacian `canonicalReggeHessian`. CONTENT WARNING: this
427equation is a tautology — `reggeActionRemainder` is DEFINED as
428`S − S(0) − (1/2)·Q`, so it holds for any quadratic form and pins nothing.
429It exists only to name the frozen postulate and expose the remainder as the
430object a later stage must expand. The real (non-tautological) content is
431`reggeAction_conformal_eq` (a genuine equality of two independently defined
432actions) composed with `hessianQuadratic_canonical_eq_freudenthalStencil`
433(Test G). The identification that was FROZEN is: restrict to conformal edge
434fields (real theorem) and POSTULATE `canonicalReggeHessian` as the quadratic
435model (a postulate, not proved). -/
436theorem frozen_identification (u : Vertex N N N → ℝ) :
437 trueReggeAction N (typedConformalEdgeField N u) =
438 (1 / 2) *
439 hessianQuadratic
440 (canonicalReggeHessian (canonicalPeriodicTriangulation N N N)
441 (canonicalPeriodicIncidenceConsistent N N N))
442 (toPotential N u) +
443 reggeActionRemainder (canonicalPeriodicTriangulation N N N)
444 (canonicalPeriodicIncidenceConsistent N N N)
445 (canonicalReggeHessian (canonicalPeriodicTriangulation N N N)
446 (canonicalPeriodicIncidenceConsistent N N N))
447 (toPotential N u) := by
448 rw [← reggeAction_conformal_eq]
449 rw [reggeAction_taylor_decomposition (canonicalPeriodicTriangulation N N N)
450 (canonicalPeriodicIncidenceConsistent N N N)
451 (canonicalReggeHessian (canonicalPeriodicTriangulation N N N)
452 (canonicalPeriodicIncidenceConsistent N N N))
453 (toPotential N u)]
454 rw [reggeAction_zeroPotential_eq_zero]
455 ring
456
457/-- FROZEN-MODEL IDENTIFICATION, stencil form (THEOREM, `N > 2`): the
458frozen quadratic term along the conformal family is the anisotropic
459seven-class stencil energy of Test G (whose continuum moment tensor is
460`A₀ = (1+√2)I + (√2+√3)J`, `stencilMomentTensor_eq`). The (numerically
461observed) isotropic TT physics lives OUTSIDE this conformal family; the
462frozen anisotropy is a statement about this restriction plus this quadratic
463model, which is how the two coexist. -/
464theorem frozen_identification_stencil (hN : 2 < N) (u : Vertex N N N → ℝ) :
465 trueReggeAction N (typedConformalEdgeField N u) =
466 (1 / 2) * freudenthalStencilEnergy N u +
467 reggeActionRemainder (canonicalPeriodicTriangulation N N N)
468 (canonicalPeriodicIncidenceConsistent N N N)
469 (canonicalReggeHessian (canonicalPeriodicTriangulation N N N)
470 (canonicalPeriodicIncidenceConsistent N N N))
471 (toPotential N u) := by
472 rw [frozen_identification N u,
473 hessianQuadratic_canonical_eq_freudenthalStencil N hN u]
474
475/-! ## §4. The TT Bloch symbol object (c) — DEFINITIONS ONLY
476
477Everything in this section is a definition; no limit existence or value is
478claimed. The perturbation family, the midpoint Bloch-phase convention, the
479per-unit-cell normalization `(2/N³)`, and the `|k|⁻²` momentum
480normalization mirror the C10 preregistration
481(`state/qg_full_theory/true_regge_tt_probe/`, commit f1d44266e5). -/
482
483/-- Real coordinates of a periodic vertex (its representative in
484`[0,N)³`). -/
485def vertCoord (x : Vertex N N N) : Fin 3 → ℝ
486 | 0 => (x.1.val : ℝ)
487 | 1 => (x.2.1.val : ℝ)
488 | 2 => (x.2.2.val : ℝ)
489
490/-- Edge-class coefficient of a polarization matrix:
491`c_d = Σ_{ij} E_ij · D_d^i · D_d^j` (how a metric perturbation `E` loads
492the squared length of displacement class `d`). -/
493def polEdgeCoeff (E : Fin 3 → Fin 3 → ℝ) (d : Fin 7) : ℝ :=
494 ∑ i : Fin 3, ∑ j : Fin 3, E i j * dispReal d i * dispReal d j
495
496/-- Commensurate momentum of an integer wave vector on the side-`N` torus:
497`k = 2π·m/N`. -/
498def commensurateMomentum (m : Fin 3 → ℤ) : Fin 3 → ℝ :=
499 fun i => 2 * Real.pi * (m i : ℝ) / (N : ℝ)
500
501/-- Midpoint Bloch phase of a periodic edge: `k · (x + D_d/2)` (the
502preregistered midpoint convention of the C10 probe). -/
503def edgeMidpointPhase (k : Fin 3 → ℝ) (e : PeriodicEdge N N N) : ℝ :=
504 ∑ i : Fin 3, k i * (vertCoord N e.base i + dispReal e.disp i / 2)
505
506/-- The plane-wave perturbation family at amplitude `t`:
507`ℓ_e(t) = ℓ²_flat(e) + t · c_d · cos(k·(x + D_d/2))`. -/
508def planeWaveEdgeField (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ) (t : ℝ) :
509 EdgeField N :=
510 fun e =>
511 periodicDispSqEdge e.disp +
512 t * polEdgeCoeff E e.disp * Real.cos (edgeMidpointPhase N k e)
513
514/-- The action along the plane-wave family, as a function of the
515amplitude. -/
516def planeWaveActionProfile (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
517 (t : ℝ) : ℝ :=
518 trueReggeAction N (planeWaveEdgeField N E k t)
519
520/-- Per-unit-cell second-difference quadratic form of the true action along
521the plane-wave family at amplitude `t`:
522`(2/N³) · (S(t) − 2·S(0) + S(−t)) / t²`. The `(2/N³)` normalization makes
523this the per-unit-cell Bloch quadratic form in the C10 conventions. -/
524def ttSecondDifference (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ) (t : ℝ) : ℝ :=
525 (2 / (N : ℝ) ^ (3 : ℕ)) *
526 (planeWaveActionProfile N E k t - 2 * planeWaveActionProfile N E k 0 +
527 planeWaveActionProfile N E k (-t)) / t ^ (2 : ℕ)
528
529/-- The TT Bloch symbol VALUE PREDICATE at side `N`, polarization `E`, and
530integer wave vector `m`: the amplitude second difference converges to `H`
531as the amplitude tends to `0` (punctured-neighborhood limit). DEFINITION
532ONLY; existence is not claimed anywhere in this file. -/
533def TTBlochSymbolIs (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ) (H : ℝ) : Prop :=
534 Filter.Tendsto
535 (fun t : ℝ => ttSecondDifference N E (commensurateMomentum N m) t)
536 (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds H)
537
538/-- Squared norm of the commensurate momentum, `|2π·m/N|²`. -/
539def momentumNormSq (m : Fin 3 → ℤ) : ℝ :=
540 ∑ i : Fin 3, commensurateMomentum N m i ^ (2 : ℕ)
541
542instance instNeZeroAddThree (j : ℕ) : NeZero (j + 3) := ⟨by omega⟩
543
544/-- THE CONTINUUM TT SYMBOL VALUE PREDICATE (`ReggeTTContinuumSymbol`
545program target object): `Λ` is the continuum TT Bloch symbol coefficient
546for polarization `E` and integer wave vector `m` when there are per-torus
547symbol values `H j` at sides `N = j + 3` (so `k_N = 2π·m/N → 0` at fixed
548direction) whose `|k_N|²`-normalized values converge to `Λ`. DEFINITION
549ONLY: neither existence of the `H j` nor convergence is claimed in this
550file; the C10 numerics supporting `Λ = -(1/4)` for TT polarizations remain
551NUMERICAL EVIDENCE. -/
552def ReggeTTContinuumSymbolIs (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ)
553 (Λ : ℝ) : Prop :=
554 ∃ H : ℕ → ℝ,
555 (∀ j : ℕ, TTBlochSymbolIs (j + 3) E m (H j)) ∧
556 Filter.Tendsto (fun j : ℕ => H j / momentumNormSq (j + 3) m)
557 Filter.atTop (nhds Λ)
558
559/-- TT polarization for the integer wave vector `m`: symmetric, traceless,
560transverse to `m`, Frobenius-normalized. -/
561def IsTTPolarization (m : Fin 3 → ℤ) (E : Fin 3 → Fin 3 → ℝ) : Prop :=
562 (∀ i j : Fin 3, E i j = E j i) ∧
563 (∑ i : Fin 3, E i i) = 0 ∧
564 (∀ j : Fin 3, (∑ i : Fin 3, (m i : ℝ) * E i j) = 0) ∧
565 (∑ i : Fin 3, ∑ j : Fin 3, E i j * E i j) = 1
566
567/-- The exact continuum coefficient reported by the C10 probe: `-(1/4)`,
568which is the linearized Einstein-Hilbert TT coefficient of
569`Σ ℓ·δ = (1/2)∫√g R` in these conventions. The VALUE of this constant is
570a definition; that the symbol ATTAINS it is the OPEN target below. -/
571def reggeTTContinuumCoefficient : ℝ := -(1 / 4)
572
573/-- **OPEN TARGET** (named, NOT proved, status flag `false`): for every
574nonzero integer wave vector and every TT polarization, the continuum TT
575Bloch symbol of the true Regge action exists and equals `-(1/4)` — i.e.
576the symbol is isotropic with exactly the linearized Einstein-Hilbert TT
577coefficient. Supporting evidence is NUMERICAL ONLY (C10 probe, commit
578f1d44266e5; critic sign-off 1e38531ee2: isotropy on all 14 preregistered
579directions and exact `-1/4` identification). Closing this Prop is the
580`ReggeTTContinuumSymbol` program's kernel goal. -/
581def ReggeTTContinuumIsotropyTarget : Prop :=
582 ∀ (m : Fin 3 → ℤ) (E : Fin 3 → Fin 3 → ℝ),
583 m ≠ 0 → IsTTPolarization m E →
584 ReggeTTContinuumSymbolIs E m reggeTTContinuumCoefficient
585
586/-! ## §5. Well-formedness and symmetry of the symbol object (d) — THEOREM -/
587
588/-- At amplitude `0` the plane-wave family sits at the flat field. -/
589theorem planeWaveEdgeField_zero_amplitude (E : Fin 3 → Fin 3 → ℝ)
590 (k : Fin 3 → ℝ) :
591 planeWaveEdgeField N E k 0 = flatEdgeField N := by
592 funext e
593 simp only [planeWaveEdgeField, flatEdgeField, zero_mul, add_zero]
594
595/-- The action profile vanishes at amplitude `0` (flat point of the
596family). -/
597theorem planeWaveActionProfile_zero (E : Fin 3 → Fin 3 → ℝ)
598 (k : Fin 3 → ℝ) :
599 planeWaveActionProfile N E k 0 = 0 := by
600 unfold planeWaveActionProfile
601 rw [planeWaveEdgeField_zero_amplitude, trueReggeAction_flatEdgeField]
602
603/-- The second-difference quadratic form is even in the amplitude. -/
604theorem ttSecondDifference_even (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
605 (t : ℝ) :
606 ttSecondDifference N E k (-t) = ttSecondDifference N E k t := by
607 unfold ttSecondDifference
608 rw [neg_neg, neg_sq]
609 ring
610
611/-- Negating the polarization negates every edge-class coefficient. -/
612theorem polEdgeCoeff_neg (E : Fin 3 → Fin 3 → ℝ) (d : Fin 7) :
613 polEdgeCoeff (fun i j => -E i j) d = -polEdgeCoeff E d := by
614 unfold polEdgeCoeff
615 rw [← Finset.sum_neg_distrib]
616 refine Finset.sum_congr rfl fun i _ => ?_
617 rw [← Finset.sum_neg_distrib]
618 refine Finset.sum_congr rfl fun j _ => ?_
619 ring
620
621/-- Negating the polarization is the same as negating the amplitude. -/
622theorem planeWaveEdgeField_neg_polarization (E : Fin 3 → Fin 3 → ℝ)
623 (k : Fin 3 → ℝ) (t : ℝ) :
624 planeWaveEdgeField N (fun i j => -E i j) k t =
625 planeWaveEdgeField N E k (-t) := by
626 funext e
627 simp only [planeWaveEdgeField]
628 rw [polEdgeCoeff_neg]
629 ring
630
631/-- Sign symmetry of the symbol object (THEOREM): the second-difference
632quadratic form is invariant under `E ↦ −E`, as a quadratic form must
633be. -/
634theorem ttSecondDifference_neg_polarization (E : Fin 3 → Fin 3 → ℝ)
635 (k : Fin 3 → ℝ) (t : ℝ) :
636 ttSecondDifference N (fun i j => -E i j) k t =
637 ttSecondDifference N E k t := by
638 unfold ttSecondDifference planeWaveActionProfile
639 rw [planeWaveEdgeField_neg_polarization,
640 planeWaveEdgeField_neg_polarization,
641 planeWaveEdgeField_neg_polarization, neg_neg, neg_zero]
642 ring
643
644/-! ## §6. Non-vacuity of the TT constraint set — THEOREM
645
646The OPEN target quantifies over `IsTTPolarization`; these witnesses prove
647the constraint set is nonempty for the preregistered axis direction, so the
648target is not vacuously closable. -/
649
650/-- The axis integer wave vector `(1,0,0)`. -/
651def axisWaveVector : Fin 3 → ℤ
652 | 0 => 1
653 | 1 => 0
654 | 2 => 0
655
656/-- The `+`-polarization for the axis direction:
657`diag(0, 1/√2, −1/√2)` (the C10 deterministic TT frame gives this pair up
658to sign), as an explicit entry table. -/
659def axisTTPolarizationPlus : Fin 3 → Fin 3 → ℝ
660 | 0, 0 => 0 | 0, 1 => 0 | 0, 2 => 0
661 | 1, 0 => 0 | 1, 1 => 1 / Real.sqrt 2 | 1, 2 => 0
662 | 2, 0 => 0 | 2, 1 => 0 | 2, 2 => -(1 / Real.sqrt 2)
663
664/-- The `×`-polarization for the axis direction: symmetric off-diagonal
665block on the transverse plane with entries `1/√2`, as an explicit entry
666table. -/
667def axisTTPolarizationCross : Fin 3 → Fin 3 → ℝ
668 | 0, 0 => 0 | 0, 1 => 0 | 0, 2 => 0
669 | 1, 0 => 0 | 1, 1 => 0 | 1, 2 => 1 / Real.sqrt 2
670 | 2, 0 => 0 | 2, 1 => 1 / Real.sqrt 2 | 2, 2 => 0
671
672theorem sqrt_two_mul_self : Real.sqrt 2 * Real.sqrt 2 = 2 :=
673 Real.mul_self_sqrt (by norm_num)
674
675theorem inv_sqrt_two_sq : (1 / Real.sqrt 2) * (1 / Real.sqrt 2) = 1 / 2 := by
676 rw [div_mul_div_comm, one_mul, sqrt_two_mul_self]
677
678/-- The `+`-witness is a TT polarization for the axis wave vector. -/
679theorem axisTTPolarizationPlus_isTT :
680 IsTTPolarization axisWaveVector axisTTPolarizationPlus := by
681 refine ⟨?_, ?_, ?_, ?_⟩
682 · intro i j
683 fin_cases i <;> fin_cases j <;>
684 simp only [axisTTPolarizationPlus]
685 · simp only [Fin.sum_univ_three, axisTTPolarizationPlus]
686 ring
687 · intro j
688 fin_cases j <;>
689 · simp only [Fin.sum_univ_three, axisTTPolarizationPlus,
690 axisWaveVector]
691 push_cast
692 ring
693 · simp only [Fin.sum_univ_three, axisTTPolarizationPlus]
694 linear_combination 2 * inv_sqrt_two_sq
695
696/-- The `×`-witness is a TT polarization for the axis wave vector. -/
697theorem axisTTPolarizationCross_isTT :
698 IsTTPolarization axisWaveVector axisTTPolarizationCross := by
699 refine ⟨?_, ?_, ?_, ?_⟩
700 · intro i j
701 fin_cases i <;> fin_cases j <;>
702 simp only [axisTTPolarizationCross]
703 · simp only [Fin.sum_univ_three, axisTTPolarizationCross]
704 ring
705 · intro j
706 fin_cases j <;>
707 · simp only [Fin.sum_univ_three, axisTTPolarizationCross,
708 axisWaveVector]
709 push_cast
710 ring
711 · simp only [Fin.sum_univ_three, axisTTPolarizationCross]
712 linear_combination 2 * inv_sqrt_two_sq
713
714/-- The axis wave vector is nonzero (so the witnesses instantiate the OPEN
715target's hypotheses non-vacuously). -/
716theorem axisWaveVector_ne_zero : axisWaveVector ≠ 0 := by
717 intro h
718 have h0 : axisWaveVector 0 = 0 := by rw [h]; rfl
719 simp only [axisWaveVector] at h0
720 exact one_ne_zero h0
721
722/-! ## §7. Status flags (documentation record) -/
723
724/-- Status flags for the Regge TT symbol preflight (PROTOCOL RECORD,
725documentation only; the mathematics lives in the theorems, see
726`status_flags_grounded`).
727
728Honest scope: this stage-1 record certifies the true-action definition,
729its kernel-checked flat point, the exact frozen-model identification along
730the conformal family, the well-formedness/symmetry lemmas of the TT Bloch
731symbol object, and the non-vacuity of the TT constraint set. The
732continuum symbol VALUE flag is `false`: `ReggeTTContinuumIsotropyTarget`
733is OPEN, and the C10 isotropy/`-1/4` result is NUMERICAL EVIDENCE only. -/
734structure ReggeTTSymbolPreflightStatus where
735 /-- `deficitOfField_flatEdgeField`: all deficits vanish at flat. -/
736 flat_deficit_zero : Bool
737 /-- `trueReggeAction_flatEdgeField`: the true action vanishes at flat. -/
738 flat_action_zero : Bool
739 /-- Grounded in `reggeAction_conformal_eq` (the REAL content: the frozen
740 conformal-ansatz action equals the true action on conformal fields), which
741 is exactly what `status_flags_grounded` certifies for this flag. The
742 companion `frozen_identification(_stencil)` decomposition is a definitional
743 tautology (see its docstring) and does NOT ground this flag. -/
744 frozen_identification_proved : Bool
745 /-- `ttSecondDifference_even` + `ttSecondDifference_neg_polarization` +
746 `planeWaveActionProfile_zero`: symbol-object well-formedness. -/
747 symbol_object_symmetries : Bool
748 /-- `axisTTPolarizationPlus_isTT` + `axisTTPolarizationCross_isTT` +
749 `axisWaveVector_ne_zero`: the TT constraint set is nonempty. -/
750 tt_constraint_set_nonvacuous : Bool
751 /-- `ReggeTTContinuumIsotropyTarget` is OPEN. MUST stay `false` until a
752 kernel proof of the continuum symbol value exists; the C10 numerics are
753 NUMERICAL EVIDENCE and cannot flip this flag. -/
754 continuum_symbol_value_proved : Bool
755
756/-- The canonical status record. Every `true` flag is grounded in its
757kernel theorem by `status_flags_grounded`; the continuum-value flag is
758`false` (OPEN). -/
759def reggeTTSymbolPreflightStatus : ReggeTTSymbolPreflightStatus where
760 flat_deficit_zero := true
761 flat_action_zero := true
762 frozen_identification_proved := true
763 symbol_object_symmetries := true
764 tt_constraint_set_nonvacuous := true
765 continuum_symbol_value_proved := false
766
767/-- The status flags are not bare Booleans: each `true` flag is tied to its
768kernel theorem (here instantiated at `N = 3`, the smallest torus the
769campaign uses; the theorems themselves hold for every `N`), and the OPEN
770flag is pinned to `false`. -/
771theorem status_flags_grounded :
772 (reggeTTSymbolPreflightStatus.flat_deficit_zero = true ∧
773 ∀ e : PeriodicEdge 3 3 3, deficitOfField 3 (flatEdgeField 3) e = 0) ∧
774 (reggeTTSymbolPreflightStatus.flat_action_zero = true ∧
775 trueReggeAction 3 (flatEdgeField 3) = 0) ∧
776 (reggeTTSymbolPreflightStatus.frozen_identification_proved = true ∧
777 ∀ u : Vertex 3 3 3 → ℝ,
778 reggeAction (canonicalPeriodicTriangulation 3 3 3)
779 (canonicalPeriodicIncidenceConsistent 3 3 3)
780 (toPotential 3 u) =
781 trueReggeAction 3 (typedConformalEdgeField 3 u)) ∧
782 (reggeTTSymbolPreflightStatus.symbol_object_symmetries = true ∧
783 ∀ (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ) (t : ℝ),
784 ttSecondDifference 3 E k (-t) = ttSecondDifference 3 E k t) ∧
785 (reggeTTSymbolPreflightStatus.tt_constraint_set_nonvacuous = true ∧
786 IsTTPolarization axisWaveVector axisTTPolarizationPlus) ∧
787 reggeTTSymbolPreflightStatus.continuum_symbol_value_proved = false :=
788 ⟨⟨rfl, deficitOfField_flatEdgeField 3⟩,
789 ⟨rfl, trueReggeAction_flatEdgeField 3⟩,
790 ⟨rfl, fun u => reggeAction_conformal_eq 3 u⟩,
791 ⟨rfl, fun E k t => ttSecondDifference_even 3 E k t⟩,
792 ⟨rfl, axisTTPolarizationPlus_isTT⟩,
793 rfl⟩
794
795end
796
797end ReggeTTSymbolPreflight
798end Analysis
799end Gravity
800end IndisputableMonolith
801