IndisputableMonolith.Foundation.SimplicialLedger.NonlinearBridge
The NonlinearBridge module defines the exact J-cost action on weighted ledger graphs using the full cosh coupling prescribed by the Recognition Composition Law. Researchers deriving the discrete-to-continuum bridge to Einstein equations cite it when replacing the quadratic approximation with the precise nonlinear form. The module consists of definitions and supporting lemmas on nonnegativity and exact decomposition, with no core proofs.
claimThe exact J-cost action on a weighted ledger graph is given by $exactJCostAction(G,ε)=∑_{i,j}w_{ij}(cosh(ε_i−ε_j)−1)$, where this cosh form is the functional required by the Recognition Composition Law (contrasted with its quadratic truncation $laplacian_action(G,ε)$).
background
This module belongs to the Foundation.SimplicialLedger layer and imports Constants (with τ₀=1 tick), Cost, ContinuumBridge, and EdgeLengthFromPsi. The ContinuumBridge doc states that the J-cost functional on the simplicial ledger is the Regge action (up to κ=8φ⁵) and that J-cost stationarity yields the Regge equations. EdgeLengthFromPsi links the recognition potential ψ on 3-simplices to the edge lengths needed for the Regge action. The module's doc-comment identifies the exactJCostAction as the full cosh-based coupling that the Recognition Composition Law prescribes, with the quadratic laplacian_action as its leading-order truncation via exact_decomposition.
proof idea
This is a definition module, no proofs. It introduces exactJCostAction together with sibling lemmas (exactJCostAction_flat, exactJCostAction_nonneg, Jcost_ratio_eq_cosh_minus_one, coshRemainder and its nonnegativity and zero cases, quarticRemainder, laplacian_action_prod_form, exact_decomposition) that establish algebraic identities and sign properties of the cosh remainder.
why it matters in Recognition Science
The module supplies the precise nonlinear functional required by the Recognition Composition Law for the discrete ledger. It feeds the ContinuumBridge module, whose doc-comment states that J-cost stationarity gives the Regge equations and thereby the Einstein field equations. The definitions close the gap between the ledger and the full Regge action in the Gravity from Recognition draft without invoking the weak-field approximation.
scope and limits
- Does not derive the Recognition Composition Law.
- Does not prove the Regge-action identification.
- Does not treat the continuum limit or discretization error.
- Does not include the weak-field quadratic truncation as a theorem.
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