regge_action_from_hinges
plain-language theorem explainer
The definition sums deficit angles weighted by hinge areas to recover the Regge action from the simplicial ledger. Physicists working on discrete gravity would cite this when bridging J-cost stationarity to Einstein equations. The implementation is a direct fold over the hinge list.
Claim. The Regge action for a list of hinges is the sum over each hinge of (deficit angle) times (area), where each hinge carries a positive area and a real deficit angle.
background
The module establishes that the J-cost functional on the simplicial ledger equals the Regge action up to the normalization factor κ = 8φ⁵. In log coordinates the quadratic expansion of J(e^ε) = cosh(ε) - 1 yields a discrete Laplacian whose stationarity reproduces the Regge equations, which in turn converge to the Einstein field equations. HingeContribution packages the local data (deficit angle and area) needed for this sum. Upstream constants supply G in RS-native units as λ_rec² c³ / (π ℏ), while the cost definitions from MultiplicativeRecognizerL4 and ObserverForcing supply the J-cost that this action matches.
proof idea
One-line wrapper that applies foldl to accumulate the product of deficit angle and area over the list of hinges.
why it matters
This definition supplies the explicit identification of J-cost action with Regge action inside the derivation chain SimplicialLedger.J_global → log-coordinate expansion → discrete Laplacian → Regge action identification → κ = 8φ⁵ normalization → continuum limit = EFE. It therefore closes the discrete-to-continuum step required by the module's program and sits directly on the T5–T8 forcing chain and the Recognition Composition Law. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.