Pith. sign in
def

stencilPreflightStatus

definition
show as:
module
IndisputableMonolith.Gravity.Analysis.FreudenthalStencilPreflight
domain
Gravity
line
407 · github
papers citing
none yet

plain-language theorem explainer

Canonical documentation record for Freudenthal stencil preflight stage 1: all four status flags true. It asserts that the general-N seven-class stencil identity is derived from the canonical Regge Hessian, that the normalization ρ(N)=1/N is a priori, and that the moment tensor is anisotropic, PSD, and nonzero. Gravity continuum-limit authors cite it as a panel status snapshot, not as a proof. Construction is a pure structure inhabitant with four boolean fields.

Claim. The canonical stage-1 status record for the Freudenthal stencil preflight sets four flags to true: the general-$N$ stencil identity is derived from the canonical Regge Hessian; the normalization $\rho(N)=1/N$ is declared a priori (no post-hoc fit); the moment tensor $A_0$ is positive semidefinite and nonzero; and $A_0$ is anisotropic (not a multiple of the identity).

background

This module is Phase 2b of the QG full-theory campaign (panel-locked Test G, stage 1, candidate C8): action-level continuum limit of the frozen quadratic energy on the canonical periodic Freudenthal triangulation. Scope is partial; the pillar-2 path-sum flag stays red until a refinement-indexed measure-weighted sum over triangulation classes exists.

Stage 1 proves, for every side length $N>2$, that the quadratic form of the canonical Regge Hessian equals the seven-class nearest-displacement stencil $\sum_x \sum_{d:\mathrm{Fin},7} c_d,(u(x+d)-u(x))^2$ with weights $c_d=\sqrt{\ell_d^2}$ for classes $\ell^2\in{1,1,1,2,2,2,3}$. The normalized identity is $\rho(N),Q_N(u)=h^3\sum_x\sum_d c_d\bigl((u(x+d)-u(x))/h\bigr)^2$ with $h=1/N$ and $\rho(N)=1/N$ fixed a priori. The moment tensor is $A_0=\sum_d c_d,dd^T=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$.

StencilPreflightStatus is only a documentation structure of four booleans. The mathematics lives in the theorems above it; these flags do not discharge proof obligations.

proof idea

No proof. The definition is a structure inhabitant of StencilPreflightStatus with all four boolean fields set to true: general-$N$ identity derived, normalization a priori, moment tensor PSD and nonzero, and anisotropy recorded as the finding. It is a status snapshot, not a theorem wrapper.

why it matters

Panel-facing status seal for Test G stage 1 on the Freudenthal family. It packages the three stage-1 claims the continuum-limit campaign needs before stage 2 (FreudenthalEnergyLimit): derived general-$N$ stencil identity from the canonical Regge Hessian, a-priori $\rho(N)=1/N$, and exact anisotropic PSD moment tensor $A_0=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$. Downstream use count is zero; the value is audit and campaign bookkeeping, not a lemma dependency.

Together with stage 2 the package remains scoped: the path-sum pillar stays red. The anisotropy finding is intentional (tensor-first anisotropic action continuum limit), not a defect to be removed. No Recognition forcing-chain landmark (T0–T8) is closed here; this is gravity analysis infrastructure on the Regge/Freudenthal side.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.