CanonicalPeriodicLocalConformalSchlaefliAlongLineTargetAtN5
plain-language theorem explainer
Fixes the canonical periodic local conformal Schläfli-along-line target to the concrete 5×5×5 lattice. Gravity handoff proofs cite this sized instance when discharging the local tetrahedral Schläfli obligation on the encoded Freudenthal torus. The body is a pure abbreviation that plugs N=5 with decidable size witnesses.
Claim. The proposition that the local conformal Schläfli-along-line target holds on the canonical encoded periodic Freudenthal torus of size $5\times 5\times 5$ (with the standing hypotheses $2<5$ on each axis).
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus; it does not assert the physical Dirichlet equality for free.
The upstream target is the size-parametric proposition "canonical periodic local non-flat Schläfli target along conformal lines": it applies the local conformal Schläfli-along-line predicate to the curvature data $K$ of the canonical encoded periodic Freudenthal torus of dimensions $(N_x,N_y,N_z)$ with each $N>2$. That local target encodes the non-flat tetrahedral Schläfli identity along conformal line deformations at every lattice parameter.
The present declaration freezes those dimensions at the working lattice size used throughout the gravity track: $N_x=N_y=N_z=5$.
proof idea
One-line abbreviation. It applies the parametric target at $(5,5,5)$ and discharges the three $2<N$ side conditions by decide. No further proof content.
why it matters
This fixed-size local target is one of the two concrete non-flat inputs to the Track 1 conformal Schläfli local-expansion endpoint: that endpoint states that the global expansion/reindexing target together with this local target yield the full canonical conformal Schläfli-along-line target at $N=5$. The sibling theorem ..._of_expansion_and_local is the corresponding discharge rule, feeding the MasterTheorem handoff consumed by Track 7.
In the broader Recognition gravity stack, the local Schläfli identity on the six-tet cubic decomposition is the discrete curvature step that must match the continuum Dirichlet (Hessian) action on the Freudenthal lattice before continuum limits and physical constants are read off.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.