Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D

show as:
view Lean formalization →

Defines the 4D Regge edge stencil: class masks on the 15 nonzero bit-patterns, displacement vectors, squared weights, and midpoint plane-wave coefficients for edge loadings on the 4-torus. Gravity analysts cite it as the shared phase convention for Bloch folds and TT edge attachment. The module is mostly definitional arithmetic plus elementary positivity and additivity lemmas.

claimOn the 4-torus edge lattice, each nonzero class $d\in\{0,\ldots,14\}$ has bit-mask $m(d)=d+1\in\{1,\ldots,15\}$, displacement $D(d)\in\{\pm1\}^4$, weight $w(d)=\|D(d)\|_2^2\in\mathbb{N}_{>0}$, and midpoint plane-wave coefficient $c_d(k)=w(d)\,e^{i\,k\cdot x_{\mathrm{mid}}(d)}$ used to load axis-edge perturbations.

background

This sits in the QG full-theory 4D Regge campaign, immediately after the algebraic edge TT attachment layer. That upstream module attaches the Euclidean $4\times4$ TT / gauge / transverse-trace split to plane-wave edge loadings on axis edges of the 4-torus, with quadratic form $\sum_{ij} E_{ij} D^i D^j$ matching the 3D chain.

The stencil module freezes the discrete geometry of those loadings: each of the 15 nonzero nibble classes carries a bit-mask, a signed displacement in ${\pm1}^4$, its squared Euclidean weight, and a midpoint phase factor. Class coefficients assemble into plane-wave class perturbations that decorate edges before any Bloch fold or continuum symbol is formed.

Notation is deliberately parallel to the 3D preflight: weights are positive naturals, displacements are never zero, and coefficient addition is componentwise so multi-class superpositions stay inside the same algebra.

proof idea

Definition module with light lemma support, not a deep proof development. Masks, bits, displacements, squared displacements, and natural weights are introduced by direct formulas from the class index. Positivity of weights and non-vanishing of displacements are immediate case or arithmetic checks. The identity that squared displacement equals the weight is definitional unfolding. Midpoint phases and plane-wave class perturbations are pure constructors; coefficient additivity is a one-line fieldwise rewrite.

why it matters in Recognition Science

Supplies the committed midpoint plane-wave convention that every later 4D edge analysis imports. Downstream, EdgeTTDecompositionCloser4D composes algebraic TT decomposition with this plane-wave edge attachment to inhabit the edge_tt_decomposition preflight. ReggeBlochFold4D folds the true-weight flat Hessian on type-$(1,1)$ hinges using exactly these midpoint phases. Continuum preflight, exact action symbol, flat second-variation, and transported algebraic closer modules all depend on the same stencil so TT plus/cross witnesses, gauge decoys, and $H_{\mathrm{fold}}$ symbols stay on one edge-loading convention. Without this shared carrier, the 4D Freudenthal-torus campaign would fork incompatible phase conventions before any EH-limit claim.

scope and limits

used by (18)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (57)