Geometry Deficit Linearization Edge Perturbation

Edge perturbations and the flat background

Regge calculus is a discrete approximation to general relativity in which spacetime is built from flat triangular pieces, like a curved surface approximated by a polyhedron. The curvature lives at the hinges, the shared edges between pieces, and is measured by a deficit angle: the amount by which the angles around a hinge fall short of a full turn. In a flat region, every deficit is zero. The question this page addresses is what happens when one edge length is nudged by a small amount η, and whether the resulting change in the deficit angles can be treated as a simple linear response.

The classical answer, from T. Piran and R. M. Williams in 1986, is that it can. Around a flat background, a small perturbation of each edge length induces a deficit angle that is, to first order, a sum over edges of a coefficient times the perturbation, with corrections of order η². The coefficients depend on the combinatorics of the simplicial complex and on the vertex-angle measure. For the cubic lattice, where each edge is shared by four unit cubes, the coefficients are integer-linear in the perturbations. This is the standard linearization of Regge calculus, a tool that predates the Recognition Science framework by decades.

In Recognition Science, the declaration EdgePerturbation (a discrete record of the edge-length changes) packages exactly this classical data. It is a structure that holds, for each edge, a real number η_e representing the change in that edge's length. The framework's library of formal theorems then records the linearized deficit at each hinge as a sum of coefficients times these perturbations, and it proves a key consequence: under the flat background and Schläfli's identity, the first-order Regge action vanishes. This means the leading nontrivial action is quadratic in the perturbations, matching the form of a Dirichlet energy. The theorem linear_regge_vanishes states this result for any well-shaped package of data.

The vanishing of the linear term is not an accident; it is a structural fact. Schläfli's identity, a classical relation among the variations of dihedral angles and edge lengths, forces the sum of areas times deficit changes to cancel at first order. The framework's contribution is to record this as a machine-checked theorem, with zero unproved axioms, in its library of formal mathematics. The practical payoff is that the Regge action, when expanded around a flat background, begins at second order, which is what a continuum limit needs if it is to recover a wave equation or a Laplacian.

What this declaration does not claim is just as important. It does not prove that the linearization coefficients exist for every simplicial complex; that existence is classical Regge calculus, assumed as input. It does not show that the quadratic action matches the J-cost Dirichlet energy; that matching is a target for later phases. And it does not establish that the physical recognition-to-linking bridge holds. The declaration is a precise, limited tool: it packages the data of an edge perturbation and proves that, under the stated conditions, the first-order action vanishes.

/-- A perturbation of the flat edge-lengths. -/
structure EdgePerturbation (nE : ℕ) where
  eta : Fin 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 existence of linearization coefficients for every simplicial complex is not proved here; it is assumed from classical Regge calculus. The quadratic action matching the J-cost Dirichlet energy is not established by this declaration. The physical recognition-to-linking bridge is not addressed by this declaration.

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: