deficitAngle_zero_of_flat
plain-language theorem explainer
On any incidence-consistent 3D Regge triangulation that admits a flat analytic configuration, every edge deficit vanishes at the zero conformal potential. Geometers working the nonlinear Regge action cite it to read flatness off the configuration package. The proof is a one-line field projection from that structure.
Claim. Let $K$ be a finite 3D Regge triangulation with consistent incidence data. If $K$ carries a flat analytic configuration (arccos endpoints free at the base, zero edge deficits, and $C^\infty$ Regge action at the origin), then for every global edge $e$, the Regge deficit angle of $K$ at the zero vertex potential equals zero: $\delta_K(0,e)=0$.
background
The module supplies analytic hypotheses for the full nonlinear Regge action, beyond the exact quadratic truncation used by the closed second-order component theorem. Those hypotheses are packaged as a named configuration rather than left as axioms: 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 FlatConfiguration on an incidence-consistent triangulation $K$ has three fields: local arccos endpoint freeness at squared-edge data of every tetrahedron; the zero-deficit flatness condition at the base potential; and $C^\infty$ smoothness of the Regge action at that base point. The deficit angle at a global edge is $2\pi$ minus the sum of local dihedral contributions under the vertex-conformal ansatz. The zero potential is the constant-zero vertex potential on $K$.
proof idea
One-line term proof: project the second field of the flat-configuration hypothesis. That field is already the universal quantification over edges of deficitAngle K (zeroPotential K) e = 0, so the goal is definitionally the structure projection h_flat.flat_deficit_zero.
why it matters
The nonlinear Regge stack needs a clean interface between geometric flatness and the analytic package used for Taylor expansion of the action. Extracting zero deficit as a standalone theorem lets downstream smoothness and Hessian arguments invoke flatness without unpacking the whole configuration. The module frames this as input to smoothness of the finite Regge action at the flat potential, which is required before any second-order expansion of the full nonlinear action can be justified. No downstream consumers are wired yet in the graph; the declaration is the public face of the flatness field inside FlatConfiguration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.