IndisputableMonolith.Gravity.Analysis.ReggeTTDerivativeGate
IndisputableMonolith/Gravity/Analysis/ReggeTTDerivativeGate.lean · 766 lines · 39 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.Analysis.ReggeTTSymbolPreflight
2
3/-!
4# Regge TT derivative gate: Stage-2 Gate-0 / Lane-A of `ReggeTTContinuumSymbol`
5
6QG full-theory campaign, `ReggeTTContinuumSymbol` program, Stage 2
7(Gate 0 + Lane A of the panel-locked two-lane protocol; Stage 1 is
8`ReggeTTSymbolPreflight`).
9
10## Tier tags (binding, per-claim)
11
12* THEOREM: everything proved in this file (kernel-checked here; no sorry, no
13 admit, no new axioms, no native_decide, no `: True` shells, no
14 Nonempty-only shells).
15* NUMERICAL EVIDENCE (never proof): the continuum TT symbol value `-(1/4)`
16 remains exactly where Stage 1 left it — supported only by the C10
17 provenance-gated numerics probe. NOTHING in this file proves, or even
18 approaches, the continuum value; `ReggeTTContinuumIsotropyTarget` stays
19 OPEN with status flag `false` in Stage 1.
20* OPEN: the continuum TT symbol existence and value; also second-derivative
21 existence of the plane-wave action profile (stage 2a), which this file
22 does NOT prove — Lane A here delivers only FIRST-derivative structure at
23 the flat point of a single tetrahedron plus the flat-neighborhood
24 nondegeneracy that stage 2a will need.
25
26## What this module proves (all THEOREM)
27
28* Gate 0a (`planeWaveActionProfile_eq_trueReggeAction`): the plane-wave
29 action profile is BY DEFINITION the true nonlinear Regge action on the
30 plane-wave edge field — kernel equation, no surrogate action anywhere.
31* Gate 0b (`ttPolarization_frobeniusSq_eq_one`,
32 `isTTPolarization_of_orthonormal_transverse_pair`,
33 `exists_isTTPolarization`, `exists_isTTPolarization_of_ne_zero`): the
34 Frobenius normalization is projected out of `IsTTPolarization` as a named
35 lemma, and the TT constraint set is nonempty for EVERY integer wave
36 vector (a fortiori every nonzero one), by an explicit Gram-Schmidt-style
37 transverse frame with a planar/axial case split — not axis-only.
38* Gate 0c (`flatAngleJacobian`, `flatSqrtEdgeDeriv`, `flatReggeStencilMoment`,
39 `stencil_ordering_grounded`): the SHARED NAMED STENCIL both lanes must
40 reference — the flat tuple `freudenthalTetSqEdges` (proved in Stage 1 to
41 be exactly what every tetrahedron of the action sees at flat, re-exported
42 here as `stencil_ordering_grounded`), the closed-form flat angle Jacobian
43 `∂θ_f/∂a_k`, and the flat sqrt-edge derivatives `1/(2√a_f)`.
44* Lane A1 (`flat_nondegeneracy_eventually`): an open neighborhood of the
45 flat tuple (stated as a `∀ᶠ` in `nhds`) on which `cm3 > 0`, all six
46 squared edges are positive, all diagonal cofactor products are positive,
47 and every dihedral cosine lies strictly inside `(-1, 1)`.
48* Lane A2 (`hasDerivAt_flatAngle_directional`,
49 `hasDerivAt_flatWeightedAngleSum`): along every affine squared-edge
50 direction `v` through the flat tuple, each dihedral angle is
51 differentiable with directional derivative `∑_k v_k · J_{f,k}`, and the
52 per-tetrahedron weighted angle sum `g(a) = ∑_f √a_f · θ_f(a)` is
53 differentiable at flat with derivative `∑_f (v_f/(2√a_f)) · θ_f` — the
54 `θ'`-terms cancel EXACTLY by the proved tetrahedral Schläfli identity
55 (`flatAngleJacobian_schlaefli`), not by any numerical argument.
56* Lane A3 (`flatArccosFactor_spec`, `flatAngleJacobian_cofactor_form`,
57 `flatAngleJacobian_row0_norm`, `flatAngleJacobian_row0_eval`): every row
58 of the flat angle Jacobian is pure cofactor algebra times an exactly
59 evaluated arccos factor (√2, 1, 2/√3, 1, 1, √2 — zero arccos values
60 anywhere), and the `f = 0` row is fully evaluated to exact rationals
61 `(0, 0, 0, 0, -1/4, 1/2)`.
62
63## What this module does NOT prove (binding scope disclosure)
64
65* No second derivatives: stage 2a (second-derivative existence of the
66 plane-wave profile) is NOT attempted here.
67* No lattice sum: everything in Lane A is per-tetrahedron at the flat
68 point; the assembly over the periodic torus is later-stage work.
69* No symbol limits, no continuum value, no isotropy: `-(1/4)` remains
70 NUMERICAL EVIDENCE (C10 probe) and `ReggeTTContinuumIsotropyTarget`
71 remains OPEN.
72
73## Inherited axiom footprint (disclosure)
74
75This file never touches the certified periodic angle-sum chain, so nothing
76here inherits `Lean.ofReduceBool` / `Lean.trustCompiler`. Every theorem in
77this file is pure algebra/analysis over the standard trio
78`[propext, Classical.choice, Quot.sound]` (Gate 0a is a kernel `rfl` on the
79Stage-1 definitions; the Schläfli input `tetraSchlaefliSixEdgeClosedForm`
80and the bridge `schlaefli_summand_bridge_edge0` are pure-algebra theorems
81with the standard footprint).
82
83No `sorry`, no `admit`, no new axioms, no `native_decide` in this file.
84-/
85
86namespace IndisputableMonolith
87namespace Gravity
88namespace Analysis
89namespace ReggeTTDerivativeGate
90
91open Geometry.CayleyMengerPolynomial (SqEdges cm3)
92open Geometry.CayleyMengerMatrix (cmCofactor3 cmCofactor3_contDiff)
93open Geometry.DihedralCayleyMenger (dihedralCos3Sq dihedralDenom3 oppositeCMVertices)
94open Geometry.DihedralDerivatives (dihedralAngle3Sq dihedralAngle3SqClosedFormDeriv)
95open Geometry.FreudenthalCubeTriangulation (freudenthalTetSqEdges freudenthalTet
96 cm3_freudenthalTetSqEdges)
97
98noncomputable section
99
100/-! ## §1. Gate 0a — the profile IS the true action (THEOREM, kernel `rfl`)
101
102The C10 observable is the second difference of `planeWaveActionProfile`.
103This theorem pins, as a kernel equation, that the profile is the TRUE
104nonlinear Regge action `S(ℓ) = Σ_e √ℓ_e·(2π − Σθ)` evaluated on the
105plane-wave edge field — there is no linearized or surrogate action anywhere
106in the symbol object. -/
107
108theorem planeWaveActionProfile_eq_trueReggeAction
109 (N : ℕ) [NeZero N] (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ) (t : ℝ) :
110 ReggeTTSymbolPreflight.planeWaveActionProfile N E k t =
111 ReggeTTSymbolPreflight.trueReggeAction N
112 (ReggeTTSymbolPreflight.planeWaveEdgeField N E k t) := rfl
113
114/-! ## §2. Gate 0b — TT audit and non-vacuity for every wave vector
115
116`IsTTPolarization` bundles symmetry, tracelessness, transversality, and
117Frobenius normalization. The normalization is projected out as a named
118lemma, and the constraint set is proved nonempty for EVERY integer wave
119vector by an explicit orthonormal transverse frame (planar/axial case
120split), strengthening the Stage-1 axis-only witnesses. -/
121
122/-- The fourth `IsTTPolarization` conjunct as a named audit lemma: every TT
123polarization has Frobenius norm square exactly `1`. -/
124theorem ttPolarization_frobeniusSq_eq_one (m : Fin 3 → ℤ) (E : Fin 3 → Fin 3 → ℝ)
125 (hE : ReggeTTSymbolPreflight.IsTTPolarization m E) :
126 (∑ i : Fin 3, ∑ j : Fin 3, E i j * E i j) = 1 := hE.2.2.2
127
128private theorem sum3_div_sq (x y z c : ℝ) (hc : 0 < c) (h : x ^ 2 + y ^ 2 + z ^ 2 = c) :
129 x / Real.sqrt c * (x / Real.sqrt c) + y / Real.sqrt c * (y / Real.sqrt c) +
130 z / Real.sqrt c * (z / Real.sqrt c) = 1 := by
131 have hcs : Real.sqrt c * Real.sqrt c = c := Real.mul_self_sqrt hc.le
132 rw [div_mul_div_comm, div_mul_div_comm, div_mul_div_comm, hcs,
133 ← add_div, ← add_div,
134 show x * x + y * y + z * z = c by linear_combination h]
135 exact div_self (ne_of_gt hc)
136
137private theorem sum3_div_orth (x y z x' y' z' c d : ℝ)
138 (h : x * x' + y * y' + z * z' = 0) :
139 x / c * (x' / d) + y / c * (y' / d) + z / c * (z' / d) = 0 := by
140 rw [div_mul_div_comm, div_mul_div_comm, div_mul_div_comm,
141 ← add_div, ← add_div, h, zero_div]
142
143private theorem sum3_dot_div (a b c x y z r : ℝ) (h : a * x + b * y + c * z = 0) :
144 a * (x / r) + b * (y / r) + c * (z / r) = 0 := by
145 rw [← mul_div_assoc, ← mul_div_assoc, ← mul_div_assoc,
146 ← add_div, ← add_div, h, zero_div]
147
148/-- TT polarization from an orthonormal transverse pair: if `u, v` are unit
149vectors, mutually orthogonal, and both orthogonal to the (real cast of the)
150integer wave vector `m`, then `E = (u⊗u − v⊗v)/√2` is a TT polarization for
151`m`. This is the generic Gram-Schmidt-style constructor behind the
152non-vacuity theorem. -/
153theorem isTTPolarization_of_orthonormal_transverse_pair
154 (m : Fin 3 → ℤ) (u v : Fin 3 → ℝ)
155 (hu : (∑ i : Fin 3, u i * u i) = 1)
156 (hv : (∑ i : Fin 3, v i * v i) = 1)
157 (huv : (∑ i : Fin 3, u i * v i) = 0)
158 (hmu : (∑ i : Fin 3, (m i : ℝ) * u i) = 0)
159 (hmv : (∑ i : Fin 3, (m i : ℝ) * v i) = 0) :
160 ReggeTTSymbolPreflight.IsTTPolarization m
161 (fun i j => (u i * u j - v i * v j) / Real.sqrt 2) := by
162 have hs2 : Real.sqrt 2 * Real.sqrt 2 = 2 :=
163 Real.mul_self_sqrt (by norm_num)
164 have hhalf : ∀ x : ℝ,
165 x / Real.sqrt 2 * (x / Real.sqrt 2) = x ^ 2 / 2 := by
166 intro x
167 rw [div_mul_div_comm, hs2]
168 ring
169 simp only [Fin.sum_univ_three] at hu hv huv hmu hmv
170 refine ⟨?_, ?_, ?_, ?_⟩
171 · intro i j
172 dsimp only
173 ring
174 · simp only [Fin.sum_univ_three]
175 linear_combination (1 / Real.sqrt 2) * hu - (1 / Real.sqrt 2) * hv
176 · intro j
177 simp only [Fin.sum_univ_three]
178 linear_combination (u j / Real.sqrt 2) * hmu - (v j / Real.sqrt 2) * hmv
179 · simp only [Fin.sum_univ_three, hhalf]
180 linear_combination
181 ((u 0 * u 0 + u 1 * u 1 + u 2 * u 2 + 1) / 2) * hu +
182 ((v 0 * v 0 + v 1 * v 1 + v 2 * v 2 + 1) / 2) * hv -
183 (u 0 * v 0 + u 1 * v 1 + u 2 * v 2) * huv
184
185/-- First transverse unit vector for a wave vector with nonzero planar part
186`(m₀, m₁)`: the normalized in-plane rotation `(−m₁, m₀, 0)/√(m₀²+m₁²)`. -/
187def planarTransverse1 (m : Fin 3 → ℤ) : Fin 3 → ℝ
188 | 0 => -(m 1 : ℝ) / Real.sqrt ((m 0 : ℝ) ^ 2 + (m 1 : ℝ) ^ 2)
189 | 1 => (m 0 : ℝ) / Real.sqrt ((m 0 : ℝ) ^ 2 + (m 1 : ℝ) ^ 2)
190 | 2 => 0 / Real.sqrt ((m 0 : ℝ) ^ 2 + (m 1 : ℝ) ^ 2)
191
192/-- Second transverse unit vector: the normalized cross product
193`m × (−m₁, m₀, 0) = (−m₀m₂, −m₁m₂, m₀²+m₁²)`, with norm
194`√((m₀²+m₁²)·|m|²)`. -/
195def planarTransverse2 (m : Fin 3 → ℤ) : Fin 3 → ℝ
196 | 0 => -((m 0 : ℝ) * (m 2 : ℝ)) /
197 Real.sqrt (((m 0 : ℝ) ^ 2 + (m 1 : ℝ) ^ 2) *
198 (((m 0 : ℝ) ^ 2 + (m 1 : ℝ) ^ 2) + (m 2 : ℝ) ^ 2))
199 | 1 => -((m 1 : ℝ) * (m 2 : ℝ)) /
200 Real.sqrt (((m 0 : ℝ) ^ 2 + (m 1 : ℝ) ^ 2) *
201 (((m 0 : ℝ) ^ 2 + (m 1 : ℝ) ^ 2) + (m 2 : ℝ) ^ 2))
202 | 2 => ((m 0 : ℝ) ^ 2 + (m 1 : ℝ) ^ 2) /
203 Real.sqrt (((m 0 : ℝ) ^ 2 + (m 1 : ℝ) ^ 2) *
204 (((m 0 : ℝ) ^ 2 + (m 1 : ℝ) ^ 2) + (m 2 : ℝ) ^ 2))
205
206/-- Axial fallback frame (used when `m₀ = m₁ = 0`): the x-axis unit vector. -/
207def axialTransverse1 : Fin 3 → ℝ
208 | 0 => 1
209 | 1 => 0
210 | 2 => 0
211
212/-- Axial fallback frame (used when `m₀ = m₁ = 0`): the y-axis unit vector. -/
213def axialTransverse2 : Fin 3 → ℝ
214 | 0 => 0
215 | 1 => 1
216 | 2 => 0
217
218/-- GATE 0b NON-VACUITY (THEOREM), general form: EVERY integer wave vector
219(zero included) carries a TT polarization, built from an explicit
220orthonormal transverse frame — planar rotation + cross product when
221`(m₀, m₁) ≠ 0`, the axial `x/y` frame when `m₀ = m₁ = 0`. No axis-only
222weakening anywhere. -/
223theorem exists_isTTPolarization (m : Fin 3 → ℤ) :
224 ∃ E : Fin 3 → Fin 3 → ℝ, ReggeTTSymbolPreflight.IsTTPolarization m E := by
225 by_cases h01 : (m 0 : ℝ) = 0 ∧ (m 1 : ℝ) = 0
226 · refine ⟨_, isTTPolarization_of_orthonormal_transverse_pair m
227 axialTransverse1 axialTransverse2 ?_ ?_ ?_ ?_ ?_⟩ <;>
228 simp [axialTransverse1, axialTransverse2, Fin.sum_univ_three, h01.1, h01.2]
229 · have h01' : (m 0 : ℝ) ≠ 0 ∨ (m 1 : ℝ) ≠ 0 := by
230 by_contra h
231 push_neg at h
232 exact h01 ⟨h.1, h.2⟩
233 have hs : 0 < (m 0 : ℝ) ^ 2 + (m 1 : ℝ) ^ 2 := by
234 rcases h01' with h | h
235 · have h0 : 0 < (m 0 : ℝ) ^ 2 := by positivity
236 nlinarith [sq_nonneg ((m 1 : ℝ))]
237 · have h1 : 0 < (m 1 : ℝ) ^ 2 := by positivity
238 nlinarith [sq_nonneg ((m 0 : ℝ))]
239 have hn : 0 < ((m 0 : ℝ) ^ 2 + (m 1 : ℝ) ^ 2) + (m 2 : ℝ) ^ 2 := by
240 nlinarith [sq_nonneg ((m 2 : ℝ))]
241 have hsn : 0 < ((m 0 : ℝ) ^ 2 + (m 1 : ℝ) ^ 2) *
242 (((m 0 : ℝ) ^ 2 + (m 1 : ℝ) ^ 2) + (m 2 : ℝ) ^ 2) := mul_pos hs hn
243 refine ⟨_, isTTPolarization_of_orthonormal_transverse_pair m
244 (planarTransverse1 m) (planarTransverse2 m) ?_ ?_ ?_ ?_ ?_⟩
245 · simp only [planarTransverse1, Fin.sum_univ_three]
246 exact sum3_div_sq _ _ _ _ hs (by ring)
247 · simp only [planarTransverse2, Fin.sum_univ_three]
248 exact sum3_div_sq _ _ _ _ hsn (by ring)
249 · simp only [planarTransverse1, planarTransverse2, Fin.sum_univ_three]
250 exact sum3_div_orth _ _ _ _ _ _ _ _ (by ring)
251 · simp only [planarTransverse1, Fin.sum_univ_three]
252 exact sum3_dot_div _ _ _ _ _ _ _ (by ring)
253 · simp only [planarTransverse2, Fin.sum_univ_three]
254 exact sum3_dot_div _ _ _ _ _ _ _ (by ring)
255
256/-- GATE 0b NON-VACUITY, panel-locked form: every NONZERO integer wave
257vector carries a TT polarization. -/
258theorem exists_isTTPolarization_of_ne_zero (m : Fin 3 → ℤ) (_hm : m ≠ 0) :
259 ∃ E : Fin 3 → Fin 3 → ℝ, ReggeTTSymbolPreflight.IsTTPolarization m E :=
260 exists_isTTPolarization m
261
262/-! ## §3. Gate 0c — the SHARED NAMED STENCIL
263
264Both lanes of the Stage-2 protocol must reference these objects BY NAME;
265this structurally prevents transcription drift between the Lean lane and
266the numerics lane. The per-tet objects are: the flat squared-edge tuple
267`freudenthalTetSqEdges = (1,2,3,1,2,1)` (in the action's actual local
268six-edge ordering — Stage 1's `tetSqEdgesOfField_flat` proves every
269tetrahedron of the true action sees exactly this tuple at flat, re-exported
270below), the flat angle Jacobian `∂θ_f/∂a_k`, and the flat sqrt-edge
271derivatives `1/(2√a_f)`. -/
272
273/-- THE SHARED STENCIL JACOBIAN: closed-form derivative of the `f`-th local
274dihedral angle with respect to the `k`-th local squared-edge coordinate,
275evaluated at the flat Freudenthal tuple, in the action's local six-edge
276ordering. `flatAngleJacobian f k = ∂θ_f/∂a_k (freudenthalTetSqEdges)`. -/
277def flatAngleJacobian (f k : Fin 6) : ℝ :=
278 dihedralAngle3SqClosedFormDeriv freudenthalTetSqEdges f k
279
280/-- THE SHARED STENCIL SQRT DERIVATIVES: `d√a/da` at the flat tuple,
281`flatSqrtEdgeDeriv f = 1/(2√(a_f))` with `a = freudenthalTetSqEdges`. -/
282def flatSqrtEdgeDeriv (f : Fin 6) : ℝ :=
283 1 / (2 * Real.sqrt (freudenthalTetSqEdges f))
284
285/-- The per-tetrahedron flat second-variation stencil data: flat tuple,
286angle Jacobian, sqrt-edge derivatives. Lane B's numerics script mirrors
287exactly these three named objects. -/
288structure FlatReggeStencil where
289 /-- The flat local squared-edge tuple. -/
290 sqEdges : SqEdges
291 /-- The flat angle Jacobian `∂θ_f/∂a_k`. -/
292 angleJacobian : Fin 6 → Fin 6 → ℝ
293 /-- The flat sqrt-edge derivatives `1/(2√a_f)`. -/
294 sqrtEdgeDeriv : Fin 6 → ℝ
295
296/-- THE SHARED NAMED STENCIL (Gate 0c deliverable): the canonical per-tet
297stencil moment object at the flat Freudenthal point. -/
298def flatReggeStencilMoment : FlatReggeStencil where
299 sqEdges := freudenthalTetSqEdges
300 angleJacobian := flatAngleJacobian
301 sqrtEdgeDeriv := flatSqrtEdgeDeriv
302
303/-- Ordering grounding: at the flat edge field, every tetrahedron of the
304TRUE action sees exactly the stencil's flat tuple (re-export of Stage 1's
305`tetSqEdgesOfField_flat` in stencil vocabulary, so the stencil ordering and
306the action's local ordering are kernel-identified). -/
307theorem stencil_ordering_grounded (N : ℕ) [NeZero N]
308 (cellTet : Geometry.PeriodicFreudenthalTorus.PeriodicTet N N N) :
309 ReggeTTSymbolPreflight.tetSqEdgesOfField N
310 (ReggeTTSymbolPreflight.flatEdgeField N) cellTet =
311 flatReggeStencilMoment.sqEdges :=
312 ReggeTTSymbolPreflight.tetSqEdgesOfField_flat N cellTet
313
314/-- The stencil sqrt-edge derivative is the actual derivative of
315`Real.sqrt` at the flat squared edge (the edges are positive, so `sqrt` is
316differentiable there). -/
317theorem hasDerivAt_sqrt_flatEdge (f : Fin 6) :
318 HasDerivAt Real.sqrt (flatSqrtEdgeDeriv f) (freudenthalTetSqEdges f) :=
319 Real.hasDerivAt_sqrt (ne_of_gt (freudenthalTet.sqEdge_pos f))
320
321/-! ## §4. Exact flat cosine values and endpoint freedom
322
323The six flat dihedral cosines are exactly `√2/2, 0, 1/2, 0, 0, √2/2`
324(Stage-1 `freudenthalLocalDihedralCos_eq`), all strictly inside `(-1, 1)`.
325These are the arccos endpoint-freedom facts every derivative below needs. -/
326
327/-- Exact flat cosine at local edge slot `0`. -/
328theorem flatCos₀ : dihedralCos3Sq freudenthalTetSqEdges 0 = Real.sqrt 2 / 2 :=
329 PhysicalSixTetCubicDirichletInstance.freudenthalLocalDihedralCos_eq 0
330
331/-- Exact flat cosine at local edge slot `1`. -/
332theorem flatCos₁ : dihedralCos3Sq freudenthalTetSqEdges 1 = 0 :=
333 PhysicalSixTetCubicDirichletInstance.freudenthalLocalDihedralCos_eq 1
334
335/-- Exact flat cosine at local edge slot `2`. -/
336theorem flatCos₂ : dihedralCos3Sq freudenthalTetSqEdges 2 = 1 / 2 :=
337 PhysicalSixTetCubicDirichletInstance.freudenthalLocalDihedralCos_eq 2
338
339/-- Exact flat cosine at local edge slot `3`. -/
340theorem flatCos₃ : dihedralCos3Sq freudenthalTetSqEdges 3 = 0 :=
341 PhysicalSixTetCubicDirichletInstance.freudenthalLocalDihedralCos_eq 3
342
343/-- Exact flat cosine at local edge slot `4`. -/
344theorem flatCos₄ : dihedralCos3Sq freudenthalTetSqEdges 4 = 0 :=
345 PhysicalSixTetCubicDirichletInstance.freudenthalLocalDihedralCos_eq 4
346
347/-- Exact flat cosine at local edge slot `5`. -/
348theorem flatCos₅ : dihedralCos3Sq freudenthalTetSqEdges 5 = Real.sqrt 2 / 2 :=
349 PhysicalSixTetCubicDirichletInstance.freudenthalLocalDihedralCos_eq 5
350
351/-- Every flat cosine is one of the three exact values `√2/2, 0, 1/2`. -/
352theorem flatCos_value_cases (f : Fin 6) :
353 dihedralCos3Sq freudenthalTetSqEdges f = Real.sqrt 2 / 2 ∨
354 dihedralCos3Sq freudenthalTetSqEdges f = 0 ∨
355 dihedralCos3Sq freudenthalTetSqEdges f = 1 / 2 := by
356 fin_cases f
357 · exact Or.inl flatCos₀
358 · exact Or.inr (Or.inl flatCos₁)
359 · exact Or.inr (Or.inr flatCos₂)
360 · exact Or.inr (Or.inl flatCos₃)
361 · exact Or.inr (Or.inl flatCos₄)
362 · exact Or.inl flatCos₅
363
364/-- Every flat cosine lies strictly inside `(-1, 1)`. -/
365theorem flatCos_bounds (f : Fin 6) :
366 -1 < dihedralCos3Sq freudenthalTetSqEdges f ∧
367 dihedralCos3Sq freudenthalTetSqEdges f < 1 := by
368 have hs2sq : Real.sqrt 2 ^ 2 = 2 := Real.sq_sqrt (by norm_num)
369 have hs2nn : 0 ≤ Real.sqrt 2 := Real.sqrt_nonneg 2
370 rcases flatCos_value_cases f with h | h | h <;> rw [h] <;> constructor <;>
371 nlinarith [sq_nonneg (Real.sqrt 2 - 2)]
372
373/-- Arccos endpoint freedom at flat: no flat cosine equals `±1`. -/
374theorem flatCos_ne_endpoints (f : Fin 6) :
375 dihedralCos3Sq freudenthalTetSqEdges f ≠ -1 ∧
376 dihedralCos3Sq freudenthalTetSqEdges f ≠ 1 :=
377 ⟨ne_of_gt (flatCos_bounds f).1, ne_of_lt (flatCos_bounds f).2⟩
378
379/-- All diagonal cofactor products are strictly positive at the flat tuple
380(determinant-cofactor form, i.e. exactly the hypothesis shape of the
381explicit derivative theorems). -/
382theorem flat_cofactorProduct_pos (f : Fin 6) :
383 0 < cmCofactor3 freudenthalTetSqEdges
384 (oppositeCMVertices f).1 (oppositeCMVertices f).1 *
385 cmCofactor3 freudenthalTetSqEdges
386 (oppositeCMVertices f).2 (oppositeCMVertices f).2 := by
387 have h := Geometry.CofactorDerivatives.dihedralCofactorProductPoly_pos_of_nonDegenerate
388 freudenthalTet f
389 simpa [Geometry.CofactorDerivatives.dihedralCofactorProductPoly,
390 Geometry.CofactorPolynomial.cmCofactor3_eq_poly] using h
391
392/-- The dihedral cosine denominator is nonzero at the flat tuple. -/
393theorem flat_denom_ne_zero (f : Fin 6) :
394 dihedralDenom3 freudenthalTetSqEdges f ≠ 0 := by
395 rw [Geometry.CofactorDerivatives.dihedralDenom3_eq_poly]
396 exact Geometry.CofactorDerivatives.dihedralDenom3Poly_ne_zero_of_nonDegenerate
397 freudenthalTet f
398
399/-! ## §5. Lane A1 — neighborhood nondegeneracy at the flat tuple (THEOREM)
400
401There is an open neighborhood of `freudenthalTetSqEdges` in
402`SqEdges = Fin 6 → ℝ` on which `cm3 > 0`, every squared edge is positive,
403every diagonal cofactor product is positive, and every dihedral cosine is
404strictly inside `(-1, 1)`. Stated as a filter `∀ᶠ` at `nhds`; membership
405of an actual open set follows from `Filter.eventually_iff_exists_open` /
406`eventually_nhds_iff` if a set-level form is needed downstream. Proof:
407continuity of the polynomial/ratio maps plus the exact flat values
408(`cm3 = 8`, cosines `√2/2, 0, 1/2`, integer cofactor products). -/
409
410theorem flat_nondegeneracy_eventually :
411 ∀ᶠ a in nhds freudenthalTetSqEdges,
412 0 < cm3 a ∧
413 ∀ f : Fin 6,
414 0 < a f ∧
415 0 < cmCofactor3 a
416 (oppositeCMVertices f).1 (oppositeCMVertices f).1 *
417 cmCofactor3 a
418 (oppositeCMVertices f).2 (oppositeCMVertices f).2 ∧
419 -1 < dihedralCos3Sq a f ∧ dihedralCos3Sq a f < 1 := by
420 have hcm : ∀ᶠ a in nhds freudenthalTetSqEdges, 0 < cm3 a := by
421 have hcont : ContinuousAt cm3 freudenthalTetSqEdges :=
422 (Geometry.CayleyMengerPolynomial.cm3_contDiff (0 : ℕ∞)).continuous.continuousAt
423 have hpos : (0 : ℝ) < cm3 freudenthalTetSqEdges := by
424 rw [cm3_freudenthalTetSqEdges]; norm_num
425 exact Filter.Tendsto.eventually hcont (eventually_gt_nhds hpos)
426 have hf : ∀ f : Fin 6, ∀ᶠ a in nhds freudenthalTetSqEdges,
427 0 < a f ∧
428 0 < cmCofactor3 a
429 (oppositeCMVertices f).1 (oppositeCMVertices f).1 *
430 cmCofactor3 a
431 (oppositeCMVertices f).2 (oppositeCMVertices f).2 ∧
432 -1 < dihedralCos3Sq a f ∧ dihedralCos3Sq a f < 1 := by
433 intro f
434 have hedge : ∀ᶠ a in nhds freudenthalTetSqEdges, 0 < a f := by
435 have hcont : ContinuousAt (fun a : SqEdges => a f) freudenthalTetSqEdges :=
436 (continuous_apply f).continuousAt
437 exact Filter.Tendsto.eventually hcont
438 (eventually_gt_nhds (freudenthalTet.sqEdge_pos f))
439 have hprod : ∀ᶠ a in nhds freudenthalTetSqEdges,
440 0 < cmCofactor3 a
441 (oppositeCMVertices f).1 (oppositeCMVertices f).1 *
442 cmCofactor3 a
443 (oppositeCMVertices f).2 (oppositeCMVertices f).2 := by
444 have hcont : ContinuousAt (fun a : SqEdges =>
445 cmCofactor3 a
446 (oppositeCMVertices f).1 (oppositeCMVertices f).1 *
447 cmCofactor3 a
448 (oppositeCMVertices f).2 (oppositeCMVertices f).2)
449 freudenthalTetSqEdges :=
450 (((cmCofactor3_contDiff (0 : ℕ∞)
451 (oppositeCMVertices f).1 (oppositeCMVertices f).1).continuous).mul
452 ((cmCofactor3_contDiff (0 : ℕ∞)
453 (oppositeCMVertices f).2 (oppositeCMVertices f).2).continuous)).continuousAt
454 exact Filter.Tendsto.eventually hcont
455 (eventually_gt_nhds (flat_cofactorProduct_pos f))
456 have hcosCont : ContinuousAt (fun a : SqEdges => dihedralCos3Sq a f)
457 freudenthalTetSqEdges :=
458 Geometry.ReggeActionSmoothness.dihedralCos3Sq_continuousAt_of_den_ne_zero
459 freudenthalTetSqEdges f (flat_denom_ne_zero f)
460 have hlo : ∀ᶠ a in nhds freudenthalTetSqEdges, -1 < dihedralCos3Sq a f :=
461 Filter.Tendsto.eventually hcosCont (eventually_gt_nhds (flatCos_bounds f).1)
462 have hhi : ∀ᶠ a in nhds freudenthalTetSqEdges, dihedralCos3Sq a f < 1 :=
463 Filter.Tendsto.eventually hcosCont (eventually_lt_nhds (flatCos_bounds f).2)
464 exact hedge.and (hprod.and (hlo.and hhi))
465 exact hcm.and (Filter.eventually_all.2 hf)
466
467/-! ## §6. Lane A2 — the one-tet Schläfli spike (THEOREM)
468
469For every direction `v : Fin 6 → ℝ`, the per-tetrahedron weighted angle sum
470`g(a) = ∑_f √a_f · θ_f(a)` is differentiable at the flat tuple along the
471affine path `a + t·v`, with derivative `∑_f (v_f/(2√a_f)) · θ_f(a)` — the
472`√a_f · θ'_f` group cancels EXACTLY by the proved squared-edge tetrahedral
473Schläfli identity. This is the first-derivative vertical slice toward
474stage 2a. -/
475
476/-- The shared stencil Jacobian is exactly the squared-edge closed-form
477dihedral derivative of the Schläfli module at the flat tetrahedron
478(kernel `rfl`; this ties the Gate-0c stencil to the proved Schläfli
479machinery with zero transcription). -/
480theorem flatAngleJacobian_eq_dihedralClosedDerivSq (f k : Fin 6) :
481 flatAngleJacobian f k =
482 Geometry.SchlaefliTetrahedronProof.dihedralClosedDerivSq freudenthalTet f k := rfl
483
484/-- SCHLÄFLI CANCELLATION AT FLAT (THEOREM): for every squared-edge
485coordinate `k`, `∑_f √(a_f) · flatAngleJacobian f k = 0` at the flat tuple.
486This is the proved six-edge closed-form tetrahedral Schläfli identity
487(`tetraSchlaefliSixEdgeClosedForm`) instantiated at the Freudenthal
488tetrahedron and written in stencil vocabulary. -/
489theorem flatAngleJacobian_schlaefli (k : Fin 6) :
490 (∑ f : Fin 6, Real.sqrt (freudenthalTetSqEdges f) * flatAngleJacobian f k) = 0 :=
491 Geometry.SchlaefliTetrahedronProof.tetraSchlaefliSixEdgeClosedForm freudenthalTet k
492
493/-- Directional derivative of one flat dihedral angle (THEOREM): along the
494affine path `t ↦ a + t·v` through the flat tuple, the `f`-th dihedral angle
495has derivative `∑_k v_k · flatAngleJacobian f k` at `t = 0`. The
496directional derivative is assembled from the six proved coordinate partial
497derivatives through the `C¹` Fréchet derivative at the flat point. -/
498theorem hasDerivAt_flatAngle_directional (v : Fin 6 → ℝ) (f : Fin 6) :
499 HasDerivAt
500 (fun t : ℝ =>
501 dihedralAngle3Sq (fun j : Fin 6 => freudenthalTetSqEdges j + t * v j) f)
502 (∑ k : Fin 6, v k * flatAngleJacobian f k) 0 := by
503 have hC : ContDiffAt ℝ 1 (fun x : SqEdges => dihedralAngle3Sq x f)
504 freudenthalTetSqEdges :=
505 Geometry.ReggeActionFirstVariation.dihedralAngle3Sq_contDiffAt_nonDegenerate
506 freudenthalTet f 1 (flatCos_ne_endpoints f)
507 have hDiff : DifferentiableAt ℝ (fun x : SqEdges => dihedralAngle3Sq x f)
508 freudenthalTetSqEdges :=
509 hC.differentiableAt (by simp)
510 have hF : HasFDerivAt (fun x : SqEdges => dihedralAngle3Sq x f)
511 (fderiv ℝ (fun x : SqEdges => dihedralAngle3Sq x f) freudenthalTetSqEdges)
512 freudenthalTetSqEdges :=
513 hDiff.hasFDerivAt
514 have hγ : HasDerivAt
515 (fun t : ℝ => (fun j : Fin 6 => freudenthalTetSqEdges j + t * v j)) v 0 := by
516 rw [hasDerivAt_pi]
517 intro j
518 simpa using
519 ((hasDerivAt_id (0 : ℝ)).mul_const (v j)).const_add (freudenthalTetSqEdges j)
520 have hF' : HasFDerivAt (fun x : SqEdges => dihedralAngle3Sq x f)
521 (fderiv ℝ (fun x : SqEdges => dihedralAngle3Sq x f) freudenthalTetSqEdges)
522 (fun j : Fin 6 => freudenthalTetSqEdges j + (0 : ℝ) * v j) := by
523 simpa using hF
524 have hcomp := HasFDerivAt.comp_hasDerivAt (x := (0 : ℝ))
525 (f := fun t : ℝ => (fun j : Fin 6 => freudenthalTetSqEdges j + t * v j))
526 hF' hγ
527 have hvalue :
528 (fderiv ℝ (fun x : SqEdges => dihedralAngle3Sq x f) freudenthalTetSqEdges) v =
529 ∑ k : Fin 6, v k * flatAngleJacobian f k := by
530 rw [Geometry.ReggeActionFirstVariation.continuousLinearMap_apply_eq_sum_single]
531 refine Finset.sum_congr rfl fun k _ => ?_
532 exact congrArg (fun z => v k * z)
533 (Geometry.ReggeActionFirstVariation.fderiv_dihedralAngle3Sq_apply_single
534 freudenthalTet f k (flatCos_ne_endpoints f))
535 rw [hvalue] at hcomp
536 simpa [Function.comp_def] using hcomp
537
538/-- Directional derivative of one flat sqrt-edge factor (THEOREM): along
539the same affine path, `√((a + t·v)_f)` has derivative `v_f/(2√a_f)` at
540`t = 0`. -/
541theorem hasDerivAt_flatSqrtEdge_directional (v : Fin 6 → ℝ) (f : Fin 6) :
542 HasDerivAt (fun t : ℝ => Real.sqrt (freudenthalTetSqEdges f + t * v f))
543 (v f / (2 * Real.sqrt (freudenthalTetSqEdges f))) 0 := by
544 have hpos : 0 < freudenthalTetSqEdges f := freudenthalTet.sqEdge_pos f
545 have hinner : HasDerivAt (fun t : ℝ => freudenthalTetSqEdges f + t * v f) (v f) 0 := by
546 simpa using
547 ((hasDerivAt_id (0 : ℝ)).mul_const (v f)).const_add (freudenthalTetSqEdges f)
548 have hsq : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt (freudenthalTetSqEdges f)))
549 (freudenthalTetSqEdges f + (0 : ℝ) * v f) := by
550 simpa using Real.hasDerivAt_sqrt (ne_of_gt hpos)
551 have hcomp : HasDerivAt (fun t : ℝ => Real.sqrt (freudenthalTetSqEdges f + t * v f))
552 (1 / (2 * Real.sqrt (freudenthalTetSqEdges f)) * v f) 0 :=
553 hsq.comp (0 : ℝ) hinner
554 have hval : v f / (2 * Real.sqrt (freudenthalTetSqEdges f)) =
555 1 / (2 * Real.sqrt (freudenthalTetSqEdges f)) * v f := by ring
556 rw [hval]
557 exact hcomp
558
559/-- LANE A2, THE ONE-TET SCHLÄFLI SPIKE (THEOREM): along every affine
560squared-edge direction `v` through the flat Freudenthal tuple, the
561per-tetrahedron weighted angle sum `∑_f √a_f · θ_f(a)` is differentiable at
562flat with derivative `∑_f (v_f/(2√a_f)) · θ_f(flat)`. The product rule
563produces `∑_f [(√)'·θ + √·θ']`; the entire `θ'` group
564`∑_k v_k (∑_f √a_f · ∂θ_f/∂a_k)` vanishes term-by-term by the PROVED
565tetrahedral Schläfli identity (`flatAngleJacobian_schlaefli`). Only the
566sqrt-derivative group survives — exactly the structure the second-variation
567stage needs. -/
568theorem hasDerivAt_flatWeightedAngleSum (v : Fin 6 → ℝ) :
569 HasDerivAt
570 (fun t : ℝ => ∑ f : Fin 6,
571 Real.sqrt (freudenthalTetSqEdges f + t * v f) *
572 dihedralAngle3Sq (fun j : Fin 6 => freudenthalTetSqEdges j + t * v j) f)
573 (∑ f : Fin 6,
574 v f / (2 * Real.sqrt (freudenthalTetSqEdges f)) *
575 dihedralAngle3Sq freudenthalTetSqEdges f) 0 := by
576 have hterm : ∀ f : Fin 6, HasDerivAt
577 (fun t : ℝ =>
578 Real.sqrt (freudenthalTetSqEdges f + t * v f) *
579 dihedralAngle3Sq (fun j : Fin 6 => freudenthalTetSqEdges j + t * v j) f)
580 (v f / (2 * Real.sqrt (freudenthalTetSqEdges f)) *
581 dihedralAngle3Sq freudenthalTetSqEdges f +
582 Real.sqrt (freudenthalTetSqEdges f) *
583 (∑ k : Fin 6, v k * flatAngleJacobian f k)) 0 := by
584 intro f
585 have h := (hasDerivAt_flatSqrtEdge_directional v f).mul
586 (hasDerivAt_flatAngle_directional v f)
587 simpa using h
588 have hsum := HasDerivAt.sum (u := Finset.univ)
589 (A := fun f t =>
590 Real.sqrt (freudenthalTetSqEdges f + t * v f) *
591 dihedralAngle3Sq (fun j : Fin 6 => freudenthalTetSqEdges j + t * v j) f)
592 (A' := fun f =>
593 v f / (2 * Real.sqrt (freudenthalTetSqEdges f)) *
594 dihedralAngle3Sq freudenthalTetSqEdges f +
595 Real.sqrt (freudenthalTetSqEdges f) *
596 (∑ k : Fin 6, v k * flatAngleJacobian f k))
597 (x := 0) (fun f _ => hterm f)
598 have hcancel : (∑ f : Fin 6, Real.sqrt (freudenthalTetSqEdges f) *
599 (∑ k : Fin 6, v k * flatAngleJacobian f k)) = 0 := by
600 calc
601 (∑ f : Fin 6, Real.sqrt (freudenthalTetSqEdges f) *
602 (∑ k : Fin 6, v k * flatAngleJacobian f k))
603 = ∑ k : Fin 6, v k *
604 (∑ f : Fin 6, Real.sqrt (freudenthalTetSqEdges f) *
605 flatAngleJacobian f k) := by
606 simp_rw [Finset.mul_sum]
607 rw [Finset.sum_comm]
608 refine Finset.sum_congr rfl fun k _ => ?_
609 refine Finset.sum_congr rfl fun f _ => ?_
610 ring
611 _ = 0 := by
612 refine Finset.sum_eq_zero fun k _ => ?_
613 rw [flatAngleJacobian_schlaefli k]
614 ring
615 have hfinal :
616 (∑ f : Fin 6,
617 (v f / (2 * Real.sqrt (freudenthalTetSqEdges f)) *
618 dihedralAngle3Sq freudenthalTetSqEdges f +
619 Real.sqrt (freudenthalTetSqEdges f) *
620 (∑ k : Fin 6, v k * flatAngleJacobian f k))) =
621 ∑ f : Fin 6,
622 v f / (2 * Real.sqrt (freudenthalTetSqEdges f)) *
623 dihedralAngle3Sq freudenthalTetSqEdges f := by
624 rw [Finset.sum_add_distrib, hcancel, add_zero]
625 rw [hfinal] at hsum
626 exact hsum
627
628/-! ## §7. Lane A3 — the flat Jacobian rows as pure cofactor algebra
629
630Every row of `flatAngleJacobian` is `-(arccos factor) × (closed-form
631cofactor cosine derivative)`, with the arccos factor evaluated to exact
632radicals (`√2, 1, 2/√3, 1, 1, √2`) — ZERO arccos values remain. The
633`f = 0` row is then fully evaluated to exact rationals through the proved
634Schläfli radical bridge (the row is `(1/4)·(rationalized summand)` at flat,
635and the rationalized summand is radical-free cofactor algebra). -/
636
637/-- The exact arccos chain-rule factors `1/√(1-c_f²)` at the flat point:
638`√2, 1, 2/√3, 1, 1, √2`. -/
639def flatArccosFactor : Fin 6 → ℝ
640 | 0 => Real.sqrt 2
641 | 1 => 1
642 | 2 => 2 / Real.sqrt 3
643 | 3 => 1
644 | 4 => 1
645 | 5 => Real.sqrt 2
646
647private theorem inv_sqrt_half : 1 / Real.sqrt (1 - (Real.sqrt 2 / 2) ^ 2) = Real.sqrt 2 := by
648 have h2 : Real.sqrt 2 ^ 2 = 2 := Real.sq_sqrt (by norm_num)
649 rw [show (1 : ℝ) - (Real.sqrt 2 / 2) ^ 2 = 1 / 2 by rw [div_pow, h2]; norm_num]
650 rw [show (1 / 2 : ℝ) = 2⁻¹ by norm_num, Real.sqrt_inv, one_div, inv_inv]
651
652private theorem inv_sqrt_three_quarters :
653 1 / Real.sqrt (1 - (1 / 2 : ℝ) ^ 2) = 2 / Real.sqrt 3 := by
654 rw [show (1 : ℝ) - (1 / 2 : ℝ) ^ 2 = 3 / 4 by norm_num]
655 rw [Real.sqrt_div (by norm_num : (0 : ℝ) ≤ 3) 4]
656 rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2)]
657 rw [one_div_div]
658
659private theorem arccosFactor₀ :
660 1 / Real.sqrt (1 - dihedralCos3Sq freudenthalTetSqEdges 0 ^ 2) = Real.sqrt 2 := by
661 rw [flatCos₀]; exact inv_sqrt_half
662
663private theorem arccosFactor₁ :
664 1 / Real.sqrt (1 - dihedralCos3Sq freudenthalTetSqEdges 1 ^ 2) = 1 := by
665 rw [flatCos₁]; norm_num
666
667private theorem arccosFactor₂ :
668 1 / Real.sqrt (1 - dihedralCos3Sq freudenthalTetSqEdges 2 ^ 2) = 2 / Real.sqrt 3 := by
669 rw [flatCos₂]; exact inv_sqrt_three_quarters
670
671private theorem arccosFactor₃ :
672 1 / Real.sqrt (1 - dihedralCos3Sq freudenthalTetSqEdges 3 ^ 2) = 1 := by
673 rw [flatCos₃]; norm_num
674
675private theorem arccosFactor₄ :
676 1 / Real.sqrt (1 - dihedralCos3Sq freudenthalTetSqEdges 4 ^ 2) = 1 := by
677 rw [flatCos₄]; norm_num
678
679private theorem arccosFactor₅ :
680 1 / Real.sqrt (1 - dihedralCos3Sq freudenthalTetSqEdges 5 ^ 2) = Real.sqrt 2 := by
681 rw [flatCos₅]; exact inv_sqrt_half
682
683/-- LANE A3 ARCCOS FACTOR EVALUATION (THEOREM): at the flat point the
684arccos chain-rule multiplier `1/√(1-c_f²)` equals the exact radical table
685`flatArccosFactor` — `c = √2/2` gives `√2`, `c = 0` gives `1`, `c = 1/2`
686gives `2/√3`. -/
687theorem flatArccosFactor_spec (f : Fin 6) :
688 1 / Real.sqrt (1 - dihedralCos3Sq freudenthalTetSqEdges f ^ 2) =
689 flatArccosFactor f := by
690 fin_cases f
691 · exact arccosFactor₀
692 · exact arccosFactor₁
693 · exact arccosFactor₂
694 · exact arccosFactor₃
695 · exact arccosFactor₄
696 · exact arccosFactor₅
697
698/-- LANE A3 ROW NORMALIZATION (THEOREM): every entry of the flat angle
699Jacobian is pure cofactor algebra times the exactly evaluated arccos
700factor — `flatAngleJacobian f k = -(factor_f) · (closed-form cofactor
701cosine derivative at flat)`, with NO arccos value anywhere on the right. -/
702theorem flatAngleJacobian_cofactor_form (f k : Fin 6) :
703 flatAngleJacobian f k =
704 -(flatArccosFactor f) *
705 Geometry.CofactorDerivatives.dihedralCos3SqClosedFormDeriv
706 freudenthalTetSqEdges f k := by
707 unfold flatAngleJacobian
708 rw [Geometry.DihedralDerivatives.dihedralAngle3SqClosedFormDeriv_def,
709 ← flatArccosFactor_spec f]
710
711/-- The `f = 0` Jacobian row through the proved Schläfli radical bridge: at
712the flat tuple (`√a₀ = 1`, `√(2·cm3) = 4`) the row is `(1/4)` times the
713RADICAL-FREE rationalized Schläfli summand. This is the exact convention
714manifest Lane B mirrors: the row is pure rational cofactor algebra. -/
715theorem flatAngleJacobian_row0_norm (k : Fin 6) :
716 flatAngleJacobian 0 k =
717 (1 / 4 : ℝ) *
718 Geometry.SchlaefliTetrahedronProof.schlaefliPolySummandNorm
719 freudenthalTetSqEdges 0 k := by
720 have hb := Geometry.SchlaefliTetrahedronProof.schlaefli_summand_bridge_edge0
721 freudenthalTet k
722 have h1 : Real.sqrt (freudenthalTet.sqEdge 0) = 1 := by
723 rw [show freudenthalTet.sqEdge 0 = 1 from rfl, Real.sqrt_one]
724 have h4 : Real.sqrt (2 * cm3 freudenthalTet.sqEdge) = 4 := by
725 have hcm : cm3 freudenthalTet.sqEdge = 8 := cm3_freudenthalTetSqEdges
726 rw [hcm, show (2 : ℝ) * 8 = 4 ^ 2 by norm_num,
727 Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 4)]
728 rw [h1, one_mul, h4] at hb
729 have hkey : flatAngleJacobian 0 k =
730 Geometry.SchlaefliTetrahedronProof.dihedralClosedDerivSqPoly freudenthalTet 0 k := by
731 rw [flatAngleJacobian_eq_dihedralClosedDerivSq]
732 exact Geometry.SchlaefliTetrahedronProof.dihedralClosedDerivSq_eq_poly
733 freudenthalTet 0 k
734 rw [hkey, hb]
735 rfl
736
737/-- The exact `f = 0` Jacobian row values at the flat tuple. -/
738def flatAngleJacobianRow0 : Fin 6 → ℝ
739 | 0 => 0
740 | 1 => 0
741 | 2 => 0
742 | 3 => 0
743 | 4 => -(1 / 4)
744 | 5 => 1 / 2
745
746/-- LANE A3 ROW `f = 0` FULL EVALUATION (THEOREM): the flat angle Jacobian
747row `f = 0` is exactly `(0, 0, 0, 0, -1/4, 1/2)` — exact rationals, no
748radicals survive (the arccos factor `√2` cancels against the `1/√32`
749cofactor denominator through the Schläfli radical bridge). -/
750theorem flatAngleJacobian_row0_eval (k : Fin 6) :
751 flatAngleJacobian 0 k = flatAngleJacobianRow0 k := by
752 rw [flatAngleJacobian_row0_norm k]
753 fin_cases k <;>
754 norm_num [flatAngleJacobianRow0,
755 Geometry.SchlaefliTetrahedronProof.schlaefliPolySummandNorm,
756 Geometry.CofactorPolynomial.cmCofactor3Poly,
757 Geometry.CofactorPolynomial.cmCofactorPartial,
758 Geometry.FreudenthalCubeTriangulation.freudenthalTetSqEdges]
759
760end
761
762end ReggeTTDerivativeGate
763end Analysis
764end Gravity
765end IndisputableMonolith
766