flatConfiguration_of_localChart_zeroDeficit
plain-language theorem explainer
Packages a flat analytic configuration for the nonlinear Regge action from three inputs: a local Euclidean chart on every tetrahedron, global vanishing of deficit angles at the zero potential, and C^∞ smoothness of the action there. Gravity and discrete-geometry workers cite it when assembling analytic hypotheses before Taylor expansion about flat space. The body is a pure structure constructor that reassigns those three fields.
Claim. Given an incidence-consistent 3D triangulation $K$, a local analytic flat chart (Euclidean nondegenerate realizations of every tetrahedron), the condition that every edge deficit angle vanishes at the zero potential, and $C^\infty$ smoothness of the Regge action at that potential, obtain a flat analytic configuration for $K$: arccos endpoints stay off $\pm 1$, deficits vanish globally, and the action is smooth at flat.
background
The module records analytic requirements for the full nonlinear Regge action as a named configuration rather than axioms. The closed second-order component theorem uses an exact quadratic truncation; the nonlinear action needs the conformal edge chart inside the nondegenerate tetrahedral cone, arccos arguments away from $\pm 1$, and smoothness of the finite Regge action at the flat potential.
A local analytic flat chart supplies Euclidean realizations of every tetrahedron and yields strict arccos endpoint avoidance: squared dihedral cosines never hit $\pm 1$. Global zero-deficit at flat is a separate assembled-triangulation condition: every edge deficit angle vanishes at the zero potential; it does not follow from local nondegeneracy alone. Smoothness closure asserts that the Regge action is $C^\infty$ at the zero potential once the local chart is given.
A flat configuration packages exactly those three fields so Taylor theory can be invoked on the nonlinear action.
proof idea
Pure structure constructor, not a proof. The local arccos-endpoint field is taken from the local chart's derived endpoint-free theorem. The flat-deficit field is the supplied global zero-deficit hypothesis. The action smoothness field is the contDiff-at-zero component of the smoothness-from-local-chart package. No algebraic work; field reassignment only.
why it matters
Gives the standard assembly point for analytic hypotheses on the nonlinear Regge action before any Taylor or second-variation argument about flat space. Downstream, the physical six-tet cubic Dirichlet instance uses it via CanonicalPeriodicFlatConfigurationInputs: that structure holds the remaining data (local chart and global zero-deficit) needed to build the canonical periodic flat configuration on the encoded Freudenthal torus, with smoothness already obtained from the local chart.
In the Recognition geometry stack this sits under discrete gravity / Regge calculus supporting continuum limits and curvature functionals, not under the T0–T8 forcing chain itself. It closes the packaging step so later gravity modules can treat flat analytic configurations as a single object rather than three loose hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.