CanonicalPeriodicFlatConfigurationInputs
plain-language theorem explainer
Packages the two geometric inputs needed for a canonical periodic flat configuration on an encoded Freudenthal torus of size Nx×Ny×Nz (each >2): a local analytic flat chart and global zero deficit at the flat potential. Gravity and Regge-calculus workers cite it when wiring the periodic six-tet cubic model to Dirichlet energy. It is a pure data bundle; smoothness is left to an existing chart-to-ContDiff constructor.
Claim. For lattice sizes $N_x,N_y,N_z\ge 3$, a canonical periodic flat-configuration input bundle consists of (i) a local analytic flat chart on the curvature functional $K$ of the canonical encoded periodic Freudenthal torus, and (ii) a global zero-deficit certificate for that same $K$ at the flat potential. Smoothness of the Regge action is not part of the bundle.
background
This module bridges the encoded periodic Freudenthal torus to the physical six-tet cubic Dirichlet model. It does not claim the Dirichlet equality outright; it packages the exact obligations needed to instantiate that model on a periodic Freudenthal triangulation of a 3-torus with periods $N_x,N_y,N_z$ (each at least 3).
The curvature functional $K$ attached to the canonical encoded periodic Freudenthal torus is the ambient object. A local analytic flat chart supplies analytic coordinates in which the configuration is flat near the reference potential. Global zero deficit at flat means the angle-sum (deficit) around every encoded periodic edge vanishes when the edge lengths sit at the flat point.
Smoothness of the Regge action is deliberately omitted: once a local chart is given, reggeActionContDiffFromLocalChart_of_localChart already builds the required ContDiff data. The dimensionless bridge ratio $K=\varphi^{1/2}$ appears in the broader constants layer but is not the structure field here; the field $K$ is the torus curvature functional.
proof idea
No proof body: this is a structure definition. It declares two fields (local analytic flat chart; global zero deficit at flat) parameterized by the lattice sizes and the strict inequalities $N_x,N_y,N_z>2$. Inhabitants are built downstream by packaging a realized nondegenerate Freudenthal tetrahedron chart with a certified periodic angle-sum zero-deficit hypothesis.
why it matters
This bundle is the exact remaining data for a canonical periodic FlatConfiguration on the encoded Freudenthal torus. Downstream, canonicalPeriodicFlatConfigurationInputs_of_realizedFreudenthalTet_zeroDeficit and the fully discharged canonicalPeriodicFlatConfigurationInputs inhabit it once the local chart reduces to one realized Freudenthal tetrahedron and the periodic angle-sum chain certifies zero deficit.
Parent theorems then use any such inhabitant to obtain: flat-action normalization (Regge action at zero potential equals zero), second-order finite aggregates tending to Dirichlet energy, and the full nonlinear Regge finite aggregate in Dirichlet-energy form. In the Recognition gravity stack this is the packaging step that lets the six-tet cubic periodic scaffold feed the physical Dirichlet target without smuggling smoothness or flatness hypotheses into each limit theorem.
It sits in the discrete-to-continuum gravity bridge (Regge on Freudenthal cubes toward continuum Dirichlet energy in $D=3$), not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.