IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumCertificateSpike
IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumCertificateSpike.lean · 397 lines · 13 declarations
show as:
view math explainer →
1/-
2BOUNDED FEASIBILITY SPIKE -- NOT A CAMPAIGN MODULE, NOT A CONTINUUM THEOREM
3QG campaign, C10 follow-up spike (regge_tt_continuum_certificate), 2026-07-15.
4
5**WHAT THIS FILE PROVES AND WHAT IT DOES NOT.** This certificate proves an
6algebraic identity about an explicitly transcribed polynomial; the
7identification of that polynomial with the second variation / Bloch symbol of
8`trueReggeAction` is NOT proved here and the continuum target stays OPEN.
9
10The transcribed polynomial is the O(k^2) Bloch coefficient of the true Regge
11TT probe (commit f1d44266e5, state/qg_full_theory/true_regge_tt_probe/
12exact_limit.py):
13
14 Q(E, x) = (1/2) * sum_{tau=0..5} sum_{f,g=0..5}
15 G_fg * c_{d(tau,f)} * c_{d(tau,g)} * (x . (m_g - m_f))^2,
16 c_d = sum_{i,j} E_ij * D_d^i * D_d^j (7 displacement classes D_d),
17 m_f = midpoint offset of slot f in tet tau (SLOT_OFF + D/2),
18
19with G the exact per-tet flat Regge Hessian at a* = (1,2,3,1,2,1), whose
20entries live in QQ(sqrt 2, sqrt 3, pi). The 2*pi*L'' hinge diagonal of the
21real-space Hessian sits at zero midpoint offset (m_g - m_f = 0), so it does
22not appear in this O(k^2) moment form; per exact_limit.py's derivation it
23enters the O(1) term, which cancels by the flat zero mode (that cancellation
24is NOT re-proved here). K_inf uses G only, mirrored here EXACTLY (all 216
25(tau,f,g) terms including f = g, zero G entries kept as literal 0 factors).
26
27The LHS below is that literal per-tet sum with s2, s3, p COMPLETELY FREE real
28variables standing for sqrt 2, sqrt 3, pi. No hypotheses s2^2 = 2, s3^2 = 3
29or anything about p are needed. WHERE THE TRANSCENDENTALS GO (exact sympy
30finding): the pi / s2*p / s3*p entries of G occur ONLY on the diagonal
31f = g, and there the midpoint difference m_g - m_f vanishes, so every
32transcendental term carries a literal (0)^2 factor. They cancel BEFORE any
33TT reduction, and for this structural reason rather than by a cross-tet
34conspiracy; the assembled Q is a 30-term pure-QQ polynomial. The kernel
35still checks this since s2, s3, p are free variables that ring normalization
36must eliminate.
37
38The identity: on the TT variety (E symmetric, traceless, x-transverse),
39 Q(E, x) = -(1/4) * |x|^2 * ||E||_F^2
40for EVERY direction x and EVERY such E (no normalization needed, by
41bilinearity). Proof: an explicit cofactor certificate computed offline
42(sympy 1.14, exact QQ linear solve; /tmp scratch, gen_lean.py):
43 Q + (1/4)|x|^2 ||E||_F^2 = sum_a h_a * g_a
44with g_a the seven TT generators (3 symmetry, 1 trace, 3 transversality) and
45h_a explicit bihomogeneous QQ cofactors, passed to `linear_combination`.
46
47Offline cross-checks (sympy, exact):
48 - G matches the exact flat per-tet Hessian from stencil.py route B.
49 - assembled Q equals a 30-term pure-QQ polynomial (transcendentals cancel
50 pre-TT); certificate residual is exactly 0.
51 - all 14 preregistered directions give K = -(1/4) I_TT on exact TT bases.
52
53Do NOT import from campaign modules; do NOT cite as proof of the continuum
54-(1/4) TT symbol of `trueReggeAction`. Tier of the continuum claim remains
55NUMERICAL EVIDENCE (exact symbolic at the identity level, kernel-checked at
56the transcribed-polynomial level).
57-/
58import Mathlib.Data.Real.Basic
59import Mathlib.Tactic.Ring
60import Mathlib.Tactic.LinearCombination
61
62namespace IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumCertificateSpike
63
64set_option maxHeartbeats 1600000 in
65/-- Tet 0: LITERAL transcription of the 36 (f,g) terms of
66(1/2) * G_fg * c_(d(tau,f)) * c_(d(tau,g)) * (x.(m_g - m_f))^2. -/
67noncomputable def tetBlock0 (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ) : ℝ :=
68 (((1 : ℝ)/2) * (((-1 : ℝ)/16) * p) * (E00) * (E00) * (0 : ℝ)^2
69 + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E00 + E01 + E10 + E11) * (x1/2)^2
70 + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (x1/2 + x2/2)^2
71 + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E11) * (x0/2 + x1/2)^2
72 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00) * (E11 + E12 + E21 + E22) * (x0/2 + x1/2 + x2/2)^2
73 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E22) * (x0/2 + x1 + x2/2)^2
74 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E10 + E11) * (E00) * (-x1/2)^2
75 + ((1 : ℝ)/2) * (((-1 : ℝ)/32) * s2 * p + ((1 : ℝ)/8)) * (E00 + E01 + E10 + E11) * (E00 + E01 + E10 + E11) * (0 : ℝ)^2
76 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E10 + E11) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (x2/2)^2
77 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + E01 + E10 + E11) * (E11) * (x0/2)^2
78 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + E01 + E10 + E11) * (E11 + E12 + E21 + E22) * (x0/2 + x2/2)^2
79 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E10 + E11) * (E22) * (x0/2 + x1/2 + x2/2)^2
80 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00) * (-x1/2 - x2/2)^2
81 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00 + E01 + E10 + E11) * (-x2/2)^2
82 + ((1 : ℝ)/2) * (((-1 : ℝ)/108) * s3 * p + ((1 : ℝ)/12)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (0 : ℝ)^2
83 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E11) * (x0/2 - x2/2)^2
84 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E11 + E12 + E21 + E22) * (x0/2)^2
85 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E22) * (x0/2 + x1/2)^2
86 + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E00) * (-x0/2 - x1/2)^2
87 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11) * (E00 + E01 + E10 + E11) * (-x0/2)^2
88 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x0/2 + x2/2)^2
89 + ((1 : ℝ)/2) * (((-1 : ℝ)/8) * p + ((1 : ℝ)/4)) * (E11) * (E11) * (0 : ℝ)^2
90 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11) * (E11 + E12 + E21 + E22) * (x2/2)^2
91 + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E22) * (x1/2 + x2/2)^2
92 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + E12 + E21 + E22) * (E00) * (-x0/2 - x1/2 - x2/2)^2
93 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11 + E12 + E21 + E22) * (E00 + E01 + E10 + E11) * (-x0/2 - x2/2)^2
94 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + E12 + E21 + E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x0/2)^2
95 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11 + E12 + E21 + E22) * (E11) * (-x2/2)^2
96 + ((1 : ℝ)/2) * (((-1 : ℝ)/32) * s2 * p + ((1 : ℝ)/8)) * (E11 + E12 + E21 + E22) * (E11 + E12 + E21 + E22) * (0 : ℝ)^2
97 + ((1 : ℝ)/2) * (0 : ℝ) * (E11 + E12 + E21 + E22) * (E22) * (x1/2)^2
98 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E00) * (-x0/2 - x1 - x2/2)^2
99 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E22) * (E00 + E01 + E10 + E11) * (-x0/2 - x1/2 - x2/2)^2
100 + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x0/2 - x1/2)^2
101 + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E11) * (-x1/2 - x2/2)^2
102 + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E11 + E12 + E21 + E22) * (-x1/2)^2
103 + ((1 : ℝ)/2) * (((-1 : ℝ)/16) * p) * (E22) * (E22) * (0 : ℝ)^2)
104
105/-- Tet 0 collapses to a pure-QQ polynomial (every s2/s3/p entry of G
106carries a literal (0)^2 midpoint factor). -/
107theorem tetBlock0_eq (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ) :
108 tetBlock0 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p
109 =
110 (-E00^2*x2^2/32 - E00*E01*x2^2/16 - E00*E02*x2^2/32 - E00*E10*x2^2/16 - E00*E11*x0*x1/16 - E00*E11*x0*x2/16 - E00*E11*x1^2/32 - E00*E11*x1*x2/16 + E00*E11*x2^2/32 - E00*E12*x0*x1/16 + E00*E12*x0*x2/16 - E00*E12*x1^2/32 - E00*E12*x1*x2/16 - E00*E20*x2^2/32 - E00*E21*x0*x1/16 + E00*E21*x0*x2/16 - E00*E21*x1^2/32 - E00*E21*x1*x2/16 + E00*E22*x0^2/32 + E00*E22*x0*x1/8 + E00*E22*x0*x2/8 + 3*E00*E22*x1^2/16 + E00*E22*x1*x2/8 + E00*E22*x2^2/32 - E01^2*x2^2/32 - E01*E02*x2^2/32 - E01*E10*x2^2/16 + E01*E11*x0^2/32 + E01*E11*x2^2/16 + E01*E12*x0^2/32 + E01*E12*x0*x2/8 + E01*E12*x2^2/32 - E01*E20*x2^2/32 + E01*E21*x0^2/32 + E01*E21*x0*x2/8 + E01*E21*x2^2/32 - E01*E22*x0*x1/16 + E01*E22*x0*x2/16 - E01*E22*x1^2/32 - E01*E22*x1*x2/16 - E02*E10*x2^2/32 + E02*E11*x0^2/32 - E02*E11*x0*x2/8 + E02*E11*x2^2/32 - E02*E12*x0^2/32 - E02*E21*x0^2/32 - E02*E22*x0^2/32 - E10^2*x2^2/32 + E10*E11*x0^2/32 + E10*E11*x2^2/16 + E10*E12*x0^2/32 + E10*E12*x0*x2/8 + E10*E12*x2^2/32 - E10*E20*x2^2/32 + E10*E21*x0^2/32 + E10*E21*x0*x2/8 + E10*E21*x2^2/32 - E10*E22*x0*x1/16 + E10*E22*x0*x2/16 - E10*E22*x1^2/32 - E10*E22*x1*x2/16 + E11^2*x0^2/32 + E11^2*x2^2/32 + E11*E12*x0^2/16 + E11*E12*x2^2/32 + E11*E20*x0^2/32 - E11*E20*x0*x2/8 + E11*E20*x2^2/32 + E11*E21*x0^2/16 + E11*E21*x2^2/32 + E11*E22*x0^2/32 - E11*E22*x0*x1/16 - E11*E22*x0*x2/16 - E11*E22*x1^2/32 - E11*E22*x1*x2/16 - E12^2*x0^2/32 - E12*E20*x0^2/32 - E12*E21*x0^2/16 - E12*E22*x0^2/16 - E20*E21*x0^2/32 - E20*E22*x0^2/32 - E21^2*x0^2/32 - E21*E22*x0^2/16 - E22^2*x0^2/32) := by
111 unfold tetBlock0
112 ring
113
114set_option maxHeartbeats 1600000 in
115/-- Tet 1: LITERAL transcription of the 36 (f,g) terms of
116(1/2) * G_fg * c_(d(tau,f)) * c_(d(tau,g)) * (x.(m_g - m_f))^2. -/
117noncomputable def tetBlock1 (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ) : ℝ :=
118 (((1 : ℝ)/2) * (((-1 : ℝ)/16) * p) * (E00) * (E00) * (0 : ℝ)^2
119 + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E00 + E02 + E20 + E22) * (x2/2)^2
120 + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (x1/2 + x2/2)^2
121 + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E22) * (x0/2 + x2/2)^2
122 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00) * (E11 + E12 + E21 + E22) * (x0/2 + x1/2 + x2/2)^2
123 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E11) * (x0/2 + x1/2 + x2)^2
124 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E02 + E20 + E22) * (E00) * (-x2/2)^2
125 + ((1 : ℝ)/2) * (((-1 : ℝ)/32) * s2 * p + ((1 : ℝ)/8)) * (E00 + E02 + E20 + E22) * (E00 + E02 + E20 + E22) * (0 : ℝ)^2
126 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E02 + E20 + E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (x1/2)^2
127 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + E02 + E20 + E22) * (E22) * (x0/2)^2
128 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + E02 + E20 + E22) * (E11 + E12 + E21 + E22) * (x0/2 + x1/2)^2
129 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E02 + E20 + E22) * (E11) * (x0/2 + x1/2 + x2/2)^2
130 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00) * (-x1/2 - x2/2)^2
131 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00 + E02 + E20 + E22) * (-x1/2)^2
132 + ((1 : ℝ)/2) * (((-1 : ℝ)/108) * s3 * p + ((1 : ℝ)/12)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (0 : ℝ)^2
133 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E22) * (x0/2 - x1/2)^2
134 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E11 + E12 + E21 + E22) * (x0/2)^2
135 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E11) * (x0/2 + x2/2)^2
136 + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E00) * (-x0/2 - x2/2)^2
137 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E22) * (E00 + E02 + E20 + E22) * (-x0/2)^2
138 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x0/2 + x1/2)^2
139 + ((1 : ℝ)/2) * (((-1 : ℝ)/8) * p + ((1 : ℝ)/4)) * (E22) * (E22) * (0 : ℝ)^2
140 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E22) * (E11 + E12 + E21 + E22) * (x1/2)^2
141 + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E11) * (x1/2 + x2/2)^2
142 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + E12 + E21 + E22) * (E00) * (-x0/2 - x1/2 - x2/2)^2
143 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11 + E12 + E21 + E22) * (E00 + E02 + E20 + E22) * (-x0/2 - x1/2)^2
144 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + E12 + E21 + E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x0/2)^2
145 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11 + E12 + E21 + E22) * (E22) * (-x1/2)^2
146 + ((1 : ℝ)/2) * (((-1 : ℝ)/32) * s2 * p + ((1 : ℝ)/8)) * (E11 + E12 + E21 + E22) * (E11 + E12 + E21 + E22) * (0 : ℝ)^2
147 + ((1 : ℝ)/2) * (0 : ℝ) * (E11 + E12 + E21 + E22) * (E11) * (x2/2)^2
148 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E00) * (-x0/2 - x1/2 - x2)^2
149 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11) * (E00 + E02 + E20 + E22) * (-x0/2 - x1/2 - x2/2)^2
150 + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x0/2 - x2/2)^2
151 + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E22) * (-x1/2 - x2/2)^2
152 + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E11 + E12 + E21 + E22) * (-x2/2)^2
153 + ((1 : ℝ)/2) * (((-1 : ℝ)/16) * p) * (E11) * (E11) * (0 : ℝ)^2)
154
155/-- Tet 1 collapses to a pure-QQ polynomial (every s2/s3/p entry of G
156carries a literal (0)^2 midpoint factor). -/
157theorem tetBlock1_eq (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ) :
158 tetBlock1 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p
159 =
160 (-E00^2*x1^2/32 - E00*E01*x1^2/32 - E00*E02*x1^2/16 - E00*E10*x1^2/32 + E00*E11*x0^2/32 + E00*E11*x0*x1/8 + E00*E11*x0*x2/8 + E00*E11*x1^2/32 + E00*E11*x1*x2/8 + 3*E00*E11*x2^2/16 + E00*E12*x0*x1/16 - E00*E12*x0*x2/16 - E00*E12*x1*x2/16 - E00*E12*x2^2/32 - E00*E20*x1^2/16 + E00*E21*x0*x1/16 - E00*E21*x0*x2/16 - E00*E21*x1*x2/16 - E00*E21*x2^2/32 - E00*E22*x0*x1/16 - E00*E22*x0*x2/16 + E00*E22*x1^2/32 - E00*E22*x1*x2/16 - E00*E22*x2^2/32 - E01*E02*x1^2/32 - E01*E11*x0^2/32 - E01*E12*x0^2/32 - E01*E20*x1^2/32 - E01*E21*x0^2/32 + E01*E22*x0^2/32 - E01*E22*x0*x1/8 + E01*E22*x1^2/32 - E02^2*x1^2/32 - E02*E10*x1^2/32 + E02*E11*x0*x1/16 - E02*E11*x0*x2/16 - E02*E11*x1*x2/16 - E02*E11*x2^2/32 + E02*E12*x0^2/32 + E02*E12*x0*x1/8 + E02*E12*x1^2/32 - E02*E20*x1^2/16 + E02*E21*x0^2/32 + E02*E21*x0*x1/8 + E02*E21*x1^2/32 + E02*E22*x0^2/32 + E02*E22*x1^2/16 - E10*E11*x0^2/32 - E10*E12*x0^2/32 - E10*E20*x1^2/32 - E10*E21*x0^2/32 + E10*E22*x0^2/32 - E10*E22*x0*x1/8 + E10*E22*x1^2/32 - E11^2*x0^2/32 - E11*E12*x0^2/16 + E11*E20*x0*x1/16 - E11*E20*x0*x2/16 - E11*E20*x1*x2/16 - E11*E20*x2^2/32 - E11*E21*x0^2/16 + E11*E22*x0^2/32 - E11*E22*x0*x1/16 - E11*E22*x0*x2/16 - E11*E22*x1*x2/16 - E11*E22*x2^2/32 - E12^2*x0^2/32 + E12*E20*x0^2/32 + E12*E20*x0*x1/8 + E12*E20*x1^2/32 - E12*E21*x0^2/16 + E12*E22*x0^2/16 + E12*E22*x1^2/32 - E20^2*x1^2/32 + E20*E21*x0^2/32 + E20*E21*x0*x1/8 + E20*E21*x1^2/32 + E20*E22*x0^2/32 + E20*E22*x1^2/16 - E21^2*x0^2/32 + E21*E22*x0^2/16 + E21*E22*x1^2/32 + E22^2*x0^2/32 + E22^2*x1^2/32) := by
161 unfold tetBlock1
162 ring
163
164set_option maxHeartbeats 1600000 in
165/-- Tet 2: LITERAL transcription of the 36 (f,g) terms of
166(1/2) * G_fg * c_(d(tau,f)) * c_(d(tau,g)) * (x.(m_g - m_f))^2. -/
167noncomputable def tetBlock2 (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ) : ℝ :=
168 (((1 : ℝ)/2) * (((-1 : ℝ)/16) * p) * (E11) * (E11) * (0 : ℝ)^2
169 + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E00 + E01 + E10 + E11) * (x0/2)^2
170 + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (x0/2 + x2/2)^2
171 + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E00) * (x0/2 + x1/2)^2
172 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11) * (E00 + E02 + E20 + E22) * (x0/2 + x1/2 + x2/2)^2
173 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E22) * (x0 + x1/2 + x2/2)^2
174 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E10 + E11) * (E11) * (-x0/2)^2
175 + ((1 : ℝ)/2) * (((-1 : ℝ)/32) * s2 * p + ((1 : ℝ)/8)) * (E00 + E01 + E10 + E11) * (E00 + E01 + E10 + E11) * (0 : ℝ)^2
176 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E10 + E11) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (x2/2)^2
177 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + E01 + E10 + E11) * (E00) * (x1/2)^2
178 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + E01 + E10 + E11) * (E00 + E02 + E20 + E22) * (x1/2 + x2/2)^2
179 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E10 + E11) * (E22) * (x0/2 + x1/2 + x2/2)^2
180 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E11) * (-x0/2 - x2/2)^2
181 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00 + E01 + E10 + E11) * (-x2/2)^2
182 + ((1 : ℝ)/2) * (((-1 : ℝ)/108) * s3 * p + ((1 : ℝ)/12)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (0 : ℝ)^2
183 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00) * (x1/2 - x2/2)^2
184 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00 + E02 + E20 + E22) * (x1/2)^2
185 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E22) * (x0/2 + x1/2)^2
186 + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E11) * (-x0/2 - x1/2)^2
187 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00) * (E00 + E01 + E10 + E11) * (-x1/2)^2
188 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x1/2 + x2/2)^2
189 + ((1 : ℝ)/2) * (((-1 : ℝ)/8) * p + ((1 : ℝ)/4)) * (E00) * (E00) * (0 : ℝ)^2
190 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00) * (E00 + E02 + E20 + E22) * (x2/2)^2
191 + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E22) * (x0/2 + x2/2)^2
192 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E02 + E20 + E22) * (E11) * (-x0/2 - x1/2 - x2/2)^2
193 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + E02 + E20 + E22) * (E00 + E01 + E10 + E11) * (-x1/2 - x2/2)^2
194 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E02 + E20 + E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x1/2)^2
195 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + E02 + E20 + E22) * (E00) * (-x2/2)^2
196 + ((1 : ℝ)/2) * (((-1 : ℝ)/32) * s2 * p + ((1 : ℝ)/8)) * (E00 + E02 + E20 + E22) * (E00 + E02 + E20 + E22) * (0 : ℝ)^2
197 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E02 + E20 + E22) * (E22) * (x0/2)^2
198 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E11) * (-x0 - x1/2 - x2/2)^2
199 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E22) * (E00 + E01 + E10 + E11) * (-x0/2 - x1/2 - x2/2)^2
200 + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x0/2 - x1/2)^2
201 + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E00) * (-x0/2 - x2/2)^2
202 + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E00 + E02 + E20 + E22) * (-x0/2)^2
203 + ((1 : ℝ)/2) * (((-1 : ℝ)/16) * p) * (E22) * (E22) * (0 : ℝ)^2)
204
205/-- Tet 2 collapses to a pure-QQ polynomial (every s2/s3/p entry of G
206carries a literal (0)^2 midpoint factor). -/
207theorem tetBlock2_eq (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ) :
208 tetBlock2 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p
209 =
210 (E00^2*x1^2/32 + E00^2*x2^2/32 + E00*E01*x1^2/32 + E00*E01*x2^2/16 + E00*E02*x1^2/16 + E00*E02*x2^2/32 + E00*E10*x1^2/32 + E00*E10*x2^2/16 - E00*E11*x0^2/32 - E00*E11*x0*x1/16 - E00*E11*x0*x2/16 - E00*E11*x1*x2/16 + E00*E11*x2^2/32 + E00*E12*x1^2/32 - E00*E12*x1*x2/8 + E00*E12*x2^2/32 + E00*E20*x1^2/16 + E00*E20*x2^2/32 + E00*E21*x1^2/32 - E00*E21*x1*x2/8 + E00*E21*x2^2/32 - E00*E22*x0^2/32 - E00*E22*x0*x1/16 - E00*E22*x0*x2/16 + E00*E22*x1^2/32 - E00*E22*x1*x2/16 - E01^2*x2^2/32 + E01*E02*x1^2/32 + E01*E02*x1*x2/8 + E01*E02*x2^2/32 - E01*E10*x2^2/16 - E01*E11*x2^2/16 - E01*E12*x2^2/32 + E01*E20*x1^2/32 + E01*E20*x1*x2/8 + E01*E20*x2^2/32 - E01*E21*x2^2/32 - E01*E22*x0^2/32 - E01*E22*x0*x1/16 - E01*E22*x0*x2/16 + E01*E22*x1*x2/16 - E02^2*x1^2/32 + E02*E10*x1^2/32 + E02*E10*x1*x2/8 + E02*E10*x2^2/32 - E02*E11*x0^2/32 - E02*E11*x0*x1/16 - E02*E11*x0*x2/16 + E02*E11*x1*x2/16 - E02*E12*x1^2/32 - E02*E20*x1^2/16 - E02*E21*x1^2/32 - E02*E22*x1^2/16 - E10^2*x2^2/32 - E10*E11*x2^2/16 - E10*E12*x2^2/32 + E10*E20*x1^2/32 + E10*E20*x1*x2/8 + E10*E20*x2^2/32 - E10*E21*x2^2/32 - E10*E22*x0^2/32 - E10*E22*x0*x1/16 - E10*E22*x0*x2/16 + E10*E22*x1*x2/16 - E11^2*x2^2/32 - E11*E12*x2^2/32 - E11*E20*x0^2/32 - E11*E20*x0*x1/16 - E11*E20*x0*x2/16 + E11*E20*x1*x2/16 - E11*E21*x2^2/32 + 3*E11*E22*x0^2/16 + E11*E22*x0*x1/8 + E11*E22*x0*x2/8 + E11*E22*x1^2/32 + E11*E22*x1*x2/8 + E11*E22*x2^2/32 - E12*E20*x1^2/32 - E12*E22*x1^2/32 - E20^2*x1^2/32 - E20*E21*x1^2/32 - E20*E22*x1^2/16 - E21*E22*x1^2/32 - E22^2*x1^2/32) := by
211 unfold tetBlock2
212 ring
213
214set_option maxHeartbeats 1600000 in
215/-- Tet 3: LITERAL transcription of the 36 (f,g) terms of
216(1/2) * G_fg * c_(d(tau,f)) * c_(d(tau,g)) * (x.(m_g - m_f))^2. -/
217noncomputable def tetBlock3 (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ) : ℝ :=
218 (((1 : ℝ)/2) * (((-1 : ℝ)/16) * p) * (E11) * (E11) * (0 : ℝ)^2
219 + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E11 + E12 + E21 + E22) * (x2/2)^2
220 + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (x0/2 + x2/2)^2
221 + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E22) * (x1/2 + x2/2)^2
222 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11) * (E00 + E02 + E20 + E22) * (x0/2 + x1/2 + x2/2)^2
223 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E00) * (x0/2 + x1/2 + x2)^2
224 + ((1 : ℝ)/2) * (0 : ℝ) * (E11 + E12 + E21 + E22) * (E11) * (-x2/2)^2
225 + ((1 : ℝ)/2) * (((-1 : ℝ)/32) * s2 * p + ((1 : ℝ)/8)) * (E11 + E12 + E21 + E22) * (E11 + E12 + E21 + E22) * (0 : ℝ)^2
226 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + E12 + E21 + E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (x0/2)^2
227 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11 + E12 + E21 + E22) * (E22) * (x1/2)^2
228 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11 + E12 + E21 + E22) * (E00 + E02 + E20 + E22) * (x0/2 + x1/2)^2
229 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + E12 + E21 + E22) * (E00) * (x0/2 + x1/2 + x2/2)^2
230 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E11) * (-x0/2 - x2/2)^2
231 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E11 + E12 + E21 + E22) * (-x0/2)^2
232 + ((1 : ℝ)/2) * (((-1 : ℝ)/108) * s3 * p + ((1 : ℝ)/12)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (0 : ℝ)^2
233 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E22) * (-x0/2 + x1/2)^2
234 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00 + E02 + E20 + E22) * (x1/2)^2
235 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00) * (x1/2 + x2/2)^2
236 + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E11) * (-x1/2 - x2/2)^2
237 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E22) * (E11 + E12 + E21 + E22) * (-x1/2)^2
238 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (x0/2 - x1/2)^2
239 + ((1 : ℝ)/2) * (((-1 : ℝ)/8) * p + ((1 : ℝ)/4)) * (E22) * (E22) * (0 : ℝ)^2
240 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E22) * (E00 + E02 + E20 + E22) * (x0/2)^2
241 + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E00) * (x0/2 + x2/2)^2
242 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E02 + E20 + E22) * (E11) * (-x0/2 - x1/2 - x2/2)^2
243 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + E02 + E20 + E22) * (E11 + E12 + E21 + E22) * (-x0/2 - x1/2)^2
244 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E02 + E20 + E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x1/2)^2
245 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + E02 + E20 + E22) * (E22) * (-x0/2)^2
246 + ((1 : ℝ)/2) * (((-1 : ℝ)/32) * s2 * p + ((1 : ℝ)/8)) * (E00 + E02 + E20 + E22) * (E00 + E02 + E20 + E22) * (0 : ℝ)^2
247 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E02 + E20 + E22) * (E00) * (x2/2)^2
248 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E11) * (-x0/2 - x1/2 - x2)^2
249 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00) * (E11 + E12 + E21 + E22) * (-x0/2 - x1/2 - x2/2)^2
250 + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x1/2 - x2/2)^2
251 + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E22) * (-x0/2 - x2/2)^2
252 + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E00 + E02 + E20 + E22) * (-x2/2)^2
253 + ((1 : ℝ)/2) * (((-1 : ℝ)/16) * p) * (E00) * (E00) * (0 : ℝ)^2)
254
255/-- Tet 3 collapses to a pure-QQ polynomial (every s2/s3/p entry of G
256carries a literal (0)^2 midpoint factor). -/
257theorem tetBlock3_eq (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ) :
258 tetBlock3 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p
259 =
260 (-E00^2*x1^2/32 - E00*E01*x1^2/32 - E00*E02*x1^2/16 - E00*E10*x1^2/32 + E00*E11*x0^2/32 + E00*E11*x0*x1/8 + E00*E11*x0*x2/8 + E00*E11*x1^2/32 + E00*E11*x1*x2/8 + 3*E00*E11*x2^2/16 + E00*E12*x0*x1/16 - E00*E12*x0*x2/16 - E00*E12*x1*x2/16 - E00*E12*x2^2/32 - E00*E20*x1^2/16 + E00*E21*x0*x1/16 - E00*E21*x0*x2/16 - E00*E21*x1*x2/16 - E00*E21*x2^2/32 - E00*E22*x0*x1/16 - E00*E22*x0*x2/16 + E00*E22*x1^2/32 - E00*E22*x1*x2/16 - E00*E22*x2^2/32 - E01*E02*x1^2/32 - E01*E11*x0^2/32 - E01*E12*x0^2/32 - E01*E20*x1^2/32 - E01*E21*x0^2/32 + E01*E22*x0^2/32 - E01*E22*x0*x1/8 + E01*E22*x1^2/32 - E02^2*x1^2/32 - E02*E10*x1^2/32 + E02*E11*x0*x1/16 - E02*E11*x0*x2/16 - E02*E11*x1*x2/16 - E02*E11*x2^2/32 + E02*E12*x0^2/32 + E02*E12*x0*x1/8 + E02*E12*x1^2/32 - E02*E20*x1^2/16 + E02*E21*x0^2/32 + E02*E21*x0*x1/8 + E02*E21*x1^2/32 + E02*E22*x0^2/32 + E02*E22*x1^2/16 - E10*E11*x0^2/32 - E10*E12*x0^2/32 - E10*E20*x1^2/32 - E10*E21*x0^2/32 + E10*E22*x0^2/32 - E10*E22*x0*x1/8 + E10*E22*x1^2/32 - E11^2*x0^2/32 - E11*E12*x0^2/16 + E11*E20*x0*x1/16 - E11*E20*x0*x2/16 - E11*E20*x1*x2/16 - E11*E20*x2^2/32 - E11*E21*x0^2/16 + E11*E22*x0^2/32 - E11*E22*x0*x1/16 - E11*E22*x0*x2/16 - E11*E22*x1*x2/16 - E11*E22*x2^2/32 - E12^2*x0^2/32 + E12*E20*x0^2/32 + E12*E20*x0*x1/8 + E12*E20*x1^2/32 - E12*E21*x0^2/16 + E12*E22*x0^2/16 + E12*E22*x1^2/32 - E20^2*x1^2/32 + E20*E21*x0^2/32 + E20*E21*x0*x1/8 + E20*E21*x1^2/32 + E20*E22*x0^2/32 + E20*E22*x1^2/16 - E21^2*x0^2/32 + E21*E22*x0^2/16 + E21*E22*x1^2/32 + E22^2*x0^2/32 + E22^2*x1^2/32) := by
261 unfold tetBlock3
262 ring
263
264set_option maxHeartbeats 1600000 in
265/-- Tet 4: LITERAL transcription of the 36 (f,g) terms of
266(1/2) * G_fg * c_(d(tau,f)) * c_(d(tau,g)) * (x.(m_g - m_f))^2. -/
267noncomputable def tetBlock4 (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ) : ℝ :=
268 (((1 : ℝ)/2) * (((-1 : ℝ)/16) * p) * (E22) * (E22) * (0 : ℝ)^2
269 + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E00 + E02 + E20 + E22) * (x0/2)^2
270 + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (x0/2 + x1/2)^2
271 + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E00) * (x0/2 + x2/2)^2
272 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E22) * (E00 + E01 + E10 + E11) * (x0/2 + x1/2 + x2/2)^2
273 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E11) * (x0 + x1/2 + x2/2)^2
274 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E02 + E20 + E22) * (E22) * (-x0/2)^2
275 + ((1 : ℝ)/2) * (((-1 : ℝ)/32) * s2 * p + ((1 : ℝ)/8)) * (E00 + E02 + E20 + E22) * (E00 + E02 + E20 + E22) * (0 : ℝ)^2
276 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E02 + E20 + E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (x1/2)^2
277 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + E02 + E20 + E22) * (E00) * (x2/2)^2
278 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + E02 + E20 + E22) * (E00 + E01 + E10 + E11) * (x1/2 + x2/2)^2
279 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E02 + E20 + E22) * (E11) * (x0/2 + x1/2 + x2/2)^2
280 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E22) * (-x0/2 - x1/2)^2
281 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00 + E02 + E20 + E22) * (-x1/2)^2
282 + ((1 : ℝ)/2) * (((-1 : ℝ)/108) * s3 * p + ((1 : ℝ)/12)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (0 : ℝ)^2
283 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00) * (-x1/2 + x2/2)^2
284 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00 + E01 + E10 + E11) * (x2/2)^2
285 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E11) * (x0/2 + x2/2)^2
286 + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E22) * (-x0/2 - x2/2)^2
287 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00) * (E00 + E02 + E20 + E22) * (-x2/2)^2
288 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (x1/2 - x2/2)^2
289 + ((1 : ℝ)/2) * (((-1 : ℝ)/8) * p + ((1 : ℝ)/4)) * (E00) * (E00) * (0 : ℝ)^2
290 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00) * (E00 + E01 + E10 + E11) * (x1/2)^2
291 + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E11) * (x0/2 + x1/2)^2
292 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E10 + E11) * (E22) * (-x0/2 - x1/2 - x2/2)^2
293 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + E01 + E10 + E11) * (E00 + E02 + E20 + E22) * (-x1/2 - x2/2)^2
294 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E10 + E11) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x2/2)^2
295 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + E01 + E10 + E11) * (E00) * (-x1/2)^2
296 + ((1 : ℝ)/2) * (((-1 : ℝ)/32) * s2 * p + ((1 : ℝ)/8)) * (E00 + E01 + E10 + E11) * (E00 + E01 + E10 + E11) * (0 : ℝ)^2
297 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E10 + E11) * (E11) * (x0/2)^2
298 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E22) * (-x0 - x1/2 - x2/2)^2
299 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11) * (E00 + E02 + E20 + E22) * (-x0/2 - x1/2 - x2/2)^2
300 + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x0/2 - x2/2)^2
301 + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E00) * (-x0/2 - x1/2)^2
302 + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E00 + E01 + E10 + E11) * (-x0/2)^2
303 + ((1 : ℝ)/2) * (((-1 : ℝ)/16) * p) * (E11) * (E11) * (0 : ℝ)^2)
304
305/-- Tet 4 collapses to a pure-QQ polynomial (every s2/s3/p entry of G
306carries a literal (0)^2 midpoint factor). -/
307theorem tetBlock4_eq (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ) :
308 tetBlock4 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p
309 =
310 (E00^2*x1^2/32 + E00^2*x2^2/32 + E00*E01*x1^2/32 + E00*E01*x2^2/16 + E00*E02*x1^2/16 + E00*E02*x2^2/32 + E00*E10*x1^2/32 + E00*E10*x2^2/16 - E00*E11*x0^2/32 - E00*E11*x0*x1/16 - E00*E11*x0*x2/16 - E00*E11*x1*x2/16 + E00*E11*x2^2/32 + E00*E12*x1^2/32 - E00*E12*x1*x2/8 + E00*E12*x2^2/32 + E00*E20*x1^2/16 + E00*E20*x2^2/32 + E00*E21*x1^2/32 - E00*E21*x1*x2/8 + E00*E21*x2^2/32 - E00*E22*x0^2/32 - E00*E22*x0*x1/16 - E00*E22*x0*x2/16 + E00*E22*x1^2/32 - E00*E22*x1*x2/16 - E01^2*x2^2/32 + E01*E02*x1^2/32 + E01*E02*x1*x2/8 + E01*E02*x2^2/32 - E01*E10*x2^2/16 - E01*E11*x2^2/16 - E01*E12*x2^2/32 + E01*E20*x1^2/32 + E01*E20*x1*x2/8 + E01*E20*x2^2/32 - E01*E21*x2^2/32 - E01*E22*x0^2/32 - E01*E22*x0*x1/16 - E01*E22*x0*x2/16 + E01*E22*x1*x2/16 - E02^2*x1^2/32 + E02*E10*x1^2/32 + E02*E10*x1*x2/8 + E02*E10*x2^2/32 - E02*E11*x0^2/32 - E02*E11*x0*x1/16 - E02*E11*x0*x2/16 + E02*E11*x1*x2/16 - E02*E12*x1^2/32 - E02*E20*x1^2/16 - E02*E21*x1^2/32 - E02*E22*x1^2/16 - E10^2*x2^2/32 - E10*E11*x2^2/16 - E10*E12*x2^2/32 + E10*E20*x1^2/32 + E10*E20*x1*x2/8 + E10*E20*x2^2/32 - E10*E21*x2^2/32 - E10*E22*x0^2/32 - E10*E22*x0*x1/16 - E10*E22*x0*x2/16 + E10*E22*x1*x2/16 - E11^2*x2^2/32 - E11*E12*x2^2/32 - E11*E20*x0^2/32 - E11*E20*x0*x1/16 - E11*E20*x0*x2/16 + E11*E20*x1*x2/16 - E11*E21*x2^2/32 + 3*E11*E22*x0^2/16 + E11*E22*x0*x1/8 + E11*E22*x0*x2/8 + E11*E22*x1^2/32 + E11*E22*x1*x2/8 + E11*E22*x2^2/32 - E12*E20*x1^2/32 - E12*E22*x1^2/32 - E20^2*x1^2/32 - E20*E21*x1^2/32 - E20*E22*x1^2/16 - E21*E22*x1^2/32 - E22^2*x1^2/32) := by
311 unfold tetBlock4
312 ring
313
314set_option maxHeartbeats 1600000 in
315/-- Tet 5: LITERAL transcription of the 36 (f,g) terms of
316(1/2) * G_fg * c_(d(tau,f)) * c_(d(tau,g)) * (x.(m_g - m_f))^2. -/
317noncomputable def tetBlock5 (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ) : ℝ :=
318 (((1 : ℝ)/2) * (((-1 : ℝ)/16) * p) * (E22) * (E22) * (0 : ℝ)^2
319 + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E11 + E12 + E21 + E22) * (x1/2)^2
320 + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (x0/2 + x1/2)^2
321 + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E11) * (x1/2 + x2/2)^2
322 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E22) * (E00 + E01 + E10 + E11) * (x0/2 + x1/2 + x2/2)^2
323 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E00) * (x0/2 + x1 + x2/2)^2
324 + ((1 : ℝ)/2) * (0 : ℝ) * (E11 + E12 + E21 + E22) * (E22) * (-x1/2)^2
325 + ((1 : ℝ)/2) * (((-1 : ℝ)/32) * s2 * p + ((1 : ℝ)/8)) * (E11 + E12 + E21 + E22) * (E11 + E12 + E21 + E22) * (0 : ℝ)^2
326 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + E12 + E21 + E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (x0/2)^2
327 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11 + E12 + E21 + E22) * (E11) * (x2/2)^2
328 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11 + E12 + E21 + E22) * (E00 + E01 + E10 + E11) * (x0/2 + x2/2)^2
329 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + E12 + E21 + E22) * (E00) * (x0/2 + x1/2 + x2/2)^2
330 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E22) * (-x0/2 - x1/2)^2
331 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E11 + E12 + E21 + E22) * (-x0/2)^2
332 + ((1 : ℝ)/2) * (((-1 : ℝ)/108) * s3 * p + ((1 : ℝ)/12)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (0 : ℝ)^2
333 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E11) * (-x0/2 + x2/2)^2
334 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00 + E01 + E10 + E11) * (x2/2)^2
335 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00) * (x1/2 + x2/2)^2
336 + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E22) * (-x1/2 - x2/2)^2
337 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11) * (E11 + E12 + E21 + E22) * (-x2/2)^2
338 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (x0/2 - x2/2)^2
339 + ((1 : ℝ)/2) * (((-1 : ℝ)/8) * p + ((1 : ℝ)/4)) * (E11) * (E11) * (0 : ℝ)^2
340 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11) * (E00 + E01 + E10 + E11) * (x0/2)^2
341 + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E00) * (x0/2 + x1/2)^2
342 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E10 + E11) * (E22) * (-x0/2 - x1/2 - x2/2)^2
343 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + E01 + E10 + E11) * (E11 + E12 + E21 + E22) * (-x0/2 - x2/2)^2
344 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E10 + E11) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x2/2)^2
345 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + E01 + E10 + E11) * (E11) * (-x0/2)^2
346 + ((1 : ℝ)/2) * (((-1 : ℝ)/32) * s2 * p + ((1 : ℝ)/8)) * (E00 + E01 + E10 + E11) * (E00 + E01 + E10 + E11) * (0 : ℝ)^2
347 + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E10 + E11) * (E00) * (x1/2)^2
348 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E22) * (-x0/2 - x1 - x2/2)^2
349 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00) * (E11 + E12 + E21 + E22) * (-x0/2 - x1/2 - x2/2)^2
350 + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x1/2 - x2/2)^2
351 + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E11) * (-x0/2 - x1/2)^2
352 + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E00 + E01 + E10 + E11) * (-x1/2)^2
353 + ((1 : ℝ)/2) * (((-1 : ℝ)/16) * p) * (E00) * (E00) * (0 : ℝ)^2)
354
355/-- Tet 5 collapses to a pure-QQ polynomial (every s2/s3/p entry of G
356carries a literal (0)^2 midpoint factor). -/
357theorem tetBlock5_eq (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ) :
358 tetBlock5 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p
359 =
360 (-E00^2*x2^2/32 - E00*E01*x2^2/16 - E00*E02*x2^2/32 - E00*E10*x2^2/16 - E00*E11*x0*x1/16 - E00*E11*x0*x2/16 - E00*E11*x1^2/32 - E00*E11*x1*x2/16 + E00*E11*x2^2/32 - E00*E12*x0*x1/16 + E00*E12*x0*x2/16 - E00*E12*x1^2/32 - E00*E12*x1*x2/16 - E00*E20*x2^2/32 - E00*E21*x0*x1/16 + E00*E21*x0*x2/16 - E00*E21*x1^2/32 - E00*E21*x1*x2/16 + E00*E22*x0^2/32 + E00*E22*x0*x1/8 + E00*E22*x0*x2/8 + 3*E00*E22*x1^2/16 + E00*E22*x1*x2/8 + E00*E22*x2^2/32 - E01^2*x2^2/32 - E01*E02*x2^2/32 - E01*E10*x2^2/16 + E01*E11*x0^2/32 + E01*E11*x2^2/16 + E01*E12*x0^2/32 + E01*E12*x0*x2/8 + E01*E12*x2^2/32 - E01*E20*x2^2/32 + E01*E21*x0^2/32 + E01*E21*x0*x2/8 + E01*E21*x2^2/32 - E01*E22*x0*x1/16 + E01*E22*x0*x2/16 - E01*E22*x1^2/32 - E01*E22*x1*x2/16 - E02*E10*x2^2/32 + E02*E11*x0^2/32 - E02*E11*x0*x2/8 + E02*E11*x2^2/32 - E02*E12*x0^2/32 - E02*E21*x0^2/32 - E02*E22*x0^2/32 - E10^2*x2^2/32 + E10*E11*x0^2/32 + E10*E11*x2^2/16 + E10*E12*x0^2/32 + E10*E12*x0*x2/8 + E10*E12*x2^2/32 - E10*E20*x2^2/32 + E10*E21*x0^2/32 + E10*E21*x0*x2/8 + E10*E21*x2^2/32 - E10*E22*x0*x1/16 + E10*E22*x0*x2/16 - E10*E22*x1^2/32 - E10*E22*x1*x2/16 + E11^2*x0^2/32 + E11^2*x2^2/32 + E11*E12*x0^2/16 + E11*E12*x2^2/32 + E11*E20*x0^2/32 - E11*E20*x0*x2/8 + E11*E20*x2^2/32 + E11*E21*x0^2/16 + E11*E21*x2^2/32 + E11*E22*x0^2/32 - E11*E22*x0*x1/16 - E11*E22*x0*x2/16 - E11*E22*x1^2/32 - E11*E22*x1*x2/16 - E12^2*x0^2/32 - E12*E20*x0^2/32 - E12*E21*x0^2/16 - E12*E22*x0^2/16 - E20*E21*x0^2/32 - E20*E22*x0^2/32 - E21^2*x0^2/32 - E21*E22*x0^2/16 - E22^2*x0^2/32) := by
361 unfold tetBlock5
362 ring
363
364set_option maxHeartbeats 1600000 in
365/-- TT continuum certificate: the literal 216-term per-tet sum (s2, s3, p
366COMPLETELY FREE, standing for sqrt 2, sqrt 3, pi) equals
367-(1/4) * |x|^2 * ||E||_F^2 on the TT constraints. Proof: collapse each
368per-tet block by `tetBlock*_eq` (kernel re-verifies the s2/s3/p
369cancellation), then discharge the pure-QQ identity with the explicit offline
370cofactor certificate via `linear_combination`. -/
371theorem tt_continuum_certificate (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ)
372 (hsym01 : E01 = E10) (hsym02 : E02 = E20) (hsym12 : E12 = E21)
373 (htr : E00 + E11 + E22 = 0)
374 (htrans0 : x0 * E00 + x1 * E10 + x2 * E20 = 0)
375 (htrans1 : x0 * E01 + x1 * E11 + x2 * E21 = 0)
376 (htrans2 : x0 * E02 + x1 * E12 + x2 * E22 = 0) :
377 ((tetBlock0 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p)
378 + (tetBlock1 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p)
379 + (tetBlock2 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p)
380 + (tetBlock3 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p)
381 + (tetBlock4 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p)
382 + (tetBlock5 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p))
383 =
384 -((1 : ℝ)/4) * (x0^2 + x1^2 + x2^2) * (E00^2 + E01^2 + E02^2 + E10^2 + E11^2 + E12^2 + E20^2 + E21^2 + E22^2) := by
385 rw [tetBlock0_eq, tetBlock1_eq, tetBlock2_eq, tetBlock3_eq,
386 tetBlock4_eq, tetBlock5_eq]
387 linear_combination
388 (E00*x0*x1/2 - E01*x0^2/4 + E01*x1^2/4 + E01*x2^2/8 + E02*x1*x2/4 - E10*x0^2/4 - E10*x1^2/4 - E10*x2^2/8 - E12*x0*x2/4 - E20*x1*x2/4 - E21*x0*x2/4 + E22*x0*x1/2) * hsym01
389 + (E00*x0*x2/2 - E02*x0^2/4 + E02*x1^2/8 + E02*x2^2/4 + E11*x0*x2/2 - E12*x0*x1/4 - E20*x0^2/4 - E20*x1^2/8 - E20*x2^2/4 - E21*x0*x1/4) * hsym02
390 + (E00*x1*x2/2 - E02*x0*x1/2 + E11*x1*x2/2 + E12*x0^2/8 - E12*x1^2/4 + E12*x2^2/4 - E21*x0^2/8 - E21*x1^2/4 - E21*x2^2/4) * hsym12
391 + (-E00*x0^2/4 + E00*x1^2/4 + E00*x2^2/4 - E01*x0*x1 - E02*x0*x2/2 + E11*x0^2/4 - E11*x1^2/4 + E11*x2^2/4 - E12*x1*x2/2 + E22*x0^2/4 + E22*x1^2/4 + E22*x2^2/4) * htr
392 + (E00*x0/2 + E01*x1/2 + E02*x2/2) * htrans0
393 + (E01*x0/2 + E11*x1/2 + E12*x2/2) * htrans1
394 + (-E00*x2/2 + E02*x0/2 - E11*x2/2 + E12*x1/2) * htrans2
395
396end IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumCertificateSpike
397