FlatConfiguration
plain-language theorem explainer
Packages the three analytic hypotheses needed for Taylor theory of the nonlinear Regge action on a 3D triangulation: arccos arguments stay off ±1 at the flat base point, every edge deficit vanishes at the zero potential, and the full Regge action is C^∞ there. Downstream cubic-remainder bounds and cascade-closure certificates take this package as input. It is a named structure, not a proved theorem.
Claim. A flat analytic configuration on an incidence-consistent 3D triangulation $K$ is a triple of properties at the zero vertex potential: (i) for every tetrahedron and every of its six edge-pairs, the squared dihedral cosine is neither $-1$ nor $1$ (arccos endpoint-free); (ii) the deficit angle on every edge vanishes; (iii) the nonlinear Regge action is $C^\infty$ at that base point.
background
The module collects smoothness inputs for the full nonlinear Regge action. The closed second-order component theorem only needs an exact quadratic truncation; the nonlinear theory needs the conformal edge chart to stay in the nondegenerate tetrahedral cone, arccos arguments away from $\pm 1$, and the finite Regge action smooth at the flat potential.
A triangulation $K$ carries tetrahedra with squared edge lengths; dihedralCos3Sq is the squared cosine of a dihedral angle built from those lengths. The deficit angle on an edge is $2\pi$ minus the sum of incident dihedral angles. The zero potential is the flat base point in the space of vertex potentials. ContDiffAt of order $\top$ means infinite differentiability in the Fréchet sense at that point.
Supporting geometry (affine-independent interiors, cofactor derivatives, concrete Regge action) already supplies the polynomial and strict-interior facts; this structure names the configuration rather than hiding the requirements as axioms.
proof idea
No proof body: this is a structure definition. Its three fields are Prop-valued hypotheses that a later constructor packages from (1) local realized tetrahedra giving the arccos endpoint condition, (2) a separately stated global zero-deficit condition at the zero potential, and (3) the smoothness theorem for the local chart that yields ContDiffAt of the Regge action at zero. Sibling lemmas such as flatConfiguration_of_localChart_zeroDeficit assemble instances.
why it matters
This is the analytic gate for the cubic Taylor cascade on the nonlinear Regge action. Downstream, CanonicalRemainderAnalyticClosureCert takes a FlatConfiguration together with first- and second-variation jet inputs to close the nonlinear cubic Taylor theorem. Multiple remainder theorems (ContDiffAt of the canonical remainder and of its line restriction, local bounds on the third iterated Fréchet derivative, line chain-rule bounds) are proved of_flatConfiguration by reading off the ContDiffAt field and the flat base point.
In the Recognition geometry stack this is the named interface between discrete curvature (deficit angles on a triangulation) and continuum Taylor estimates needed for effective continuum limits. It does not itself invoke the forcing chain T0–T8 or the J-cost; it sits in the Regge/geometry layer that feeds higher continuum arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.