IndisputableMonolith.Foundation.SimplicialLedger.NonlinearBridge
NonlinearBridge supplies the exact nonlinear J-cost action on weighted ledger graphs via the full cosh coupling. Researchers closing the discrete ledger to Regge action would cite it when replacing the quadratic truncation. The module defines the action and records its nonnegativity, flat zero, and decomposition into Laplacian plus remainder terms.
claimThe exact J-cost action on a weighted graph is $S = ∑_{i,j} w_{ij} (cosh(ε_i − ε_j) − 1)$, where the sum runs over edges with weights $w_{ij}$ and $ε$ is the recognition potential; this is the form prescribed by the Recognition Composition Law.
background
The module sits inside the simplicial-ledger layer of Recognition Science. It imports the RS time quantum τ₀ = 1 tick from Constants and the J-cost machinery from the Cost module. It extends the ContinuumBridge result that identifies the J-cost functional with the Regge action (up to κ = 8φ⁵) and the EdgeLengthFromPsi result that equates the recognition potential on 3-simplices with the full set of edge lengths needed for that action.
proof idea
This is a definition module, no proofs. It introduces the exact cosh form of the action together with auxiliary lemmas on the cosh and quartic remainders and their nonnegativity.
why it matters in Recognition Science
The module supplies the precise nonlinear expression required by the Recognition Composition Law for the J-cost functional that ContinuumBridge equates with the Regge action. It therefore feeds the stationarity condition that yields the Regge equations and, via EdgeLengthFromPsi, the Field-Curvature Identity that links the potential field to curvature.
scope and limits
- Does not derive the Einstein field equations.
- Does not fix the overall normalization constant κ.
- Does not perform the continuum limit.
- Does not contain the weak-field quadratic truncation.
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