jcost_stationarity_implies_regge
plain-language theorem explainer
Stationarity of the J-cost action on a simplicial ledger, expressed as vanishing of the discrete Laplacian, implies equality of that action with a scaled Regge action. Researchers deriving discrete gravity from recognition-based ledger minimization would cite the result when equating their variational principle to Regge calculus. The proof is a direct one-line application of the field-curvature bridge identity.
Claim. Let $B$ be a field-curvature bridge consisting of a weighted ledger graph together with a perturbation field $ε$. If the discrete Laplacian of the ledger graph vanishes at every vertex for this $ε$, then the J-cost action of $B$ equals $(1/κ)$ times the Regge action induced by the same ledger data, where $κ$ is the normalization factor matching the quadratic structures.
background
The module establishes the continuum bridge from the discrete J-cost functional on a simplicial ledger to Regge calculus and ultimately the Einstein field equations. A FieldCurvatureBridge packages a WeightedLedgerGraph together with a perturbation field $ε : Fin n → ℝ$; its jcost_action is defined as the Dirichlet energy laplacian_action of that graph and field, while regge_action is the corresponding deficit-angle sum normalized by the same data. The key local fact is that the quadratic expansion of J in log coordinates, J(e^ε) = ε²/2 + O(ε⁴), produces exactly the discrete Laplacian structure that matches the quadratic form of the Regge action. Upstream results include the proved J_global functional on the simplicial ledger and the quadratic expansion of J proved in the Cost module.
proof idea
The proof is a one-line wrapper that applies the bridge_identity lemma packaged inside the FieldCurvatureBridge structure. That identity directly equates the two actions once the discrete Laplacian vanishes, with the constant factor arising from the κ-normalization already built into the bridge definition.
why it matters
The declaration closes the critical discrete-to-continuum step in the Recognition Science derivation chain: J-cost stationarity on the ledger yields Regge stationarity, which in turn converges to the Einstein equations under the Cheeger-Müller-Schrader limit. It thereby supports the full sequence from SimplicialLedger.J_global through the quadratic Laplacian identification to the Einstein field equations with κ = 8φ⁵. The result sits inside the T5–T8 forcing chain by confirming that the self-similar J-cost functional reproduces the geometric action whose stationary points are the Einstein equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.