canonicalPeriodicReggeAction_zeroPotential_eq_zero_of_flatConfigurationInputs
plain-language theorem explainer
On the canonical encoded periodic Freudenthal torus with sizes greater than 2, the Regge action at the zero potential is exactly zero once a local analytic flat chart and global zero deficit are supplied. Lattice-gravity and Regge-calculus workers cite this as the flat-action normalization step before quadratic Hessian analysis. The proof is a one-line wrapper that unpacks the two-input bundle into a flat configuration and reuses the existing zero-potential vanishing theorem.
Claim. Let $N_x,N_y,N_z\in\mathbb{N}$ with each $N_i>2$. Suppose one is given a local analytic flat chart on the canonical encoded periodic Freudenthal torus of those sizes, together with global zero deficit at the flat potential. Then the Regge action of that torus, evaluated at the zero potential, equals $0$.
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 freely assert the physical Dirichlet equality; it ties the encoded periodic scaffold to the model target through concrete theorem-shaped data.
The Regge action here is the discrete curvature functional on edge lengths of the torus complex. The zero potential is the flat edge-length assignment. The structure CanonicalPeriodicFlatConfigurationInputs supplies the remaining data for a flat configuration: a local analytic flat chart on the canonical encoded torus, and a global zero-deficit certificate at that flat potential. Smoothness is already obtained from the local chart, so it is not re-bundled.
Upstream, the shifted cost $H(x)=J(x)+1=\frac12(x+x^{-1})$ rewrites the Recognition Composition Law as the d'Alembert identity; the dimensionless bridge ratio $K=\varphi^{1/2}$ appears in related curvature bookkeeping. The present statement is purely geometric: flat inputs force vanishing of the discrete action.
proof idea
One-line term wrapper. Convert the two-input bundle I to a flat configuration via I.toFlatConfiguration, then apply the sibling theorem that already proves zero-potential Regge action vanishes on any such flat configuration of the canonical encoded periodic Freudenthal torus. No new algebraic work occurs at this layer.
why it matters
Flat-action normalization is the baseline for the module's second-order analysis: once the flat action is zero, the spacing-scaled second-order Regge action on $a\cdot\xi$, divided by $|a|^2$, equals the quadratic form $\frac12 H(\xi,\xi)$ for every nonzero spacing $a$. That exact quadratic normalization sits immediately downstream in the file narrative and feeds the physical finite-difference Dirichlet target on the six-tet cubic lattice.
In the Recognition gravity stack this closes a scaffold obligation rather than a forcing-chain landmark (T5–T8). It ensures the encoded periodic Freudenthal geometry is a legitimate flat background before Dirichlet/Hessian comparisons. No used_by edges are recorded yet, so the declaration is presently a leaf packaging step inside the physical-instance module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.