LocalAnalyticFlatChart
plain-language theorem explainer
Packages, for every tetrahedron of a 3D triangulation, a Euclidean nondegenerate realization matching that tet. This is the local analytic chart data that keeps dihedral cosines strictly inside (-1,1), so arccos stays smooth. Smoothness and flat-configuration constructors for the nonlinear Regge action cite it; gravity instances build it from a single Freudenthal tet. Pure structure definition, not a proved existence claim.
Claim. A local analytic flat chart on a 3D triangulation $K$ is data assigning to each tetrahedron $\tau$ of $K$ a realized nondegenerate tetrahedron whose underlying combinatorial tetrahedron equals $K$'s tetrahedron $\tau$.
background
The module records analytic inputs needed for the full nonlinear Regge action (as opposed to the exact quadratic truncation used by the closed second-order component theorem). Three requirements appear: the conformal edge chart must stay in the nondegenerate tetrahedral cone; arccos arguments must avoid $\pm 1$; and the finite Regge action must be smooth at the flat potential.
A realized nondegenerate tetrahedron supplies a Euclidean embedding with strict interior dihedral data: squared dihedral cosines lie in $(-1,1)$. The triangulation type Triangulation3D carries a finite family of combinatorial tets with squared edge lengths. The chart simply equips every tet of $K$ with such a realization and records that the combinatorial tet is recovered exactly.
This is configuration data, not an axiom: lower-level polynomial and strict-interior facts from the geometry stack (affine-independence interior, cofactor derivatives, concrete Regge action) are meant to discharge the fields in concrete instances.
proof idea
Structure definition, not a proof. Two fields: realizedTet assigns to each tet index a RealizedNonDegenerateTet, and realizes_tet asserts that realization's combinatorial tet equals $K$'s tet at that index.
The companion lemma local_arccos_endpoint_free is a short transport: for each tet and each of the six faces, pull the strict-interior bound -1 < dihedralCos3Sq < 1 from the realization, rewrite along realizes_tet, and apply DihedralDerivatives.arccos_endpoint_hypotheses_of_interior to obtain the endpoint-free hypotheses ≠ -1 and ≠ 1 needed by the arccos chain.
why it matters
Named local ingredient behind strict arccos endpoint avoidance for the nonlinear Regge action. Downstream, reggeAction_contDiffAt_zero_of_localChart feeds the chart's endpoint-free lemma into ContDiffAt of the Regge action at the zero potential; reggeActionContDiffFromLocalChart_of_localChart packages that into the smoothness-closure structure; and flatConfiguration_of_localChart_zeroDeficit builds a full FlatConfiguration from the chart plus global zero-deficit plus that smoothness package.
In the gravity stack, CanonicalPeriodicFlatConfigurationInputs requires exactly such a chart on the encoded periodic Freudenthal torus, and canonicalPeriodicLocalAnalyticFlatChart_of_realizedFreudenthalTet constructs it from one realized nondegenerate Freudenthal tet (all encoded periodic tets are copies of that local model).
Closes the analytic-input gap the module doc flags: requirements are recorded as named configuration rather than hidden axioms. Does not itself touch T0–T8 or the RCL; it is geometry infrastructure for the discrete gravity / Regge side of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.