IndisputableMonolith.Gravity.Analysis.ReggeTTBlochAssembly
IndisputableMonolith/Gravity/Analysis/ReggeTTBlochAssembly.lean · 423 lines · 26 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode
2import IndisputableMonolith.Gravity.Analysis.BlochCellSum
3
4/-!
5# Regge TT finite Bloch assembly
6
7This module is the C-DAG1 finite-cell assembly stage. The cosine evaluator
8is defined directly from a bucket's integer phase key, independently of any
9quadratic moment evaluator.
10
11For every side length and commensurate integer wave vector whose doubled
12frequency is non-aliased in one coordinate, the normalized canonical finite
13value equals the raw bucket-fiber Bloch fold exactly. The proof uses
14`BlochCellSum.cellSum_cos_mul_cos`; periodic wrapping in `localEdgeOf` is
15handled by an explicit integer-turn phase decomposition and cosine
16periodicity.
17
18No spike or continuum-certificate module is imported.
19-/
20
21namespace IndisputableMonolith
22namespace Gravity
23namespace Analysis
24namespace ReggeTTBlochAssembly
25
26open Geometry.PeriodicFreudenthalTorus
27open ReggeTTSymbolPreflight
28open ReggeTTBlochInterfaceAudit
29open ReggeTTHingeAwareZeroMode (slotDispClass slotDispClass_grounded)
30
31noncomputable section
32
33/-! ## Cell-relative phases and periodic wrapping -/
34
35/-- A coordinate of a periodic vertex as a natural representative. -/
36def vertexNatCoord {N : ℕ} (x : Vertex N N N) : Fin 3 → ℕ
37 | 0 => x.1.val
38 | 1 => x.2.1.val
39 | 2 => x.2.2.val
40
41/-- The selected Boolean coordinate of a cube vertex label. -/
42def cubeVertexBit (a : Fin 8) : Fin 3 → Bool
43 | 0 => (vertexBits a).1
44 | 1 => (vertexBits a).2.1
45 | 2 => (vertexBits a).2.2
46
47/-- The base-vertex bit of local slot `f` in tetrahedron type `t`. -/
48def slotBaseBit (t f : Fin 6) (i : Fin 3) : Bool :=
49 cubeVertexBit
50 (cubeEdgeBase (Geometry.FreudenthalCubeTriangulation.localEdgeOf t f)) i
51
52/-- The selected Boolean coordinate of a positive cube displacement. -/
53def cubeDispBit (d : Fin 7) : Fin 3 → Bool
54 | 0 => (dispBits d).1
55 | 1 => (dispBits d).2.1
56 | 2 => (dispBits d).2.2
57
58/-- The displacement bit of local slot `f` in tetrahedron type `t`. -/
59def slotDispBit (t f : Fin 6) (i : Fin 3) : Bool :=
60 cubeDispBit
61 (cubeEdgeDisp (Geometry.FreudenthalCubeTriangulation.localEdgeOf t f)) i
62
63/-- Geometry-derived doubled midpoint coordinate of a local edge slot:
64twice its base offset plus its positive displacement bit. -/
65def slotMidTwice (t f : Fin 6) (i : Fin 3) : ℤ :=
66 2 * (bit (slotBaseBit t f i) : ℤ) + (bit (slotDispBit t f i) : ℤ)
67
68/-- Number of periodic wraps made by the base-vertex translation in one
69coordinate. Since the translation bit is zero or one this is zero or one,
70but the quotient form gives the exact modular identity without cases. -/
71def slotWrapCount (N : ℕ) (cell : Vertex N N N) (t f : Fin 6)
72 (i : Fin 3) : ℕ :=
73 (vertexNatCoord cell i + bit (slotBaseBit t f i)) / N
74
75/-- Total integer number of phase turns removed by periodic wrapping. -/
76def slotWrapTurns (N : ℕ) (m : Fin 3 → ℤ) (cell : Vertex N N N)
77 (t f : Fin 6) : ℤ :=
78 ∑ i : Fin 3, m i * (slotWrapCount N cell t f i : ℤ)
79
80/-- The cell-independent midpoint phase of one local edge slot. -/
81def slotPhase (N : ℕ) [NeZero N] (m : Fin 3 → ℤ) (t f : Fin 6) : ℝ :=
82 ∑ i : Fin 3,
83 commensurateMomentum N m i * (((slotMidTwice t f i : ℤ) : ℝ) / 2)
84
85/-- Cosine phase evaluator on a raw bucket. This definition is direct from
86the integer phase key and does not mention `rawPhaseQuadratic`. -/
87def rawCosineEvaluator (N : ℕ) [NeZero N] (m : Fin 3 → ℤ)
88 (b : Bucket) : ℝ :=
89 Real.cos
90 (∑ i : Fin 3,
91 commensurateMomentum N m i * (((b.phase i : ℤ) : ℝ) / 2))
92
93/-- Bucket key of one raw stencil triple. Its phase is the doubled
94midpoint displacement from the left slot to the right slot. -/
95def bucketKeyOf (p : Fin 6 × Fin 6 × Fin 6) : Bucket :=
96 ⟨p.2.1, p.2.2,
97 fun i => slotMidTwice p.1 p.2.2 i - slotMidTwice p.1 p.2.1 i⟩
98
99/-- Finite support of the raw cosine fold, obtained as the image of all
100216 tetrahedron/slot triples under the geometry-derived bucket key. -/
101def rawCosineSupport : Finset Bucket :=
102 Finset.univ.image bucketKeyOf
103
104/-- Signed cell-independent coefficient of one raw stencil triple. -/
105def rawTripleWeight (E : Fin 3 → Fin 3 → ℝ)
106 (p : Fin 6 × Fin 6 × Fin 6) : ℝ :=
107 -(rawJacobianCoefficient p.2.1 p.2.2 *
108 polEdgeCoeff E (slotDispClass p.1 p.2.1) *
109 polEdgeCoeff E (slotDispClass p.1 p.2.2))
110
111/-- Honest bucket-fiber aggregation of the signed raw stencil weights. -/
112def rawBucketAmplitude (E : Fin 3 → Fin 3 → ℝ) (b : Bucket) : ℝ :=
113 ∑ p ∈ Finset.univ.filter (fun p => bucketKeyOf p = b),
114 rawTripleWeight E p
115
116private theorem addBit_val_real (N : ℕ) [NeZero N] (x : Fin N) (b : Bool) :
117 ((addBit x b).val : ℝ) =
118 (x.val : ℝ) + (bit b : ℝ) -
119 (N : ℝ) * (((x.val + bit b) / N : ℕ) : ℝ) := by
120 have hnat :
121 (x.val + bit b) % N + N * ((x.val + bit b) / N) =
122 x.val + bit b :=
123 Nat.mod_add_div (x.val + bit b) N
124 have hreal :
125 (((x.val + bit b) % N : ℕ) : ℝ) +
126 (N : ℝ) * (((x.val + bit b) / N : ℕ) : ℝ) =
127 (x.val : ℝ) + (bit b : ℝ) := by
128 exact_mod_cast hnat
129 change ((((x.val + bit b) % N : ℕ) : ℝ)) =
130 (x.val : ℝ) + (bit b : ℝ) -
131 (N : ℝ) * (((x.val + bit b) / N : ℕ) : ℝ)
132 linarith
133
134private theorem vertCoord_addVertexBits (N : ℕ) [NeZero N]
135 (cell : Vertex N N N) (a : Fin 8) (i : Fin 3) :
136 vertCoord N (addVertexBits cell a) i =
137 (vertexNatCoord cell i : ℝ) + (bit (cubeVertexBit a i) : ℝ) -
138 (N : ℝ) *
139 (((vertexNatCoord cell i + bit (cubeVertexBit a i)) / N : ℕ) : ℝ) := by
140 fin_cases i <;>
141 simp only [vertCoord, addVertexBits, addBits, vertexNatCoord, cubeVertexBit] <;>
142 apply addBit_val_real
143
144/-- The literal doubled-midpoint table is exactly twice the base bit plus
145the actual displacement vector, coordinate by coordinate. -/
146theorem slotMidTwice_eq_geometry (N : ℕ) [NeZero N]
147 (cell : Vertex N N N) (t f : Fin 6) (i : Fin 3) :
148 (((slotMidTwice t f i : ℤ) : ℝ) / 2) =
149 (bit (slotBaseBit t f i) : ℝ) +
150 FreudenthalStencilPreflight.dispReal (localEdgeOf cell t f).disp i / 2 := by
151 fin_cases t <;> fin_cases f <;> fin_cases i <;>
152 norm_num [slotMidTwice, slotBaseBit, slotDispBit, cubeVertexBit,
153 cubeDispBit, localEdgeOf,
154 Geometry.FreudenthalCubeTriangulation.localEdgeOf, cubeEdgeBase,
155 cubeEdgeDisp, vertexBits, dispBits, bit,
156 FreudenthalStencilPreflight.dispReal]
157
158/-- Exact phase decomposition for every cell, including periodic seams.
159The wrapped representative differs from the unwrapped cell-relative phase
160by an integral number of full turns. -/
161theorem localEdge_phase_decomposition (N : ℕ) [NeZero N]
162 (m : Fin 3 → ℤ) (cell : Vertex N N N) (t f : Fin 6) :
163 edgeMidpointPhase N (commensurateMomentum N m) (localEdgeOf cell t f) =
164 BlochCellSum.theta N m cell + slotPhase N m t f -
165 2 * Real.pi * (slotWrapTurns N m cell t f : ℝ) := by
166 have hwrap :
167 (slotWrapTurns N m cell t f : ℝ) =
168 ∑ i : Fin 3, (m i : ℝ) * (slotWrapCount N cell t f i : ℝ) := by
169 unfold slotWrapTurns
170 rw [Int.cast_sum]
171 refine Finset.sum_congr rfl fun i _ => ?_
172 norm_cast
173 unfold edgeMidpointPhase slotPhase
174 simp only [Fin.sum_univ_three]
175 rw [show (localEdgeOf cell t f).base =
176 addVertexBits cell
177 (cubeEdgeBase
178 (Geometry.FreudenthalCubeTriangulation.localEdgeOf t f)) from rfl]
179 rw [vertCoord_addVertexBits N cell _ 0,
180 vertCoord_addVertexBits N cell _ 1,
181 vertCoord_addVertexBits N cell _ 2]
182 rw [slotMidTwice_eq_geometry N cell t f 0,
183 slotMidTwice_eq_geometry N cell t f 1,
184 slotMidTwice_eq_geometry N cell t f 2]
185 rw [hwrap]
186 unfold BlochCellSum.theta commensurateMomentum slotWrapCount
187 simp only [Fin.sum_univ_three]
188 unfold slotBaseBit vertexNatCoord
189 push_cast
190 have hN : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne N)
191 field_simp [hN]
192 ring
193
194/-- Cosine form of the phase decomposition. Integral seam corrections
195disappear by `2*pi` periodicity. -/
196theorem cos_localEdge_eq_cell_slot (N : ℕ) [NeZero N]
197 (m : Fin 3 → ℤ) (cell : Vertex N N N) (t f : Fin 6) :
198 Real.cos
199 (edgeMidpointPhase N (commensurateMomentum N m)
200 (localEdgeOf cell t f)) =
201 Real.cos (BlochCellSum.theta N m cell + slotPhase N m t f) := by
202 rw [localEdge_phase_decomposition N m cell t f]
203 rw [show 2 * Real.pi * (slotWrapTurns N m cell t f : ℝ) =
204 (slotWrapTurns N m cell t f : ℝ) * (2 * Real.pi) by ring]
205 exact Real.cos_sub_int_mul_two_pi _ _
206
207/-! ## Raw triple and bucket assembly -/
208
209/-- The bucket cosine for a raw triple is the cosine of the difference of
210its two cell-independent slot phases. -/
211theorem rawCosineEvaluator_bucketKeyOf (N : ℕ) [NeZero N]
212 (m : Fin 3 → ℤ) (p : Fin 6 × Fin 6 × Fin 6) :
213 rawCosineEvaluator N m (bucketKeyOf p) =
214 Real.cos (slotPhase N m p.1 p.2.1 - slotPhase N m p.1 p.2.2) := by
215 unfold rawCosineEvaluator bucketKeyOf slotPhase
216 have harg :
217 (∑ i : Fin 3,
218 commensurateMomentum N m i *
219 (((slotMidTwice p.1 p.2.2 i - slotMidTwice p.1 p.2.1 i : ℤ) : ℝ) / 2)) =
220 -(∑ i : Fin 3,
221 commensurateMomentum N m i * (((slotMidTwice p.1 p.2.1 i : ℤ) : ℝ) / 2) -
222 ∑ i : Fin 3,
223 commensurateMomentum N m i *
224 (((slotMidTwice p.1 p.2.2 i : ℤ) : ℝ) / 2)) := by
225 simp only [Fin.sum_univ_three]
226 push_cast
227 ring
228 rw [harg, Real.cos_neg]
229
230/-- One signed raw stencil term is a cell-independent raw triple weight
231times the two phase-shifted cell cosines. -/
232theorem neg_rawCellStencilTerm_eq (N : ℕ) [NeZero N]
233 (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ)
234 (cell : Vertex N N N) (t f g : Fin 6) :
235 -rawCellStencilTerm N E m (cell, t) f g =
236 rawTripleWeight E (t, f, g) *
237 Real.cos (BlochCellSum.theta N m cell + slotPhase N m t f) *
238 Real.cos (BlochCellSum.theta N m cell + slotPhase N m t g) := by
239 unfold rawCellStencilTerm rawTripleWeight
240 unfold ReggeTTLocalSymbolExistence.planeWaveTetVelocity
241 rw [slotDispClass_grounded N cell t f, slotDispClass_grounded N cell t g]
242 rw [cos_localEdge_eq_cell_slot N m cell t f,
243 cos_localEdge_eq_cell_slot N m cell t g]
244 unfold ReggeTTBlochInterfaceAudit.rawJacobianCoefficient
245 ring
246
247/-- The raw cosine bucket fold expands to the plain sum over all 216 raw
248triples, with bucket collisions retained through the fiber amplitude. -/
249theorem rawCosineFold_eq_rawTripleSum (N : ℕ) [NeZero N]
250 (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ) :
251 reggeTTBlochFold rawCosineSupport (rawCosineEvaluator N m)
252 (rawBucketAmplitude E) =
253 ∑ p : Fin 6 × Fin 6 × Fin 6,
254 rawCosineEvaluator N m (bucketKeyOf p) * rawTripleWeight E p := by
255 unfold reggeTTBlochFold rawCosineSupport
256 rw [Finset.sum_image' (fun p : Fin 6 × Fin 6 × Fin 6 =>
257 rawCosineEvaluator N m (bucketKeyOf p) * rawTripleWeight E p)]
258 intro p _
259 unfold rawBucketAmplitude
260 rw [Finset.mul_sum]
261 refine Finset.sum_congr rfl fun q hq => ?_
262 have hkey : bucketKeyOf q = bucketKeyOf p := (Finset.mem_filter.mp hq).2
263 rw [hkey]
264
265/-- Exact cell sum for one raw triple under the one-coordinate doubled
266frequency non-aliasing hypothesis. -/
267theorem rawTriple_cellSum (N : ℕ) [NeZero N]
268 (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ)
269 (p : Fin 6 × Fin 6 × Fin 6)
270 (halias : ∃ i : Fin 3, ¬ (N : ℤ) ∣ 2 * m i) :
271 (∑ cell : Vertex N N N,
272 rawTripleWeight E p *
273 Real.cos (BlochCellSum.theta N m cell + slotPhase N m p.1 p.2.1) *
274 Real.cos (BlochCellSum.theta N m cell + slotPhase N m p.1 p.2.2)) =
275 rawTripleWeight E p * ((N : ℝ) ^ 3 / 2) *
276 rawCosineEvaluator N m (bucketKeyOf p) := by
277 have hcell := BlochCellSum.cellSum_cos_mul_cos N m
278 (slotPhase N m p.1 p.2.1) (slotPhase N m p.1 p.2.2) halias
279 calc
280 (∑ cell : Vertex N N N,
281 rawTripleWeight E p *
282 Real.cos (BlochCellSum.theta N m cell + slotPhase N m p.1 p.2.1) *
283 Real.cos (BlochCellSum.theta N m cell + slotPhase N m p.1 p.2.2))
284 = rawTripleWeight E p *
285 ∑ cell : Vertex N N N,
286 Real.cos
287 (BlochCellSum.theta N m cell + slotPhase N m p.1 p.2.1) *
288 Real.cos
289 (BlochCellSum.theta N m cell + slotPhase N m p.1 p.2.2) := by
290 rw [Finset.mul_sum]
291 refine Finset.sum_congr rfl fun cell _ => ?_
292 ring
293 _ = rawTripleWeight E p * ((N : ℝ) ^ 3 / 2) *
294 rawCosineEvaluator N m (bucketKeyOf p) := by
295 rw [hcell, rawCosineEvaluator_bucketKeyOf N m p]
296 ring
297
298/-- FINITE ASSEMBLY HEADLINE: under exact doubled-frequency non-aliasing,
299the Schlaefli-reduced raw stencil equals the raw bucket cosine fold. -/
300theorem rawCellStencil_eq_rawCosineBlochFold (N : ℕ) [NeZero N]
301 (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ)
302 (halias : ∃ i : Fin 3, ¬ (N : ℤ) ∣ 2 * m i) :
303 rawCellStencil N E m =
304 reggeTTBlochFold rawCosineSupport (rawCosineEvaluator N m)
305 (rawBucketAmplitude E) := by
306 unfold rawCellStencil
307 have hregroup :
308 -(∑ τ : PeriodicTet N N N, ∑ f : Fin 6, ∑ g : Fin 6,
309 rawCellStencilTerm N E m τ f g) =
310 ∑ p : Fin 6 × Fin 6 × Fin 6, ∑ cell : Vertex N N N,
311 rawTripleWeight E p *
312 Real.cos (BlochCellSum.theta N m cell + slotPhase N m p.1 p.2.1) *
313 Real.cos (BlochCellSum.theta N m cell + slotPhase N m p.1 p.2.2) := by
314 calc
315 -(∑ τ : PeriodicTet N N N, ∑ f : Fin 6, ∑ g : Fin 6,
316 rawCellStencilTerm N E m τ f g)
317 = ∑ cell : Vertex N N N, ∑ t : Fin 6, ∑ f : Fin 6, ∑ g : Fin 6,
318 -rawCellStencilTerm N E m (cell, t) f g := by
319 rw [Fintype.sum_prod_type, ← Finset.sum_neg_distrib]
320 refine Finset.sum_congr rfl fun cell _ => ?_
321 rw [← Finset.sum_neg_distrib]
322 refine Finset.sum_congr rfl fun t _ => ?_
323 rw [← Finset.sum_neg_distrib]
324 refine Finset.sum_congr rfl fun f _ => ?_
325 rw [← Finset.sum_neg_distrib]
326 _ = ∑ t : Fin 6, ∑ f : Fin 6, ∑ g : Fin 6, ∑ cell : Vertex N N N,
327 -rawCellStencilTerm N E m (cell, t) f g := by
328 rw [Finset.sum_comm]
329 refine Finset.sum_congr rfl fun t _ => ?_
330 rw [Finset.sum_comm]
331 refine Finset.sum_congr rfl fun f _ => ?_
332 rw [Finset.sum_comm]
333 _ = ∑ t : Fin 6, ∑ f : Fin 6, ∑ g : Fin 6, ∑ cell : Vertex N N N,
334 rawTripleWeight E (t, f, g) *
335 Real.cos (BlochCellSum.theta N m cell + slotPhase N m t f) *
336 Real.cos
337 (BlochCellSum.theta N m cell + slotPhase N m t g) := by
338 refine Finset.sum_congr rfl fun t _ => ?_
339 refine Finset.sum_congr rfl fun f _ => ?_
340 refine Finset.sum_congr rfl fun g _ => ?_
341 exact Finset.sum_congr rfl fun cell _ =>
342 neg_rawCellStencilTerm_eq N E m cell t f g
343 _ = ∑ p : Fin 6 × Fin 6 × Fin 6, ∑ cell : Vertex N N N,
344 rawTripleWeight E p *
345 Real.cos
346 (BlochCellSum.theta N m cell + slotPhase N m p.1 p.2.1) *
347 Real.cos
348 (BlochCellSum.theta N m cell + slotPhase N m p.1 p.2.2) := by
349 rw [Fintype.sum_prod_type]
350 refine Finset.sum_congr rfl fun t _ => ?_
351 rw [Fintype.sum_prod_type]
352 rw [hregroup]
353 rw [Finset.sum_congr rfl fun p _ => rawTriple_cellSum N E m p halias]
354 have hNcast : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne N)
355 have hN : (N : ℝ) ^ (3 : ℕ) ≠ 0 := by
356 positivity
357 have hcancel :
358 (2 / (N : ℝ) ^ (3 : ℕ)) * ((N : ℝ) ^ (3 : ℕ) / 2) = 1 := by
359 field_simp [hNcast]
360 calc
361 (2 / (N : ℝ) ^ (3 : ℕ)) *
362 ∑ p : Fin 6 × Fin 6 × Fin 6,
363 rawTripleWeight E p * ((N : ℝ) ^ 3 / 2) *
364 rawCosineEvaluator N m (bucketKeyOf p)
365 = ∑ p : Fin 6 × Fin 6 × Fin 6,
366 rawCosineEvaluator N m (bucketKeyOf p) * rawTripleWeight E p := by
367 rw [Finset.mul_sum]
368 refine Finset.sum_congr rfl fun p _ => ?_
369 calc
370 (2 / (N : ℝ) ^ (3 : ℕ)) *
371 (rawTripleWeight E p * ((N : ℝ) ^ 3 / 2) *
372 rawCosineEvaluator N m (bucketKeyOf p))
373 = ((2 / (N : ℝ) ^ (3 : ℕ)) *
374 ((N : ℝ) ^ (3 : ℕ) / 2)) *
375 (rawTripleWeight E p *
376 rawCosineEvaluator N m (bucketKeyOf p)) := by ring
377 _ = rawCosineEvaluator N m (bucketKeyOf p) *
378 rawTripleWeight E p := by
379 rw [hcancel, one_mul]
380 ring
381 _ = reggeTTBlochFold rawCosineSupport (rawCosineEvaluator N m)
382 (rawBucketAmplitude E) :=
383 (rawCosineFold_eq_rawTripleSum N E m).symm
384
385/-- CANONICAL FINITE ASSEMBLY: the actual reduced finite second variation
386equals the raw bucket cosine fold under the same non-aliasing condition. -/
387theorem canonicalFiniteH_eq_rawCosineBlochFold (N : ℕ) [NeZero N]
388 (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ)
389 (halias : ∃ i : Fin 3, ¬ (N : ℤ) ∣ 2 * m i) :
390 canonicalFiniteH N E m =
391 reggeTTBlochFold rawCosineSupport (rawCosineEvaluator N m)
392 (rawBucketAmplitude E) := by
393 rw [a2_reduced_eq_rawCellStencil,
394 rawCellStencil_eq_rawCosineBlochFold N E m halias]
395
396/-- For every fixed nonzero integer mode, the canonical finite assembly
397identity holds at every sufficiently large side length. The explicit
398`NeZero N` argument only supplies the existing finite-torus definitions. -/
399theorem eventually_canonicalFiniteH_eq_rawCosineBlochFold
400 (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ)
401 (hm : ∃ i : Fin 3, m i ≠ 0) :
402 ∀ᶠ N : ℕ in Filter.atTop, ∀ hN : NeZero N,
403 @canonicalFiniteH N hN E m =
404 reggeTTBlochFold rawCosineSupport (@rawCosineEvaluator N hN m)
405 (rawBucketAmplitude E) := by
406 filter_upwards [BlochCellSum.eventually_nonaliased m hm] with N halias
407 intro hN
408 letI : NeZero N := hN
409 exact canonicalFiniteH_eq_rawCosineBlochFold N E m halias
410
411end
412
413end ReggeTTBlochAssembly
414end Analysis
415end Gravity
416end IndisputableMonolith
417
418#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTBlochAssembly.localEdge_phase_decomposition
419#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTBlochAssembly.cos_localEdge_eq_cell_slot
420#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTBlochAssembly.rawCellStencil_eq_rawCosineBlochFold
421#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTBlochAssembly.canonicalFiniteH_eq_rawCosineBlochFold
422#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTBlochAssembly.eventually_canonicalFiniteH_eq_rawCosineBlochFold
423