StencilPreflightStatus
plain-language theorem explainer
Four boolean status flags packaging stage-1 Freudenthal stencil preflight claims: general-N identity derived from the canonical Regge Hessian, a-priori normalization ρ(N)=1/N, PSD nonzero moment tensor, and anisotropy as a finding (not isotropy). The canonical inhabitant sets all flags true. Pure documentation structure; mathematics lives in the theorems above, not in these booleans.
Claim. A documentation record of four boolean flags for the Freudenthal stencil preflight: (i) the general-$N$ seven-class stencil identity is derived from the canonical Regge Hessian; (ii) the normalization $\rho(N)=1/N$ is declared a priori with dimensional justification; (iii) the moment tensor is positive semidefinite and nonzero on the diagonal; (iv) the moment tensor is anisotropic (isotropy is not claimed).
background
This module is Phase 2b of the QG full-theory campaign: panel-locked Test G stage 1 on the action-level continuum limit of frozen quadratic energy on the canonical periodic Freudenthal family (side length $N>2$). Scope is a scoped partial; the pillar-2 path-sum flag stays red until a refinement-indexed measure-weighted sum over inequivalent triangulation classes exists.
The underlying mathematics (proved elsewhere in the module) identifies the quadratic form of canonicalReggeHessian with a seven-class nearest-displacement stencil $\sum_x \sum_{d:\mathrm{Fin},7} c_d,(u(x+d)-u(x))^2$, weights $c_d=\sqrt{\ell_d^2}$ with $\ell^2\in{1,1,1,2,2,2,3}$ for axis, face-diagonal, and body-diagonal classes. The normalized identity uses $h=1/N$ and $\rho(N)=1/N$ fixed before any limit. The moment tensor is $A_0=\sum_d c_d,dd^T=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$.
These four booleans do not restate those theorems; they are a human-readable status board for the preflight checklist.
proof idea
No proof: this is a structure definition with four Bool fields and field doc-comments naming the theorems each flag is meant to track (freudenthal_stencil_identity, a-priori stencilNormalization, stencilMomentTensor_psd plus diagonal positivity, and stencilMomentTensor_not_isotropic). The sole use site is the canonical inhabitant that hard-codes all four fields to true.
why it matters
Gives a single named type for the stage-1 preflight checklist so downstream code and docs can point at one record rather than four scattered theorems. The only consumer is stencilPreflightStatus, which inhabits every flag as true and is explicitly labeled a documentation record, not a proof obligation.
In the Recognition gravity program this sits under Test G (candidate C8, tensor-first anisotropic action continuum limit). It records that the general-$N$ stencil identity, a-priori $\rho(N)=1/N$, and the exact anisotropic PSD moment $A_0=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$ are in place, while remaining honest that stage 1 plus stage 2 (FreudenthalEnergyLimit) is still only a scoped partial of the continuum limit: pillar-2 path-sum stays red.
No forcing-chain landmark (T0–T8) is discharged here; the structure is bookkeeping for the Regge/Freudenthal gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.