IndisputableMonolith.Gravity.Analysis.FreudenthalStencilPreflight
IndisputableMonolith/Gravity/Analysis/FreudenthalStencilPreflight.lean · 419 lines · 34 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Geometry.PeriodicFreudenthalTorus
3import IndisputableMonolith.Geometry.ReggeActionConcrete
4
5/-!
6# Freudenthal stencil preflight: exact general-N stencil identity and moment tensor
7
8QG full-theory campaign, Phase 2b, panel-locked Test G stage 1 (candidate C8,
9tensor-first anisotropic action continuum limit).
10
11Scope statement (panel-mandated): this module and its stage-2 companion
12(`FreudenthalEnergyLimit`) develop the action-level continuum limit of the
13frozen quadratic energy on the canonical Freudenthal family; scoped partial;
14the pillar-2 path-sum flag stays red (flipping it requires the
15refinement-indexed measure-weighted sum over inequivalent triangulation
16classes).
17
18## Status: THEOREM (everything below is proved, axiom-clean; no sorry, no
19## admit, no native_decide, no `: True` shells).
20
21## What this module proves
22
23Stage 1 of Test G, for EVERY side length `N > 2` (not just the `N = 5`
24certificates of `FreudenthalAxisStencilCoeffCert`):
25
26* `hessianQuadratic_canonical_eq_freudenthalStencil`: the quadratic form of
27 the canonical Regge Hessian `canonicalReggeHessian` on the canonical
28 periodic Freudenthal triangulation at side `N` is EXACTLY the seven-class
29 nearest-displacement stencil sum
30 `Σ_x Σ_{d : Fin 7} c_d · (u(x+d) − u(x))²`
31 with weights `c_d = √(ℓ²_d)` read off the Hessian's incidence dual weights
32 (`ℓ²` = 1,1,1,2,2,2,3 for the three axis, three face-diagonal, and one
33 body-diagonal displacement classes). Derived, never postulated: the chain
34 is `canonicalReggeHessian_quadratic_eq_dirichlet` (frozen quadratic form =
35 graph Dirichlet energy), then the no-self-loop edge-stencil reindexing of
36 `ReggeActionConcrete`, then the periodic-edge / (base, displacement)
37 product reindexing.
38* `freudenthal_stencil_identity`: the panel-locked normalized identity
39 `ρ(N) · Q_N(u) = h³ · Σ_x Σ_d c_d · ((u(x+d) − u(x))/h)²` with `h = 1/N`
40 and `ρ(N) = 1/N` stated A PRIORI (`stencilNormalization`, declared with
41 its dimensional justification before any limit computation; nothing is
42 fitted after the fact).
43* `stencilMomentTensor_eq`: the moment tensor `A₀ = Σ_d c_d · d dᵀ` is
44 computed exactly:
45 `A₀ = (1 + √2)·I + (√2 + √3)·J` (`J` = all-ones matrix), i.e. every
46 diagonal entry is `1 + 2√2 + √3` and every off-diagonal entry is
47 `√2 + √3`. The entries live in `ℚ[√2, √3]`, not `ℚ`; the brief's
48 "rational symmetric matrix" expectation is corrected by this exact
49 kernel-checked value.
50* `stencilMomentTensor_psd` / `stencilMomentTensor_diag_pos`: `A₀` is
51 positive semidefinite (kernel-proved via the exact sum-of-squares
52 decomposition `vᵀA₀v = Σ_d c_d ⟨d, v⟩²`) and nonzero.
53* `stencilMomentTensor_not_isotropic`: FINDING — `A₀` is NOT isotropic:
54 the off-diagonal entry `√2 + √3` is strictly positive, so `A₀ ≠ c·I` for
55 every `c`. The Freudenthal frozen quadratic energy carries an anisotropic
56 continuum quadratic form; its spectrum is `1 + √2` (multiplicity 2,
57 orthogonal to `(1,1,1)`) and `1 + 4√2 + 3√3` (direction `(1,1,1)`).
58
59Stage 2 (`FreudenthalEnergyLimit`) consumes `scaledCanonicalEnergy` and
60`stencilMomentTensor` from this file.
61-/
62
63namespace IndisputableMonolith
64namespace Gravity
65namespace Analysis
66namespace FreudenthalStencilPreflight
67
68open Geometry.PeriodicFreudenthalTorus
69open Geometry.ReggeActionConcrete
70open Geometry.ReggeHessian3D
71
72noncomputable section
73
74variable (N : ℕ) [NeZero N]
75
76/-! ## §1. The stencil data, read off the canonical Hessian -/
77
78/-- Displacement-class stencil weight: the square root of the squared edge
79length of displacement class `d`. This is DEFINITIONAL from the canonical
80Hessian: `canonicalDualWeight` sums `√(globalSqEdge e)` over incident edges,
81and on the canonical periodic triangulation `globalSqEdge` is
82`periodicDispSqEdge` of the edge's displacement class. -/
83def stencilWeight (d : Fin 7) : ℝ := Real.sqrt (periodicDispSqEdge d)
84
85/-- The stencil weight is exactly the Hessian dual-weight length factor of
86any canonical periodic edge in displacement class `d`: definitional
87transparency of `stencilWeight` (proof is `rfl`). -/
88theorem stencilWeight_eq_sqrt_globalSqEdge
89 (e : Fin (canonicalPeriodicTriangulation N N N).nE) :
90 Real.sqrt ((canonicalPeriodicIncidenceConsistent N N N).globalSqEdge e) =
91 stencilWeight ((edgeFinEquiv N N N e).disp) := rfl
92
93/-- Explicit values of the seven stencil weights:
94`√1, √1, √1, √2, √2, √2, √3` for the three axis classes, the three
95face-diagonal classes, and the body-diagonal class. -/
96theorem stencilWeight_values :
97 stencilWeight 0 = 1 ∧ stencilWeight 1 = 1 ∧ stencilWeight 2 = 1 ∧
98 stencilWeight 3 = Real.sqrt 2 ∧ stencilWeight 4 = Real.sqrt 2 ∧
99 stencilWeight 5 = Real.sqrt 2 ∧ stencilWeight 6 = Real.sqrt 3 := by
100 refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;>
101 norm_num [stencilWeight, periodicDispSqEdge, Real.sqrt_one]
102
103theorem stencilWeight_nonneg (d : Fin 7) : 0 ≤ stencilWeight d :=
104 Real.sqrt_nonneg _
105
106/-- Vertex shifted by one displacement class: `x + d` on the periodic torus.
107Definitional match with `PeriodicEdge.endpoints`: the edge with base `x` and
108class `d` has endpoints `(x, shiftVertex x d)`. -/
109def shiftVertex (x : Vertex N N N) (d : Fin 7) : Vertex N N N :=
110 addBits x (dispBits d).1 (dispBits d).2.1 (dispBits d).2.2
111
112theorem periodicEdge_endpoints_eq (edge : PeriodicEdge N N N) :
113 edge.endpoints = (edge.base, shiftVertex N edge.base edge.disp) := rfl
114
115/-- The seven-class Freudenthal stencil energy on arbitrary vertex data:
116`Σ_x Σ_{d ∈ D} c_d · (u(x+d) − u(x))²` over all `N³` base vertices and all
117seven displacement classes. -/
118def freudenthalStencilEnergy (u : Vertex N N N → ℝ) : ℝ :=
119 ∑ x : Vertex N N N, ∑ d : Fin 7,
120 stencilWeight d * (u (shiftVertex N x d) - u x) ^ (2 : ℕ)
121
122/-- Transport of vertex data along the canonical finite vertex indexing. -/
123def toPotential (u : Vertex N N N → ℝ) :
124 VertexPotential (canonicalPeriodicTriangulation N N N) :=
125 fun i => u (vertexFinEquiv N N N i)
126
127theorem toPotential_symm_apply (u : Vertex N N N → ℝ) (v : Vertex N N N) :
128 toPotential N u ((vertexFinEquiv N N N).symm v) = u v := by
129 unfold toPotential
130 rw [Equiv.apply_symm_apply]
131
132/-! ## §2. General-N derivation of the stencil identity from the Hessian -/
133
134theorem canonical_globalSqEdge_eq
135 (e : Fin (canonicalPeriodicTriangulation N N N).nE) :
136 (canonicalPeriodicIncidenceConsistent N N N).globalSqEdge e =
137 periodicDispSqEdge ((edgeFinEquiv N N N e).disp) := rfl
138
139theorem canonical_edgeVerts_eq
140 (e : Fin (canonicalPeriodicTriangulation N N N).nE) :
141 (canonicalPeriodicTriangulation N N N).edgeVerts e =
142 ((vertexFinEquiv N N N).symm (edgeFinEquiv N N N e).endpoints.1,
143 (vertexFinEquiv N N N).symm (edgeFinEquiv N N N e).endpoints.2) := rfl
144
145/-- For `N > 2` the canonical periodic triangulation has no self-loop edges:
146the side-length assumption rules out `x + d = x` wraparound. -/
147theorem canonicalPeriodic_noSelfLoopEdges (hN : 2 < N) :
148 NoSelfLoopEdges (canonicalPeriodicTriangulation N N N) := by
149 intro e h
150 rw [canonical_edgeVerts_eq] at h
151 exact PeriodicEdge.endpoints_ne hN hN hN (edgeFinEquiv N N N e)
152 ((vertexFinEquiv N N N).symm.injective h)
153
154/-- Bookkeeping equivalence between periodic edges and (base, class) pairs. -/
155def periodicEdgeProdEquiv : PeriodicEdge N N N ≃ Vertex N N N × Fin 7 where
156 toFun e := (e.base, e.disp)
157 invFun p := ⟨p.1, p.2⟩
158 left_inv _ := rfl
159 right_inv _ := rfl
160
161/-- The canonical edge-stencil Dirichlet energy of the periodic Freudenthal
162triangulation is exactly the seven-class stencil energy, for every `N`. -/
163theorem canonicalEdgeStencil_eq_freudenthalStencil (u : Vertex N N N → ℝ) :
164 canonicalEdgeStencilDirichletEnergy (canonicalPeriodicTriangulation N N N)
165 (canonicalPeriodicIncidenceConsistent N N N) (toPotential N u) =
166 freudenthalStencilEnergy N u := by
167 classical
168 have h1 : canonicalEdgeStencilDirichletEnergy
169 (canonicalPeriodicTriangulation N N N)
170 (canonicalPeriodicIncidenceConsistent N N N) (toPotential N u) =
171 ∑ edge : PeriodicEdge N N N,
172 stencilWeight edge.disp *
173 (u edge.endpoints.1 - u edge.endpoints.2) ^ (2 : ℕ) := by
174 unfold canonicalEdgeStencilDirichletEnergy
175 refine Fintype.sum_equiv (edgeFinEquiv N N N) _ _ fun e => ?_
176 rw [canonical_globalSqEdge_eq, canonical_edgeVerts_eq]
177 dsimp only
178 rw [toPotential_symm_apply, toPotential_symm_apply]
179 rfl
180 have h2 : (∑ edge : PeriodicEdge N N N,
181 stencilWeight edge.disp *
182 (u edge.endpoints.1 - u edge.endpoints.2) ^ (2 : ℕ)) =
183 ∑ p : Vertex N N N × Fin 7,
184 stencilWeight p.2 *
185 (u (shiftVertex N p.1 p.2) - u p.1) ^ (2 : ℕ) := by
186 refine Fintype.sum_equiv (periodicEdgeProdEquiv N) _ _ fun edge => ?_
187 rw [periodicEdge_endpoints_eq]
188 dsimp only [periodicEdgeProdEquiv, Equiv.coe_fn_mk]
189 ring
190 rw [h1, h2, Fintype.sum_prod_type]
191 rfl
192
193/-- General-N stage-1 core identity, DERIVED from the canonical Regge
194Hessian (never postulated): the frozen quadratic form
195`hessianQuadratic (canonicalReggeHessian …)` of the canonical periodic
196Freudenthal triangulation at any side `N > 2` equals the seven-class
197stencil energy `Σ_x Σ_d c_d (u(x+d) − u(x))²`.
198
199Derivation chain: `canonicalReggeHessian_quadratic_eq_dirichlet`
200(Hessian quadratic form = graph Dirichlet energy), the no-self-loop
201edge-stencil reindexing of `ReggeActionConcrete`
202(`canonicalDirichletEqualsEdgeStencil_of_sumComm_and_reindex`), and the
203periodic-edge product reindexing above. -/
204theorem hessianQuadratic_canonical_eq_freudenthalStencil
205 (hN : 2 < N) (u : Vertex N N N → ℝ) :
206 hessianQuadratic
207 (canonicalReggeHessian (canonicalPeriodicTriangulation N N N)
208 (canonicalPeriodicIncidenceConsistent N N N))
209 (toPotential N u) =
210 freudenthalStencilEnergy N u := by
211 rw [canonicalReggeHessian_quadratic_eq_dirichlet]
212 rw [canonicalDirichletEqualsEdgeStencil_of_sumComm_and_reindex
213 (canonicalPeriodicTriangulation N N N)
214 (canonicalPeriodicIncidenceConsistent N N N)
215 (canonicalEdgeStencilSumComm _ _)
216 (canonicalEdgePairWeightReindex_of_noSelfLoop _ _
217 (canonicalPeriodic_noSelfLoopEdges N hN))
218 (toPotential N u)]
219 exact canonicalEdgeStencil_eq_freudenthalStencil N u
220
221/-! ## §3. The a-priori normalization and the panel-locked identity -/
222
223/-- A-PRIORI normalization `ρ(N) = 1/N`, declared before any limit
224computation. Dimensional derivation (not a fit): each Hessian summand
225carries exactly one hinge-measure length factor `√(ℓ²_d)` at lattice
226spacing `h = 1/N`, so the physical energy density
227`h³ · Σ c_d ((Δu)/h)² = h · Σ c_d (Δu)²` differs from the raw quadratic
228form by exactly one power of `h = 1/N`. -/
229def stencilNormalization (N : ℕ) : ℝ := 1 / (N : ℝ)
230
231/-- Lattice spacing `h = 1/N` of the side-`N` canonical periodic family on
232the unit 3-torus. -/
233def meshSize (N : ℕ) : ℝ := 1 / (N : ℝ)
234
235/-- Panel-locked stage-1 observable, for ALL `N > 2` and arbitrary vertex
236data `u`:
237
238`ρ(N) · Q_N(u) = h³ · Σ_x Σ_{d ∈ D} c_d · ((u(x+d) − u(x))/h)²`, `h = 1/N`,
239
240where `Q_N` is the canonical Regge-Hessian quadratic form
241(`hessianQuadratic (canonicalReggeHessian …)`), `D` is the full
242seven-element displacement-class set, the weights `c_d` are the
243definitional Hessian dual weights (`stencilWeight`), and
244`ρ(N) = stencilNormalization N = 1/N` was declared a priori above. -/
245theorem freudenthal_stencil_identity (hN : 2 < N) (u : Vertex N N N → ℝ) :
246 stencilNormalization N *
247 hessianQuadratic
248 (canonicalReggeHessian (canonicalPeriodicTriangulation N N N)
249 (canonicalPeriodicIncidenceConsistent N N N))
250 (toPotential N u) =
251 meshSize N ^ (3 : ℕ) *
252 ∑ x : Vertex N N N, ∑ d : Fin 7,
253 stencilWeight d *
254 ((u (shiftVertex N x d) - u x) / meshSize N) ^ (2 : ℕ) := by
255 rw [hessianQuadratic_canonical_eq_freudenthalStencil N hN u]
256 unfold freudenthalStencilEnergy stencilNormalization meshSize
257 have hN0 : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
258 simp_rw [Finset.mul_sum]
259 refine Finset.sum_congr rfl fun x _ => Finset.sum_congr rfl fun d _ => ?_
260 field_simp
261
262/-- The `ρ(N)`-normalized canonical quadratic energy of the side-`N`
263periodic Freudenthal family. Stage 2 samples continuum fields into this. -/
264def scaledCanonicalEnergy (u : Vertex N N N → ℝ) : ℝ :=
265 stencilNormalization N *
266 hessianQuadratic
267 (canonicalReggeHessian (canonicalPeriodicTriangulation N N N)
268 (canonicalPeriodicIncidenceConsistent N N N))
269 (toPotential N u)
270
271theorem scaledCanonicalEnergy_eq_scaled_stencil (hN : 2 < N)
272 (u : Vertex N N N → ℝ) :
273 scaledCanonicalEnergy N u =
274 stencilNormalization N * freudenthalStencilEnergy N u := by
275 unfold scaledCanonicalEnergy
276 rw [hessianQuadratic_canonical_eq_freudenthalStencil N hN u]
277
278/-! ## §4. The moment tensor `A₀ = Σ_d c_d · d dᵀ` -/
279
280/-- Real coordinates of the seven displacement classes (0/1 entries),
281as an explicit table. `dispReal_matches_dispBits` kernel-checks the table
282against the canonical `dispBits` displacement bits. -/
283def dispReal : Fin 7 → Fin 3 → ℝ
284 | 0, 0 => 1 | 0, 1 => 0 | 0, 2 => 0
285 | 1, 0 => 0 | 1, 1 => 1 | 1, 2 => 0
286 | 2, 0 => 0 | 2, 1 => 0 | 2, 2 => 1
287 | 3, 0 => 1 | 3, 1 => 1 | 3, 2 => 0
288 | 4, 0 => 1 | 4, 1 => 0 | 4, 2 => 1
289 | 5, 0 => 0 | 5, 1 => 1 | 5, 2 => 1
290 | 6, 0 => 1 | 6, 1 => 1 | 6, 2 => 1
291
292/-- The `dispReal` table is exactly the indicator coordinates of the
293canonical displacement bit table `dispBits` (no free data). -/
294theorem dispReal_matches_dispBits (d : Fin 7) :
295 dispReal d 0 = (if (dispBits d).1 then 1 else 0) ∧
296 dispReal d 1 = (if (dispBits d).2.1 then 1 else 0) ∧
297 dispReal d 2 = (if (dispBits d).2.2 then 1 else 0) := by
298 fin_cases d <;>
299 refine ⟨?_, ?_, ?_⟩ <;> norm_num [dispReal, dispBits]
300
301/-- The stencil moment tensor `A₀ = Σ_{d ∈ D} c_d · d dᵀ` of the canonical
302Freudenthal displacement classes with their Hessian dual weights. -/
303def stencilMomentTensor : Fin 3 → Fin 3 → ℝ := fun i j =>
304 ∑ d : Fin 7, stencilWeight d * dispReal d i * dispReal d j
305
306/-- EXACT value of the moment tensor:
307`A₀ = (1 + √2)·I + (√2 + √3)·J` with `J` the all-ones matrix. Every
308diagonal entry is `1 + 2√2 + √3`; every off-diagonal entry is `√2 + √3`.
309The entries are irrational (in `ℚ[√2,√3]`); this is the exact
310kernel-checked value. -/
311theorem stencilMomentTensor_eq (i j : Fin 3) :
312 stencilMomentTensor i j =
313 (if i = j then 1 + Real.sqrt 2 else 0) + (Real.sqrt 2 + Real.sqrt 3) := by
314 fin_cases i <;> fin_cases j <;>
315 · norm_num [stencilMomentTensor, Fin.sum_univ_seven, dispReal,
316 stencilWeight, periodicDispSqEdge, Real.sqrt_one]
317 try ring
318
319theorem stencilMomentTensor_symm (i j : Fin 3) :
320 stencilMomentTensor i j = stencilMomentTensor j i := by
321 unfold stencilMomentTensor
322 refine Finset.sum_congr rfl fun d _ => ?_
323 ring
324
325/-- Exact sum-of-squares decomposition of the moment-tensor quadratic form:
326`vᵀ A₀ v = Σ_d c_d ⟨d, v⟩²`. This is the kernel-level PSD witness. -/
327theorem stencilMomentTensor_quadratic_eq (v : Fin 3 → ℝ) :
328 (∑ i : Fin 3, ∑ j : Fin 3, stencilMomentTensor i j * v i * v j) =
329 ∑ d : Fin 7,
330 stencilWeight d * (∑ i : Fin 3, dispReal d i * v i) ^ (2 : ℕ) := by
331 simp only [stencilMomentTensor, Fin.sum_univ_three, Fin.sum_univ_seven,
332 dispReal]
333 ring
334
335/-- KERNEL-PROVED: the moment tensor `A₀` is positive semidefinite. -/
336theorem stencilMomentTensor_psd (v : Fin 3 → ℝ) :
337 0 ≤ ∑ i : Fin 3, ∑ j : Fin 3, stencilMomentTensor i j * v i * v j := by
338 rw [stencilMomentTensor_quadratic_eq]
339 refine Finset.sum_nonneg fun d _ => ?_
340 exact mul_nonneg (stencilWeight_nonneg d) (by positivity)
341
342theorem sqrt_two_add_sqrt_three_pos : 0 < Real.sqrt 2 + Real.sqrt 3 := by
343 have h3 : 0 < Real.sqrt 3 := Real.sqrt_pos.mpr (by norm_num)
344 have h2 : 0 ≤ Real.sqrt 2 := Real.sqrt_nonneg 2
345 linarith
346
347/-- KERNEL-PROVED: `A₀` is nonzero — every diagonal entry
348`1 + 2√2 + √3` is strictly positive. -/
349theorem stencilMomentTensor_diag_pos (i : Fin 3) :
350 0 < stencilMomentTensor i i := by
351 rw [stencilMomentTensor_eq]
352 rw [if_pos rfl]
353 have h2 : 0 ≤ Real.sqrt 2 := Real.sqrt_nonneg 2
354 have h3 : 0 ≤ Real.sqrt 3 := Real.sqrt_nonneg 3
355 linarith
356
357theorem stencilMomentTensor_ne_zero : stencilMomentTensor 0 0 ≠ 0 :=
358 ne_of_gt (stencilMomentTensor_diag_pos 0)
359
360/-- Off-diagonal entries of `A₀` are strictly positive (`√2 + √3`). -/
361theorem stencilMomentTensor_offDiag_pos (i j : Fin 3) (hij : i ≠ j) :
362 0 < stencilMomentTensor i j := by
363 rw [stencilMomentTensor_eq, if_neg hij]
364 simpa using sqrt_two_add_sqrt_three_pos
365
366/-- FINDING (kernel-checked): the moment tensor is ANISOTROPIC. The
367off-diagonal entry is `√2 + √3 > 0`, so `A₀ ≠ c·I` for every scalar `c`.
368Isotropy is NOT claimed; the exact anisotropic value is
369`stencilMomentTensor_eq`. -/
370theorem stencilMomentTensor_not_isotropic (c : ℝ) :
371 stencilMomentTensor ≠ fun i j => if i = j then c else 0 := by
372 intro h
373 have hne : (0 : Fin 3) ≠ 1 := by decide
374 have h01 := congrFun (congrFun h 0) 1
375 rw [if_neg hne] at h01
376 exact absurd h01 (ne_of_gt (stencilMomentTensor_offDiag_pos 0 1 hne))
377
378/-! ## §5. Status record (documentation, not mathematics) -/
379
380/-- Status flags for the Freudenthal stencil preflight (documentation
381record; the mathematics lives in the theorems above, not in these
382booleans).
383
384Honest scope: this stage-1 record certifies the general-N stencil identity
385derived from the canonical Regge Hessian, the a-priori normalization
386`ρ(N) = 1/N`, and the exact anisotropic PSD moment tensor
387`A₀ = (1+√2)·I + (√2+√3)·J`. Together with stage 2 this remains a SCOPED
388PARTIAL of the action-level continuum limit of the frozen quadratic energy
389on the canonical Freudenthal family; the pillar-2 path-sum flag stays red
390(flipping it requires the refinement-indexed measure-weighted sum over
391inequivalent triangulation classes). -/
392structure StencilPreflightStatus where
393 /-- `freudenthal_stencil_identity`: general-N identity, all seven
394 displacement classes, derived from `canonicalReggeHessian`. -/
395 general_N_identity_derived : Bool
396 /-- `stencilNormalization` declared a priori with dimensional
397 justification; no post-hoc fitting. -/
398 normalization_a_priori : Bool
399 /-- `stencilMomentTensor_psd` + `stencilMomentTensor_diag_pos`. -/
400 moment_tensor_psd_nonzero : Bool
401 /-- `stencilMomentTensor_not_isotropic`: anisotropy is the finding;
402 isotropy is NOT claimed. -/
403 moment_tensor_anisotropic_finding : Bool
404
405/-- The canonical status inhabitant (documentation record, not a proof
406obligation). -/
407def stencilPreflightStatus : StencilPreflightStatus where
408 general_N_identity_derived := true
409 normalization_a_priori := true
410 moment_tensor_psd_nonzero := true
411 moment_tensor_anisotropic_finding := true
412
413end
414
415end FreudenthalStencilPreflight
416end Analysis
417end Gravity
418end IndisputableMonolith
419