field_curvature_identity_under_linearization
plain-language theorem explainer
Under the ReggeDeficitLinearizationHypothesis for a deficit-angle functional D, scale a, hinge list, and weighted ledger graph G, the J-cost Dirichlet energy on any log-potential equals one over the coupling factor times the actual Regge sum on the conformal edge-length field. Workers deriving discretized gravity from recognition potentials would cite the result to equate the two actions without circular definition. The proof is a short algebraic rearrangement that substitutes the hypothesis into a normalized identity and clears the denominator
Claim. If the linearization hypothesis holds for deficit-angle functional $D$, scale $a>0$, hinges, and weighted ledger graph $G$, then for every log-potential $ε$, the J-cost Dirichlet energy satisfies $Δ_G ε = (1/κ) · Σ_h A_h δ_h(L(ε))$, where $κ$ is the coupling constant, $L(ε)$ is the conformal edge-length field scaled by $a$, and the sum is the Regge action with areas $A_h$ and deficits $δ_h$.
background
The module supplies the map from recognition potential ψ on simplices to edge-length geometry for Regge calculus. DeficitAngleFunctional assigns deficit angle and area to each hinge given an edge-length field. HingeDatum records incident edges and nonnegative weights. LogPotential is the assignment ε_i = ln ψ(σ_i). ReggeDeficitLinearizationHypothesis asserts that the Regge sum on the conformal field equals κ times the Laplacian action at leading order for small ε.
proof idea
The tactic proof extracts nonzeroness of the coupling factor and applies the hypothesis to the input log-potential. A calc block rewrites the Laplacian as (1/κ)·(κ·Laplacian) via field_simp, regroups by ring, and substitutes the hypothesis to reach the Regge sum on the right-hand side.
why it matters
This supplies the non-tautological field-curvature identity, invoked by field_curvature_identity_cubic, edgeLengthFromPsiCert, and field_curvature_identity_simplicial. It realizes the paper proposition in the Gravity from Recognition draft §5, equating J-cost Dirichlet energy to linearized Regge action with coupling κ = 8 φ^5. It leaves open explicit discharge of the linearization hypothesis via Cayley-Menger or Piran-Williams computations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.