WellShapedData
plain-language theorem explainer
WellShapedData bundles a flat simplicial complex, its deficit-angle linearization coefficients, and a Schläfli-identity witness into one record. Workers linearizing the Regge action around flat backgrounds cite it to certify that the first-order term vanishes identically. The declaration is a structure definition that simply records the three required components.
Claim. A structure consisting of a flat simplicial complex with $n_H$ hinges and $n_E$ edges (each hinge obeying the flat dihedral sum), a matrix of first partial derivatives of deficit angles with respect to edge lengths evaluated at the flat background, and a witness that Schläfli's identity holds for those hinges and that derivative matrix.
background
The module carries out the Piran-Williams linearization of the Regge deficit around a flat simplicial complex. A flat simplicial complex comprises finitely many hinges and edges whose lengths are positive and whose dihedral angles at each hinge sum exactly to $2π$. Linearization coefficients are the entries of the Jacobian matrix of deficit angles with respect to edge lengths, taken at the flat point; they extend the deficit derivative matrix.
proof idea
This is a structure definition that packages the flat complex, the coefficients, and the Schläfli witness. No lemmas or tactics are invoked; the declaration merely records the data triple needed by the vanishing theorem and the master certificate.
why it matters
WellShapedData supplies the hypothesis for linear_regge_vanishes and for DeficitLinearizationCert; both feed the master certificate SimplicialFieldCurvatureCert. It closes Phase C4 of the program to discharge the Regge deficit linearization hypothesis, ensuring the leading Regge action is quadratic and matches the J-cost Dirichlet energy. The module records zero sorrys and zero new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.