Geometry Deficit Linearization

Linearizing curved space

Geometry deficit linearization is a standard technique in Regge calculus, a discrete approach to general relativity where space is built from flat triangular or tetrahedral pieces. In 1986, T. Piran and R. M. Williams showed that when you start with a flat arrangement of these pieces and nudge each edge length by a small amount, the resulting curvature, measured as a deficit angle at each hinge, changes linearly with those nudges to first order. The formula reads δ_h = Σ_e (∂δ_h / ∂L_e)|_flat · η_e + O(η²), where η_e is the small change in edge length e and the coefficients come from the geometry of the complex. This linearization is the discrete analog of taking a Taylor expansion of curvature around flat space.

The technique matters because it turns a hard nonlinear problem into a tractable linear one. For a cubic lattice, where each edge is shared by four unit cubes, the coefficients become integer-linear in the perturbations. If the edge changes come from a log-potential field through the conformal ansatz η_e = a · (ε_i + ε_j)/2, then the deficit becomes a linear combination of ε-differences. The Regge action, S_Regge = Σ_h A_h · δ_h, then becomes quadratic in ε, with the linear term vanishing by Schläfli's identity combined with flatness. This quadratic form matches the Dirichlet energy of the J-cost from Recognition Science, which is why the framework uses it.

In the machine-checked library of formal theorems, the module DeficitLinearization packages this classical result. It defines a flat simplicial complex, an edge perturbation, and linearization coefficients, then bundles them into a well-shaped package, meaning the background is flat, coefficients exist, and Schläfli's identity holds. The key proved theorem, linear_regge_vanishes, states that the first-order Regge action vanishes under these conditions. In plain language: for a slightly curved space built from flat pieces, the leading curvature effect is quadratic in the deformation, not linear. The certificate deficitLinearizationCert records this as a formal theorem with zero sorry, meaning no admitted gaps, and zero new axioms.

The practical consequence is that the framework can treat small geometric perturbations as a quadratic energy, which is exactly the form its cost function takes. This is not a new physical prediction; it is a formal confirmation that a known calculus result holds in the framework's setting. The module supplies the abstract machinery needed for general simplicial complexes, with the concrete cubic lattice case already handled elsewhere. What the theorem changes is that the quadratic regime is now a proved fact, not an assumption, for any flat background satisfying the well-shaped conditions.

/-- 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 linearization coefficients for general simplicial complexes are not computed in this module, only their existence is packaged. The physical bridge from Regge calculus to continuum general relativity is not established here. The quadratic action is not claimed to be the full J-cost, only to match its Dirichlet energy form.

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: