IndisputableMonolith.Foundation.SimplicialLedger.NonlinearBridge
The NonlinearBridge module defines the exact J-cost action on weighted ledger graphs using the full cosh coupling sum w_ij (cosh(ε_i - ε_j) - 1). Researchers deriving discrete gravity from Recognition Science cite it to supply the nonlinear form required by the Recognition Composition Law. It consists of definitions and basic properties that contrast this exact action with its quadratic Laplacian truncation.
claimThe exact J-cost action on a weighted ledger graph is \( \sum_{i,j} w_{ij} (\cosh(\varepsilon_i - \varepsilon_j) - 1) \). This is the full nonlinear form prescribed by the Recognition Composition Law; the quadratic Laplacian action is its leading-order truncation.
background
This module sits in the Foundation.SimplicialLedger layer and imports Constants (fixing the RS time quantum τ₀ = 1 tick), Cost, ContinuumBridge, and EdgeLengthFromPsi. ContinuumBridge states: "This module closes the critical gap between the discrete RS ledger and Einstein's field equations by proving: 1. The J-cost functional on the simplicial ledger IS the Regge action (up to normalization by κ = 8φ⁵). 2. J-cost stationarity (δJ = 0) gives the Regge equations." EdgeLengthFromPsi identifies the recognition-potential field ψ on 3-simplices with the edge lengths required for the Regge action via the Field-Curvature Identity.
The module supplies the exact nonlinear J-cost without weak-field approximation, as forced by the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) with J(x) = cosh(log x) - 1.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the exact cosh-based J-cost action that enables the identification in ContinuumBridge of the J-cost functional with the Regge action. It directly implements the nonlinear form required by the Recognition Composition Law and the T5 J-uniqueness step in the forcing chain, supporting the bridge from discrete ledger to Einstein field equations.
scope and limits
- Does not derive the continuum limit to Einstein equations.
- Does not assume or apply weak-field approximation.
- Does not normalize the action by κ = 8φ⁵.
- Does not identify the potential ε with the recognition field ψ.
- Does not address stationarity conditions or Regge equations.
depends on (4)
declarations in this module (19)
-
def
exactJCostAction -
theorem
exactJCostAction_flat -
theorem
exactJCostAction_nonneg -
theorem
Jcost_ratio_eq_cosh_minus_one -
theorem
exactJCostAction_via_Jcost -
def
coshRemainder -
theorem
coshRemainder_nonneg -
theorem
coshRemainder_zero -
def
quarticRemainder -
theorem
quarticRemainder_nonneg -
theorem
laplacian_action_prod_form -
theorem
exact_decomposition -
theorem
exact_flat_agrees_with_linearized -
structure
NonlinearDeficitFunctional -
def
NonlinearReggeJCostIdentity -
theorem
nonlinear_field_curvature_identity -
theorem
jcost_stationarity_to_regge_nonlinear -
structure
NonlinearJCostReggeCert -
theorem
nonlinearJCostReggeCert