jcost_to_efe_chain
plain-language theorem explainer
The declaration instantiates the J-cost to Einstein field equations derivation chain by verifying each required step in the target structure. Researchers connecting discrete Recognition Science ledgers to continuum general relativity would cite this to justify the Regge-to-EFE passage. The term-mode proof constructs the structure directly via triviality for the definition, reflexivity for the quadratic expansion, and prior lemmas for the Laplacian stationarity and kappa normalization.
Claim. The J-cost functional on the simplicial ledger satisfies the derivation chain to Einstein's field equations, where the cost is defined, the quadratic expansion satisfies $J(e^ε) = ε^2/2$, the discrete Laplacian structure enforces stationarity by requiring that weighted neighbor differences sum to zero for each vertex, the Regge normalization factor equals $8φ^5$, and this factor is positive.
background
The Continuum Bridge module establishes that J-cost stationarity on the simplicial ledger yields the Regge equations and hence the Einstein field equations. J-cost is the functional induced by the multiplicative recognizer comparator on positive ratios, reparametrized in log coordinates ε = ln ψ so that J(e^ε) expands as cosh(ε) − 1. The simplicial ledger is represented by a WeightedLedgerGraph whose discrete Laplacian is the weighted sum of neighbor differences; stationarity of this Laplacian recovers the Regge action up to the factor κ = 8φ^5 drawn from the RS-native constants.
proof idea
The term proof directly constructs the JCostToEFE structure. The first step is instantiated by trivial. The quadratic step is obtained by reflexivity. The Laplacian-structure step applies the stationarity_iff_laplacian_zero lemma. The final two steps invoke the equality and positivity lemmas for the Regge factor.
why it matters
This theorem supplies the missing link that turns the quadratic J-cost structure into the Regge action and thereby into the Einstein field equations, completing the derivation chain listed in the module documentation. It is used by the continuum_bridge_cert theorem that certifies the full bridge. The result realizes the module's key insight that J-cost minimization reproduces Regge calculus because both are quadratic in the deficit angles, with the normalization κ = 8φ^5 matching the RS forcing-chain constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.