deficit_angle_deformed
plain-language theorem explainer
The definition sets the deficit angle on a deformed cubic lattice edge to -a squared times the second derivative of the metric perturbation h. Discrete gravity researchers using Regge calculus cite it to link lattice strain to continuum curvature. It is a direct algebraic expression obtained from the leading-order dihedral angle shift under quadratic metric deformation.
Claim. The deficit angle at a lattice edge is defined by $δ = -a^2 (d^2 h / dx^2)$, where $a$ denotes lattice spacing and $h$ is the metric perturbation.
background
The module formalizes discrete curvature on a cubic lattice via Regge-style deficit angles. On flat Z^3 each dihedral angle is π/2; a metric perturbation h deforms these angles so that the deficit at an edge equals 2π minus the sum of the surrounding dihedrals. In the quadratic limit the J-cost of neighboring ledger entries supplies the strain, with J(ratio) ≈ (1/2)(log ratio)^2 whose second derivative yields the deficit (normalized by lattice area). Upstream structures supply the J-cost calibration (LedgerFactorization.of) and the phi-forcing derivation of the strain measure (PhiForcingDerived.of).
proof idea
The declaration is a one-line definition that directly encodes the leading-order approximation: four dihedral shifts each contribute (a^2/4) d2h, the total deficit is their negative sum, and the expression simplifies to -a^2 d2h.
why it matters
It supplies the explicit bridge used by curvature_equals_d2h to prove lattice deficit maps to continuum curvature -d2h, and by ricci_is_sum_of_curvatures to recover the linearized Ricci scalar as the sum over three axes. The definition therefore anchors the Regge action convergence to the Einstein-Hilbert integral and the RS connection between J-cost strain and sectional curvature. It closes one step in the discrete-to-continuum passage inside the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.