module module high

`IndisputableMonolith.Gravity.Analysis.FreudenthalStencilPreflight`

Preflight layer for the Freudenthal stencil energy in the Regge continuum-limit campaign. It defines displacement-class stencil weights as square roots of squared edge lengths and packages the frozen quadratic energy on the canonical periodic Freudenthal triangulation. Continuum-limit and TT-symbol modules import this interface. Content is largely definitional: canonical dual weights are identified with periodic displacement classes.

claimOn the canonical periodic Freudenthal triangulation, the stencil weight of a displacement class $d$ is $w(d)=\sqrt{\ell^2(d)}$, where $\ell^2(d)$ is the squared edge length of that class. The freudenthal stencil energy is the frozen quadratic form built by pairing these weights with a vertex potential, matching the canonical Hessian dual-weight sum over incident edges.

background

Recognition Science gravity analysis here works on the periodic Freudenthal torus model: a typed periodic vertex/edge/tetrahedron shape for an arbitrary Freudenthal tiling. Upstream, that model supplies the global incidence and edge-slot partition needed by the nonlinear Regge first-variation theorem, without yet fixing a concrete finite $n\times m\times k$ mesh.

The companion concrete Regge Hessian target isolates the analytic second variation of the Regge action under a conformal ansatz and exposes it as ReggeHessianData. On the canonical periodic triangulation, squared edge lengths are those of displacement classes (periodicDispSqEdge). The dual weight at a vertex is the sum of square roots of those lengths over incident edges.

This module freezes that structure into stencil language: a weight per displacement class, a shift of vertices along the lattice, and a quadratic energy functional of a potential on vertices. Symmetry and nonnegativity of the weight, endpoint identities for periodic edges, and the absence of self-loop edges in the canonical model are recorded as supporting facts.

proof idea

Definition-and-identity module, not a deep existence proof. Stencil weight is introduced as the square root of the global squared edge length of a displacement class, then equated to the canonical Hessian dual-weight building block. Short lemmas record the numerical values, nonnegativity, and the match between canonical global squared edges and periodic displacement squares. Vertex shift and periodic-edge endpoint identities are pure bookkeeping on the torus model. The freudenthal stencil energy and the map from potentials assemble those weights into the frozen quadratic form used downstream; several equalities are definitional rewrites rather than analytic arguments.

why it matters in Recognition Science

Stage-1 companion in the QG full-theory campaign for the action-level continuum limit of the frozen quadratic energy on the canonical Freudenthal family (panel-locked Test G stage 2, candidate C8). Downstream, FreudenthalEnergyLimit imports this preflight to rate the continuum limit on a sampled witness field. ReggeTTSymbolPreflight also imports it as Stage 1 of the Regge TT continuum-symbol program: true nonlinear action, flat point, frozen-model identification, and the TT Bloch symbol object.

Without a clean stencil weight and energy interface tied to the canonical Hessian, those continuum and symbol arguments would re-derive displacement-class geometry ad hoc. This module closes that scaffolding gap between the periodic Freudenthal geometry and the gravity-analysis limit theorems.

scope and limits

Does not prove the continuum limit of the stencil energy; that is deferred to FreudenthalEnergyLimit.
Does not construct a concrete finite n×m×k mesh; only the typed periodic Freudenthal model.
Does not derive the nonlinear Regge first variation; it freezes the quadratic Hessian data.
Does not establish the TT Bloch symbol or its continuum identification.
Does not claim dynamical Einstein equations; only preflight identities for the frozen quadratic form.

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.Analysis.FreudenthalEnergyLimit module_import
IndisputableMonolith.Gravity.Analysis.ReggeTTSymbolPreflight module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.PeriodicFreudenthalTorus module_import
IndisputableMonolith.Geometry.ReggeActionConcrete module_import

declarations in this module (34)

def stencilWeight L83
theorem stencilWeight_eq_sqrt_globalSqEdge L88
theorem stencilWeight_values L96
theorem stencilWeight_nonneg L103
def shiftVertex L109
theorem periodicEdge_endpoints_eq L112
def freudenthalStencilEnergy L118
def toPotential L123
theorem toPotential_symm_apply L127
theorem canonical_globalSqEdge_eq L134
theorem canonical_edgeVerts_eq L139
theorem canonicalPeriodic_noSelfLoopEdges L147
def periodicEdgeProdEquiv L155
theorem canonicalEdgeStencil_eq_freudenthalStencil L163
theorem hessianQuadratic_canonical_eq_freudenthalStencil L204
def stencilNormalization L229
def meshSize L233
theorem freudenthal_stencil_identity L245
def scaledCanonicalEnergy L264
theorem scaledCanonicalEnergy_eq_scaled_stencil L271
def dispReal L283
theorem dispReal_matches_dispBits L294
def stencilMomentTensor L303
theorem stencilMomentTensor_eq L311
theorem stencilMomentTensor_symm L319
theorem stencilMomentTensor_quadratic_eq L327
theorem stencilMomentTensor_psd L336
theorem sqrt_two_add_sqrt_three_pos L342
theorem stencilMomentTensor_diag_pos L349
theorem stencilMomentTensor_ne_zero L357
theorem stencilMomentTensor_offDiag_pos L361
theorem stencilMomentTensor_not_isotropic L370
structure StencilPreflightStatus L392
def stencilPreflightStatus L407