JCostToEFE
plain-language theorem explainer
The structure packages the J-cost to Einstein field equations derivation chain by asserting the quadratic expansion of J in log coordinates, the discrete Laplacian structure on weighted graphs, and the normalization kappa equal to 8 phi to the fifth. Researchers closing the discrete-to-continuum gap in recognition science derivations of gravity would cite this when linking Regge action stationarity to EFE. It is realized as a structure definition whose fields are populated directly from the quadratic identity and the stationarity equivalence.
Claim. The J-cost to Einstein field equations chain is the structure whose fields assert: the J-cost functional is defined; the quadratic approximation satisfies $J_quadratic(ε) = ε^2/2$; for any weighted ledger graph, stationarity of the discrete Laplacian implies that the weighted sum of field differences vanishes for each vertex; the normalization factor equals $8φ^5$; and this factor is positive.
background
This module closes the gap between the discrete recognition science ledger and Einstein's field equations. The key insight is that the quadratic structure of J-cost in log coordinates ε = ln ψ matches the Regge action exactly, so J-cost stationarity yields the same equations as Regge minimization, which converge to EFE. J_log_quadratic is the quadratic approximation of J in log coordinates, with quartic error bound ε^4/24 for |ε|<1. WeightedLedgerGraph is a simplicial graph with nonnegative symmetric edge weights. The discrete Laplacian at vertex i is defined as the weighted sum ∑_j w_ij (ε_i - ε_j). Upstream results supply the gravitational constant G = λ_rec² c³ / (π ℏ) and the normalization factor jcost_to_regge_factor = 8 φ^5.
proof idea
The declaration is a structure definition with five fields and no proof body. The fields are instantiated downstream by direct substitution: the quadratic identity holds by definition of J_log_quadratic, the Laplacian structure follows from the stationarity equivalence lemma applied to the discrete Laplacian, and the kappa equalities are taken from the constant definitions.
why it matters
This structure is the core component of the Continuum Bridge Certificate, which certifies that J-cost stationarity on the simplicial ledger produces the Einstein field equations in the continuum limit with coupling κ = 8 φ^5. It completes the derivation chain in the module documentation: SimplicialLedger.J_global through log-coordinate expansion and discrete Laplacian identification to Regge action identification and the continuum limit. It directly supports the framework step from the Recognition Composition Law and phi-ladder to D = 3 spatial dimensions via the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.