zeroPotential
plain-language theorem explainer
The constant-zero assignment of conformal potentials to every vertex of a finite 3D Regge triangulation. It is the flat basepoint for Taylor expansions of the Regge action under the conformal ansatz. Anyone working second-variation or remainder identities cites it. The body is the constant map to 0.
Claim. For any finite 3D triangulation $K$, the zero conformal potential is the map sending every vertex index to $0\in\mathbb{R}$.
background
The module supplies the Hessian interface for the genuine Regge action on a finite 3D triangulation under a conformal ansatz. Analytic inputs stay explicit: a concrete implementation must give the action, a Hessian matrix, and the identity that the quadratic Taylor coefficient is that matrix.
A Triangulation3D packages finite vertex/edge/tetrahedron counts with incidence data and nondegenerate squared-edge lengths on each tet. Vertex conformal potentials are real-valued assignments on the finite vertex set: maps $\mathrm{Fin},n_V\to\mathbb{R}$. The zero potential is the distinguished flat configuration against which first and second variations are measured.
Downstream concrete Regge data subtract the action at this zero potential and a candidate quadratic Hessian term to form the nonlinear Taylor remainder.
proof idea
Definitional: the constant function fun _ => 0 of type VertexPotential K. No lemmas or tactics.
why it matters
This is the flat basepoint for the entire second-order Regge calculus stack. Concrete structures (ConcreteReggeActionData, ConcreteReggeSecondOrderData) evaluate the action and second variation relative to it. The remainder reggeActionRemainder is defined by subtracting the value at zero potential and half the Hessian quadratic form; the companion theorem shows that remainder vanishes at zero for every candidate Hessian.
It also feeds the forcing-chain bridge certificate T5_To_NonlinearReggeJCost_Bridge, which links T5 J-uniqueness to the nonlinear Regge curvature-action picture. Without a canonical zero section, the conformal Taylor expansion and the J-cost bridge have no fixed origin.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.