FieldCurvatureBridge
plain-language theorem explainer
The FieldCurvatureBridge structure assembles a weighted simplicial ledger graph with a real-valued perturbation field epsilon on its vertices. It supplies the J-cost action as the discrete Laplacian energy on that graph and the induced Regge action from the same ledger data under the kappa scaling. Workers on discrete gravity and Regge calculus cite the construction to equate J-cost stationarity with Regge stationarity. The bridge identity is obtained by unfolding the two action definitions and applying field_simp plus ring to cancel the known-
Claim. A field-curvature bridge for $n$ consists of a weighted ledger graph $G$ and a perturbation field $ε : Fin n → ℝ$. Its J-cost action is the discrete Laplacian action of $G$ on $ε$. Its Regge action is the induced Regge action from the same ledger data. The bridge identity states that the J-cost action equals $(1/κ) ×$ the Regge action, where $κ = jcost_to_regge_factor ≠ 0$.
background
The module establishes the continuum bridge from J-cost stationarity on the simplicial ledger to the Einstein field equations. WeightedLedgerGraph is a structure carrying a nonnegative symmetric weight function on Fin n × Fin n that represents the ledger; its discrete Laplacian action supplies the quadratic Dirichlet energy. Upstream results include the cost function from MultiplicativeRecognizerL4 (derivedCost on positive ratios) and from ObserverForcing (Jcost of a RecognitionEvent), together with the CPM2D bridge that packages classical defect and energy gaps for traceability.
proof idea
The structure definition directly records the ledger_graph and epsilon fields. jcost_action is a one-line wrapper that applies laplacian_action to those fields. regge_action is the analogous one-line wrapper around induced_regge_action. The bridge_identity theorem unfolds both actions, obtains the nonzero factor via jcost_to_regge_factor_ne_zero, then uses field_simp and ring to rearrange the scaling identity.
why it matters
This supplies the central data structure for the continuum bridge module, which closes the gap between the discrete RS ledger and Einstein's field equations. It feeds the theorem jcost_stationarity_implies_regge (showing J-cost stationarity implies Regge stationarity) and the ReggeDeficitLinearizationHypothesis in EdgeLengthFromPsi. The module doc places it in the derivation chain from SimplicialLedger.J_global through log-coordinate quadratic expansion to discrete Laplacian identification and κ = 8φ⁵ normalization, ultimately reaching the continuum limit to the EFE.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.