Geometry Deficit Linearization Linearization Coefficients

Linearization coefficients

In Regge calculus, space is approximated by a grid of flat pieces, and curvature is concentrated along the hinges where these pieces meet. The deficit angle at a hinge measures how much the pieces fail to lie flat: zero means a perfectly flat neighborhood, while a positive value signals curvature. Regge calculus is a standard tool in numerical relativity, introduced by Tullio Regge in 1961, and it is the framework used here.

The linearization coefficients answer a precise question: if you start with a flat grid and nudge each edge length by a small amount, how much does each deficit angle change? The answer is a linear approximation. For a hinge h and an edge e, the coefficient records the partial derivative of the deficit angle with respect to that edge length, evaluated at the flat background. The predicted deficit under a perturbation η is then a weighted sum of these coefficients times the edge perturbations, with a minus sign because deficit equals 2π minus the total angle around the hinge.

The declaration LinearizationCoefficients packages this data as a formal structure: a flat background complex, an edge-wise perturbation, and the coefficient matrix. It is a definitional choice, a way to organize the mathematics, not a theorem about the physical world. The classical result that such coefficients exist comes from Piran and Williams (1986), who derived the linearization of the Regge deficit angle around a flat simplicial complex.

What the structure enables is a theorem. When the coefficients satisfy Schläfli's identity, a geometric relation among the derivatives, the first-order Regge action vanishes. The theorem linear_regge_vanishes proves that the sum over hinges of area times linearized deficit equals zero. This means the leading nontrivial contribution to the action is quadratic in the perturbations, a fact that connects to the framework's cost function, which is also quadratic in its natural variable.

In Recognition Science, this linearization is a step toward showing that a discrete geometry can behave like a field theory. The framework models the Regge action as a discrete ledger of geometric costs, and the vanishing of the linear term is what makes the quadratic term the leading behavior. The declaration itself does not prove that the coefficients exist for any particular complex; it packages the data and the conditions under which the vanishing theorem holds.

The cubic lattice case, where edges are shared by four unit cubes, has explicit coefficients that are integer-linear in the perturbations. That concrete case is already implicit in earlier work; this declaration supplies the abstract machinery for the general simplicial case. The certificate DeficitLinearizationCert records that the vanishing theorem is proved, with zero unresolved goals and zero new axioms.

/-- Linearization coefficients: for each (hinge, edge) pair, the partial
    derivative of the deficit angle with respect to the edge length,
    evaluated at the flat background. -/
structure LinearizationCoefficients (nH nE : ℕ) extends
    DeficitDerivativeMatrix nH nE

/-- 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 declaration does not prove that linearization coefficients exist for any particular simplicial complex. It does not claim that the Regge action itself vanishes, only its first-order part. It does not establish the physical bridge from recognition to geometry.

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: