WellShapedData
WellShapedData packages a flat simplicial complex on nH hinges and nE edges, the linearization coefficients for deficit angle derivatives at flat lengths, and the Schläfli identity on those components. Discrete gravity researchers linearizing Regge actions around flat backgrounds cite this package. It is introduced as a structure to support proofs that the first-order Regge action vanishes identically under the flat background.
claimLet $n_H, n_E$ be natural numbers. A well-shaped data package consists of a flat simplicial complex $C$ with $n_H$ hinges and $n_E$ edges, linearization coefficients $M$ recording the partial derivatives of each deficit angle with respect to edge lengths at the flat background, and the Schläfli identity asserting that the area-weighted sum of those derivatives vanishes for each edge.
background
The module develops the Piran-Williams linearization of the Regge deficit angle around a flat simplicial complex. A FlatSimplicialComplex records finitely many hinges each satisfying the flat-sum condition on dihedral angles together with strictly positive flat edge lengths. LinearizationCoefficients extend the deficit derivative matrix and supply the first-order coefficients for the induced deficit under edge perturbations. The local setting is Phase C4 of discharging the Regge deficit linearization hypothesis on general simplicial complexes, where the linear term in the action vanishes by Schläfli's identity combined with flatness.
proof idea
This declaration is a structure definition that records the flat complex, the coefficients, and the Schläfli identity as three fields. No lemmas or tactics are applied; the structure serves directly as a typed package for downstream vanishing statements.
why it matters in Recognition Science
WellShapedData supplies the input package required by linear_regge_vanishes and DeficitLinearizationCert, which in turn feed the master certificate SimplicialFieldCurvatureCert. It fills the Phase C4 slot, ensuring the Regge action becomes quadratic in the perturbation and aligns with the J-cost Dirichlet energy. The module positions it as the abstract machinery needed before the sum rule with the Laplacian action on general complexes.
scope and limits
- Does not establish existence of the linearization coefficients for arbitrary complexes.
- Does not verify that the Schläfli identity holds for a given complex.
- Does not derive the explicit quadratic term in the action expansion.
- Does not restrict to or compute coefficients for the cubic lattice.
formal statement (Lean)
116structure WellShapedData (nH nE : ℕ) where
117 complex : FlatSimplicialComplex nH nE
118 coeffs : LinearizationCoefficients nH nE
119 schlaefli : SchlaefliIdentity complex.hinges coeffs.toDeficitDerivativeMatrix
120
121/-! ## §4. Linearized action vanishes at first order
122
123The key consequence: under the flat background and Schläfli's identity,
124the *first-order* Regge action vanishes. This means the leading
125non-trivial Regge action is *quadratic* in the perturbation, precisely
126matching the J-cost Dirichlet energy.
127
128The statement we need:
129
130 `Σ_h A_h · linearizedDeficit_h(η) = - Σ_e (Σ_h A_h · ∂θ_h/∂L_e) · η_e
131 = 0 (by Schläfli per edge).`
132-/
133
134/-- The linear (first-order) part of the Regge action vanishes under
135 Schläfli's identity. -/