canonicalPeriodicFlatConfigurationInputs
plain-language theorem explainer
Packages the two geometric inputs needed for a canonical periodic flat configuration on the encoded Freudenthal torus: a local analytic chart from the explicit Freudenthal tetrahedron, and global zero deficit from the certified periodic angle-sum chain. Gravity and Regge-calculus workers cite it when instantiating the physical six-tet cubic Dirichlet model. The body is a thin constructor call that wires the realized tet and the global zero-deficit certificate.
Claim. For lattice sizes $N_x,N_y,N_z\ge 3$, the structure of remaining flat-configuration data on the canonical encoded periodic Freudenthal torus is inhabited: it supplies a local analytic flat chart built from the realized Freudenthal tetrahedron together with a global zero-deficit certificate at the flat potential coming from the periodic angle-sum chain.
background
This module links the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not claim the physical Dirichlet equality outright; it packages the exact obligations needed to instantiate that model on a periodic Freudenthal torus.
The structure being filled records the two remaining geometric inputs for a canonical periodic flat configuration: a local analytic flat chart on the encoded torus complex $K$, and global zero deficit at the flat potential. Smoothness is omitted because it is already recovered from the local chart by the standard Regge continuity construction.
Deficit at a hinge is the classical $2\pi-\sum\theta$ (dihedral or Schläfli form). The upstream packaging lemma reduces the local-chart side to a single realized nondegenerate Freudenthal tetrahedron plus a global zero-deficit hypothesis on every encoded periodic edge.
proof idea
One-line constructor application. Call the packaging definition that builds the inputs from a realized Freudenthal tet and a global zero-deficit certificate. Pass the realized Freudenthal tetrahedron (via the squared-edge-of-points realization lemma), reflexivity for the tet-identity side condition, and the already-proved canonical periodic global zero-deficit-at-flat theorem for the angle-sum side.
why it matters
Closes both geometric sides of the flat-configuration interface on the canonical periodic Freudenthal torus, so downstream code can build a full flat configuration with no remaining local-chart or zero-deficit holes. The immediate consumer is the canonical periodic flat configuration itself; a further theorem then records that every encoded tetrahedron at that flat point carries the one-cube Freudenthal squared-edge tuple.
In the Recognition gravity stack this is scaffolding for the physical six-tet cubic Dirichlet instance: the Regge action on the periodic Freudenthal triangulation must sit at a true flat background before finite-difference Dirichlet comparisons make sense. It does not itself prove the Dirichlet equality; it discharges the geometric prerequisites the model demands.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.