IndisputableMonolith.Gravity.Analysis.ReggeTTCertificateScratch
IndisputableMonolith/Gravity/Analysis/ReggeTTCertificateScratch.lean · 250 lines · 2 declarations
show as:
view math explainer →
1/-
2SCRATCH FEASIBILITY PROBE -- NOT A CAMPAIGN MODULE, NOT A THEOREM CLAIM
3QG campaign, Lane B (regge_tt_stage2_certificate), 2026-07-15.
4
5Kernel-checks one representative block of the B2 raw-m TT certificate for
6the -(1/4) continuum TT Regge symbol: symmetric E (6 real vars), generic
7unnormalized m (3 real vars). The LHS is 4*M written as the UNEXPANDED
8per-tet sum (180 terms, one per tet and ordered slot pair), coefficients
9polynomials in s2 = sqrt 2, s3 = sqrt 3 (abstracted as variables), exactly
10the shape the campaign lane meets when assembling the per-tet Regge Hessian
11from exact cofactor-ratio derivatives. Offline exact computation
12(b2_certificate.py / b3_generate_lean.py) found the (s2^2-2), (s3^2-3) lift
13cofactors are IDENTICALLY ZERO, so `ring` closes the identity and hs2/hs3
14carry 0-coefficients (kept only to mirror the anticipated statement shape).
15
16CRITIC CORRECTION (2026-07-15): the original claim here, that "the radicals
17cancel across the six tets", is WRONG as a mechanism: every off-diagonal
18G entry is already INDIVIDUALLY rational at the flat point (values in
19{0, +-1/4, -1/8}), so the statement below contains no s2/s3 in any term,
20the hs2/hs3 hypotheses are INERT, and this block demonstrates term-count
21feasibility only, NOT radical-workload feasibility. The campaign lane
22should budget zero radical-cancellation work; the identity is rational
23per entry, not by cross-tet cancellation.
24
25This block certifies: 4M + |m|^2*||E||_F^2 = q_tr*(tr E) + Sum_j q_j*(E m)_j,
26i.e. on the TT variety (tr E = 0, E m = 0, E symmetric) the raw-m moment
27form satisfies 4M = -|m|^2*||E||_F^2: the Bloch-limit quadratic form is
28-(1/4)*||E||^2 per unit |m|^2 for EVERY direction and EVERY TT polarization.
29
30Generated by state/qg_full_theory/regge_tt_stage2_certificate/
31b3_generate_lean.py. Do NOT import from campaign modules; do NOT cite as
32proof of the continuum -(1/4) symbol (that still needs the Bloch t->0 limit
33analysis on top of this algebraic block).
34-/
35import Mathlib.Data.Real.Basic
36import Mathlib.Tactic.Ring
37import Mathlib.Tactic.LinearCombination
38
39namespace IndisputableMonolith.Gravity.Analysis.ReggeTTCertificateScratch
40
41set_option maxHeartbeats 4000000
42
43/-- Pre-cancellation certificate block: 4*M as the literal per-tet sum with
44s2, s3 opaque; the offline lift cofactors are 0, so `linear_combination`
45with 0-coefficients (= `ring1` on the difference) closes it. -/
46theorem certificate_block_pertet
47 (E00 E01 E02 E11 E12 E22 m0 m1 m2 s2 s3 : ℝ)
48 (hs2 : s2 ^ 2 = 2) (hs3 : s3 ^ 2 = 3) :
49 (((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E01 + E11) * (m1)^2
50 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m1 + m2)^2
51 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E11) * (m0 + m1)^2
52 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00) * (E11 + 2*E12 + E22) * (m0 + m1 + m2)^2
53 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E22) * (m0 + 2*m1 + m2)^2
54 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + E11) * (E00) * (-m1)^2
55 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m2)^2
56 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E01 + E11) * (E11) * (m0)^2
57 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + E11) * (E11 + 2*E12 + E22) * (m0 + m2)^2
58 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + E11) * (E22) * (m0 + m1 + m2)^2
59 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00) * (-m1 - m2)^2
60 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E01 + E11) * (-m2)^2
61 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11) * (m0 - m2)^2
62 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11 + 2*E12 + E22) * (m0)^2
63 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E22) * (m0 + m1)^2
64 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00) * (-m0 - m1)^2
65 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11) * (E00 + 2*E01 + E11) * (-m0)^2
66 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0 + m2)^2
67 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11) * (E11 + 2*E12 + E22) * (m2)^2
68 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E22) * (m1 + m2)^2
69 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00) * (-m0 - m1 - m2)^2
70 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E00 + 2*E01 + E11) * (-m0 - m2)^2
71 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0)^2
72 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E11) * (-m2)^2
73 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11 + 2*E12 + E22) * (E22) * (m1)^2
74 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E00) * (-m0 - 2*m1 - m2)^2
75 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E22) * (E00 + 2*E01 + E11) * (-m0 - m1 - m2)^2
76 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0 - m1)^2
77 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E11) * (-m1 - m2)^2
78 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E11 + 2*E12 + E22) * (-m1)^2
79 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E02 + E22) * (m2)^2
80 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m1 + m2)^2
81 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E22) * (m0 + m2)^2
82 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00) * (E11 + 2*E12 + E22) * (m0 + m1 + m2)^2
83 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E11) * (m0 + m1 + 2*m2)^2
84 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E02 + E22) * (E00) * (-m2)^2
85 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m1)^2
86 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E22) * (m0)^2
87 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E11 + 2*E12 + E22) * (m0 + m1)^2
88 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E11) * (m0 + m1 + m2)^2
89 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00) * (-m1 - m2)^2
90 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (-m1)^2
91 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E22) * (m0 - m1)^2
92 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11 + 2*E12 + E22) * (m0)^2
93 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11) * (m0 + m2)^2
94 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00) * (-m0 - m2)^2
95 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E22) * (E00 + 2*E02 + E22) * (-m0)^2
96 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0 + m1)^2
97 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E22) * (E11 + 2*E12 + E22) * (m1)^2
98 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E11) * (m1 + m2)^2
99 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00) * (-m0 - m1 - m2)^2
100 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (-m0 - m1)^2
101 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0)^2
102 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E22) * (-m1)^2
103 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11 + 2*E12 + E22) * (E11) * (m2)^2
104 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E00) * (-m0 - m1 - 2*m2)^2
105 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11) * (E00 + 2*E02 + E22) * (-m0 - m1 - m2)^2
106 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0 - m2)^2
107 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E22) * (-m1 - m2)^2
108 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E11 + 2*E12 + E22) * (-m2)^2
109 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00 + 2*E01 + E11) * (m0)^2
110 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0 + m2)^2
111 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00) * (m0 + m1)^2
112 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11) * (E00 + 2*E02 + E22) * (m0 + m1 + m2)^2
113 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E22) * (2*m0 + m1 + m2)^2
114 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + E11) * (E11) * (-m0)^2
115 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m2)^2
116 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E01 + E11) * (E00) * (m1)^2
117 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + E11) * (E00 + 2*E02 + E22) * (m1 + m2)^2
118 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + E11) * (E22) * (m0 + m1 + m2)^2
119 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11) * (-m0 - m2)^2
120 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E01 + E11) * (-m2)^2
121 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00) * (m1 - m2)^2
122 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (m1)^2
123 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E22) * (m0 + m1)^2
124 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E11) * (-m0 - m1)^2
125 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00) * (E00 + 2*E01 + E11) * (-m1)^2
126 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m1 + m2)^2
127 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00) * (E00 + 2*E02 + E22) * (m2)^2
128 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E22) * (m0 + m2)^2
129 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E11) * (-m0 - m1 - m2)^2
130 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + E11) * (-m1 - m2)^2
131 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m1)^2
132 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E00) * (-m2)^2
133 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E02 + E22) * (E22) * (m0)^2
134 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E11) * (-2*m0 - m1 - m2)^2
135 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E22) * (E00 + 2*E01 + E11) * (-m0 - m1 - m2)^2
136 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0 - m1)^2
137 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00) * (-m0 - m2)^2
138 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00 + 2*E02 + E22) * (-m0)^2
139 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E11 + 2*E12 + E22) * (m2)^2
140 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0 + m2)^2
141 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E22) * (m1 + m2)^2
142 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11) * (E00 + 2*E02 + E22) * (m0 + m1 + m2)^2
143 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E00) * (m0 + m1 + 2*m2)^2
144 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11 + 2*E12 + E22) * (E11) * (-m2)^2
145 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0)^2
146 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E22) * (m1)^2
147 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (m0 + m1)^2
148 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00) * (m0 + m1 + m2)^2
149 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11) * (-m0 - m2)^2
150 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11 + 2*E12 + E22) * (-m0)^2
151 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E22) * (-m0 + m1)^2
152 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (m1)^2
153 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00) * (m1 + m2)^2
154 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E11) * (-m1 - m2)^2
155 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E22) * (E11 + 2*E12 + E22) * (-m1)^2
156 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0 - m1)^2
157 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E22) * (E00 + 2*E02 + E22) * (m0)^2
158 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00) * (m0 + m2)^2
159 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E11) * (-m0 - m1 - m2)^2
160 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E11 + 2*E12 + E22) * (-m0 - m1)^2
161 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m1)^2
162 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E22) * (-m0)^2
163 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E02 + E22) * (E00) * (m2)^2
164 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E11) * (-m0 - m1 - 2*m2)^2
165 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00) * (E11 + 2*E12 + E22) * (-m0 - m1 - m2)^2
166 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m1 - m2)^2
167 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E22) * (-m0 - m2)^2
168 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E02 + E22) * (-m2)^2
169 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00 + 2*E02 + E22) * (m0)^2
170 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0 + m1)^2
171 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00) * (m0 + m2)^2
172 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E22) * (E00 + 2*E01 + E11) * (m0 + m1 + m2)^2
173 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E11) * (2*m0 + m1 + m2)^2
174 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E02 + E22) * (E22) * (-m0)^2
175 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m1)^2
176 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E00) * (m2)^2
177 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + E11) * (m1 + m2)^2
178 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E11) * (m0 + m1 + m2)^2
179 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E22) * (-m0 - m1)^2
180 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (-m1)^2
181 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00) * (-m1 + m2)^2
182 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E01 + E11) * (m2)^2
183 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11) * (m0 + m2)^2
184 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E22) * (-m0 - m2)^2
185 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00) * (E00 + 2*E02 + E22) * (-m2)^2
186 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m1 - m2)^2
187 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00) * (E00 + 2*E01 + E11) * (m1)^2
188 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E11) * (m0 + m1)^2
189 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + E11) * (E22) * (-m0 - m1 - m2)^2
190 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + E11) * (E00 + 2*E02 + E22) * (-m1 - m2)^2
191 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m2)^2
192 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E01 + E11) * (E00) * (-m1)^2
193 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + E11) * (E11) * (m0)^2
194 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E22) * (-2*m0 - m1 - m2)^2
195 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11) * (E00 + 2*E02 + E22) * (-m0 - m1 - m2)^2
196 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0 - m2)^2
197 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00) * (-m0 - m1)^2
198 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00 + 2*E01 + E11) * (-m0)^2
199 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E11 + 2*E12 + E22) * (m1)^2
200 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0 + m1)^2
201 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E11) * (m1 + m2)^2
202 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E22) * (E00 + 2*E01 + E11) * (m0 + m1 + m2)^2
203 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E00) * (m0 + 2*m1 + m2)^2
204 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11 + 2*E12 + E22) * (E22) * (-m1)^2
205 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0)^2
206 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E11) * (m2)^2
207 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E00 + 2*E01 + E11) * (m0 + m2)^2
208 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00) * (m0 + m1 + m2)^2
209 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E22) * (-m0 - m1)^2
210 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11 + 2*E12 + E22) * (-m0)^2
211 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11) * (-m0 + m2)^2
212 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E01 + E11) * (m2)^2
213 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00) * (m1 + m2)^2
214 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E22) * (-m1 - m2)^2
215 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11) * (E11 + 2*E12 + E22) * (-m2)^2
216 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0 - m2)^2
217 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11) * (E00 + 2*E01 + E11) * (m0)^2
218 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00) * (m0 + m1)^2
219 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + E11) * (E22) * (-m0 - m1 - m2)^2
220 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + E11) * (E11 + 2*E12 + E22) * (-m0 - m2)^2
221 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m2)^2
222 + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E01 + E11) * (E11) * (-m0)^2
223 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + E11) * (E00) * (m1)^2
224 + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E22) * (-m0 - 2*m1 - m2)^2
225 + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00) * (E11 + 2*E12 + E22) * (-m0 - m1 - m2)^2
226 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m1 - m2)^2
227 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E11) * (-m0 - m1)^2
228 + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E01 + E11) * (-m1)^2
229 + (m0^2 + m1^2 + m2^2) * (E00^2 + 2*E01^2 + 2*E02^2 + E11^2 + 2*E12^2 + E22^2))
230 =
231 (-E00*m0^2 + E00*m1^2 + E00*m2^2 - 4*E01*m0*m1 - 2*E02*m0*m2 + E11*m0^2 - E11*m1^2 + E11*m2^2 - 2*E12*m1*m2 + E22*m0^2 + E22*m1^2 + E22*m2^2) * (E00 + E11 + E22)
232 + (2*E00*m0 + 2*E01*m1 + 2*E02*m2) * (E00*m0 + E01*m1 + E02*m2)
233 + (2*E01*m0 + 2*E11*m1 + 2*E12*m2) * (E01*m0 + E11*m1 + E12*m2)
234 + (-2*E00*m2 + 2*E02*m0 - 2*E11*m2 + 2*E12*m1) * (E02*m0 + E12*m1 + E22*m2) := by
235 linear_combination (0 : ℝ) * hs2 + (0 : ℝ) * hs3
236
237/-- Post-cancellation rational identity (radicals already cancelled),
238closed by plain `ring`. -/
239theorem certificate_block_rational
240 (E00 E01 E02 E11 E12 E22 m0 m1 m2 : ℝ) :
241 E00^2*m0^2 + E00^2*m1^2 + E00^2*m2^2 + 2*E00*E11*m2^2 - 4*E00*E12*m1*m2 + 2*E00*E22*m1^2 + 2*E01^2*m0^2 + 2*E01^2*m1^2 + 4*E01*E02*m1*m2 + 4*E01*E12*m0*m2 - 4*E01*E22*m0*m1 + 2*E02^2*m0^2 + 2*E02^2*m2^2 - 4*E02*E11*m0*m2 + 4*E02*E12*m0*m1 + E11^2*m0^2 + E11^2*m1^2 + E11^2*m2^2 + 2*E11*E22*m0^2 + 2*E12^2*m1^2 + 2*E12^2*m2^2 + E22^2*m0^2 + E22^2*m1^2 + E22^2*m2^2
242 =
243 (-E00*m0^2 + E00*m1^2 + E00*m2^2 - 4*E01*m0*m1 - 2*E02*m0*m2 + E11*m0^2 - E11*m1^2 + E11*m2^2 - 2*E12*m1*m2 + E22*m0^2 + E22*m1^2 + E22*m2^2) * (E00 + E11 + E22)
244 + (2*E00*m0 + 2*E01*m1 + 2*E02*m2) * (E00*m0 + E01*m1 + E02*m2)
245 + (2*E01*m0 + 2*E11*m1 + 2*E12*m2) * (E01*m0 + E11*m1 + E12*m2)
246 + (-2*E00*m2 + 2*E02*m0 - 2*E11*m2 + 2*E12*m1) * (E02*m0 + E12*m1 + E22*m2) := by
247 ring
248
249end IndisputableMonolith.Gravity.Analysis.ReggeTTCertificateScratch
250