Geometry Deficit Linearization Well Shaped Data

What WellShapedData certifies

In Regge calculus, a spacetime is built from flat triangular blocks glued along their faces. The deficit angle is the amount by which the angles around a shared hinge fail to sum to a full circle; zero deficit means the blocks lie flat. Around a flat background, small changes to edge lengths produce small deficits, and the standard linearization, due to T. Piran and R. M. Williams in 1986, writes each deficit as a weighted sum of the edge changes plus higher-order corrections.

The declaration WellShapedData packages the conditions under which that linearization is well behaved. It bundles three ingredients: a flat background simplicial complex, a set of linearization coefficients, and Schläfli's identity relating the coefficients. Schläfli's identity is a classical relation among the derivatives of dihedral angles; here it is the exact condition that makes the first-order part of the Regge action vanish. The structure is a certificate: if you hold a WellShapedData object, you hold a proof that the complex is flat, the coefficients exist, and the identity holds.

The key consequence is a theorem proved in the machine-checked library of formal theorems: under these conditions, the first-order Regge action vanishes for any edge perturbation. Written out, the sum over hinges of area times linearized deficit equals zero. The leading nontrivial term is therefore quadratic in the perturbations, which is exactly the form of a Dirichlet energy. This is what the framework's Phase C5 needs to connect Regge calculus to its cost function.

What the declaration does not do is construct the coefficients for any particular lattice, nor does it prove that the quadratic term is positive. The concrete coefficients for the cubic lattice live in a separate file, and the general simplicial case is left as future work. WellShapedData is a scaffold, not a finished building.

/-- A complete well-shapedness package for the linearization. -/
structure WellShapedData (nH nE : ℕ) where
  complex : FlatSimplicialComplex nH nE
  coeffs : LinearizationCoefficients nH nE
  schlaefli : SchlaefliIdentity complex.hinges coeffs.toDeficitDerivativeMatrix

/-- The linear (first-order) part of the Regge action vanishes under
    Schläfli's identity. -/
theorem linear_regge_vanishes {nH nE : ℕ}
    (W : WellShapedData nH nE) (η : EdgePerturbation nE) :
    (∑ h : Fin nH, (W.complex.hinges h).area *
      linearizedDeficit W.coeffs η h) = 0 := by
  unfold linearizedDeficit
  -- Rewrite the sum: move the minus sign out, then swap summation order.
  have h_swap :
      (∑ h : Fin nH, (W.complex.hinges h).area *
        -(∑ e : Fin nE, W.coeffs.dThetadL h e * η.eta e))
      = - ∑ e : Fin nE,
          η.eta e * (∑ h : Fin nH, (W.complex.hinges h).area * W.coeffs.dThetadL h e) := by
    rw [show (∑ h : Fin nH, (W.complex.hinges h).area *
              -(∑ e : Fin nE, W.coeffs.dThetadL h e * η.eta e))
            = -(∑ h : Fin nH, (W.complex.hinges h).area *
                 (∑ e : Fin nE, W.coeffs.dThetadL h e * η.eta e))
         from by
           rw [← Finset.sum_neg_distrib]
           apply Finset.sum_congr rfl
           intro h _; ring]
    rw [show (∑ h : Fin nH, (W.complex.hinges h).area *
              (∑ e : Fin nE, W.coeffs.dThetadL h e * η.eta e))
            = ∑ h : Fin nH, ∑ e : Fin nE,
               (W.complex.hinges h).area * W.coeffs.dThetadL h e * η.eta e
         from by
           apply Finset.sum_congr rfl
           intro h _
           rw [Finset.mul_sum]
           apply Finset.sum_congr rfl
           intro e _; ring]
    rw [Finset.sum_comm]
    congr 1
    apply Finset.sum_congr rfl
    intro e _
    rw [← Finset.sum_mul]
    ring
  rw [h_swap]
  -- Now apply Schläfli's identity per edge.
  have h_each : ∀ e : Fin nE,
      η.eta e * (∑ h : Fin nH, (W.complex.hinges h).area * W.coeffs.dThetadL h e) = 0 := by
    intro e
    rw [W.schlaefli e, mul_zero]
  rw [Finset.sum_eq_zero (fun e _ => h_each e), neg_zero]

What this page does not claim

WellShapedData does not provide explicit linearization coefficients for any specific lattice. It does not prove the quadratic Regge action is positive definite. It does not establish that every simplicial complex admits such a well-shapedness package.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Geometry/DeficitLinearization.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: