deficit_scales_with_a_squared
plain-language theorem explainer
deficit_scales_with_a_squared establishes that the deformed deficit angle scales quadratically with lattice spacing. Doubling the spacing quadruples the deficit for fixed second derivative of the metric perturbation. Discrete gravity researchers cite it when converting Regge deficits to sectional curvature. The proof is a direct algebraic identity after unfolding and substitution.
Claim. Let $δ(d²h, a)$ denote the deformed deficit angle for second metric derivative $d²h$ and spacing $a$. Then $δ(d²h, 2a) = 4 · δ(d²h, a)$.
background
The DiscreteCurvature module formalizes Regge-style curvature on a cubic lattice using deficit angles. In flat space all dihedral angles are π/2 so the deficit vanishes. A metric perturbation h deforms the angles; its second derivative d2h encodes the strain from the quadratic J-cost approximation J(ratio) ≈ (1/2)(log ratio)². Upstream, the EdgeLengthFromPsi theorem links edge lengths to the ledger psi and references the Piran-Williams Regge formulation. The module shows deficits vanish for h=0 and that deficit over area converges to sectional curvature.
proof idea
The proof unfolds the definition of deficit_angle_deformed, rewrites using the hypothesis a2 equals 2 times a1, and applies the ring tactic to confirm the factor of four.
why it matters
This lemma supports the subsequent definitions of curvature_from_deficit and linearized_ricci_from_deficits. It realizes the Regge 1961 result that the action sum of deficit times area converges to the Einstein-Hilbert integral. In the Recognition framework it confirms that the second derivative of J-strain supplies the discrete curvature, consistent with the phi-ladder discretization and D=3 spatial dimensions. It closes one step toward continuum gravity without open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.