Geometry Deficit Linearization Deficit Linearization Cert

The linearization certificate

In Regge calculus, spacetime is approximated by a patchwork of flat pieces, like a geodesic dome. The deficit angle measures the bend where pieces meet: a measure of how much local flatness is violated. Around a perfectly flat background, a small change to any edge length induces a small change in each deficit angle, and to first order that change is a linear combination of the edge perturbations. The Piran-Williams (1986) linearization makes this precise, giving explicit coefficients for the first-order response.

The declaration deficitLinearizationCert packages the key consequence of that linearization as a machine-checked certificate. It states that for any flat background simplicial complex, any edge perturbation, and any set of linearization coefficients satisfying Schläfli's identity, the first-order Regge action vanishes: the sum over hinges of hinge area times linearized deficit is exactly zero. The certificate is inhabited by the proved theorem linear_regge_vanishes, which derives this from the flatness condition together with Schläfli's identity. The library that contains it is a machine-checked collection of formal theorems, and the certificate itself contains zero unproved assumptions and zero new axioms.

What this means physically is that the leading nontrivial Regge action is quadratic in the perturbation. First-order energy changes cancel out, so the first surviving response to a small geometric wobble is second order. That quadratic leading term is what later phases of the framework connect to a Dirichlet-type energy. The certificate does not compute the quadratic term, does not prove the linearization coefficients exist for any particular complex, and does not itself establish the connection to any physical field theory. It certifies only the vanishing of the first-order piece, under the stated hypotheses.

In the framework's internal program, this certificate is Phase C4, the step that discharges the Regge deficit linearization hypothesis on general simplicial complexes. The concrete coefficients for the cubic lattice were already implicit in an earlier phase; this file supplies the abstract machinery the general case will need. The certificate's value is that it makes the first-order vanishing a formal, checkable fact rather than a paper calculation.

structure DeficitLinearizationCert where
  linear_vanishes : ∀ {nH nE : ℕ}
    (W : WellShapedData nH nE) (η : EdgePerturbation nE),
    (∑ h : Fin nH, (W.complex.hinges h).area *
      linearizedDeficit W.coeffs η h) = 0

/-- The certificate is inhabited by the proved `linear_regge_vanishes`. -/
theorem deficitLinearizationCert : DeficitLinearizationCert where
  linear_vanishes := fun W η => linear_regge_vanishes W η

/-- 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]

/-- The certificate is inhabited by the proved `linear_regge_vanishes`. -/
theorem deficitLinearizationCert : DeficitLinearizationCert where
  linear_vanishes := fun W η => linear_regge_vanishes W η

What this page does not claim

The certificate does not prove the linearization coefficients exist for any particular complex. The certificate does not compute the quadratic term of the Regge action. The certificate does not itself establish a connection to any physical field theory.

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: