curvature_from_deficit
plain-language theorem explainer
curvature_from_deficit defines discrete curvature as the ratio of deficit angle to dual area on a cubic lattice. Lattice gravity and Regge calculus researchers cite it to connect edge deficits to continuum curvature. The definition is a direct division that supplies the bridge used to equate lattice curvature with the second derivative of the metric perturbation.
Claim. The curvature scalar is defined by $K = {δ}/{A}$, where $δ$ denotes the deficit angle at an edge and $A$ is the dual area associated with that edge.
background
The module formalizes discrete curvature via deficit angles in the style of Regge calculus. On a flat cubic lattice each dihedral angle is π/2, so the deficit angle δ_e = 2π − sum of dihedral angles around an edge vanishes; a metric perturbation h deforms the angles and produces nonzero deficits. The J-cost of neighboring ledger entries encodes the strain that drives these deformations, and in the quadratic limit J(ratio) ≈ (1/2)(log ratio)^2 yields the second derivative of the strain as the deficit angle (normalized by lattice area). Upstream results supply the structure of J-cost (PhiForcingDerived.of) and the factorization of the ledger (DAlembert.LedgerFactorization.of) that calibrate this strain.
proof idea
This is a one-line definition that returns the supplied deficit angle divided by the supplied area.
why it matters
The definition supplies the central bridge invoked by curvature_equals_d2h to prove lattice curvature equals −d²h, by ricci_is_sum_of_curvatures to express the linearized Ricci scalar as a sum of three such terms, and by lattice_ricci to define the lattice Ricci scalar. It realizes the Regge action convergence to the Einstein-Hilbert action inside the Recognition Science framework and links the discrete deficit directly to the J-cost strain on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.