induced_regge_action
plain-language theorem explainer
This definition supplies the induced Regge action on a weighted simplicial ledger graph G with perturbation field ε as the scaled discrete Laplacian action. Researchers deriving discrete curvature equations from J-cost stationarity cite it when matching to linearized Regge calculus. The implementation is a one-line wrapper that multiplies the precomputed jcost_to_regge_factor by laplacian_action G ε.
Claim. For a weighted simplicial graph $G$ and perturbation field $ε$, the induced Regge action equals the J-cost-to-Regge normalization factor times the discrete Laplacian action of $G$ on $ε$, which identifies the J-cost variation with the linearized Regge action under the $κ=8φ^5$ scaling.
background
The module establishes the bridge from discrete J-cost stationarity on simplicial ledgers to the Einstein field equations via Regge calculus. WeightedLedgerGraph is the structure holding a symmetric nonnegative weight matrix on $n$ vertices that encodes the ledger edges and their couplings. The J-cost functional in log coordinates $ε=lnψ$ expands as $cosh(ε)-1=ε^2/2+O(ε^4)$, so the coupling term between neighboring simplices produces exactly the quadratic form of a discrete Laplacian action. Upstream results include the gravitational constant $G$ from Constants (derived as $λ_{rec}^2 c^3/(π ħ)$) and the bridge packaging from ClassicalBridge.Fluids.CPM2D.
proof idea
This is a one-line wrapper that applies jcost_to_regge_factor to the result of laplacian_action G ε. The factor encodes the $κ=8φ^5$ normalization that converts the quadratic J-cost Dirichlet energy into the linearized Regge action; no further tactics or reductions are required.
why it matters
The definition supplies the explicit Regge-action expression consumed by the FieldCurvatureBridge structure. It completes the derivation step from SimplicialLedger.J_global through the discrete Laplacian identification to the Regge-action identification, allowing the $κ$-normalization to match the Einstein field equations. It touches the open question of continuum-limit convergence referenced in the module's citation of Cheeger-Müller-Schrader (1984).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.