module module

`IndisputableMonolith.Foundation.SimplicialLedger.NonlinearBridge`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge module_import
IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi module_import

declarations in this module (19)

def exactJCostAction L98
theorem exactJCostAction_flat L104
theorem exactJCostAction_nonneg L110
theorem Jcost_ratio_eq_cosh_minus_one L130
theorem exactJCostAction_via_Jcost L137
def coshRemainder L158
theorem coshRemainder_nonneg L162
theorem coshRemainder_zero L168
def quarticRemainder L177
theorem quarticRemainder_nonneg L183
theorem laplacian_action_prod_form L193
theorem exact_decomposition L210
theorem exact_flat_agrees_with_linearized L238
structure NonlinearDeficitFunctional L259
def NonlinearReggeJCostIdentity L266
theorem nonlinear_field_curvature_identity L278
theorem jcost_stationarity_to_regge_nonlinear L304
structure NonlinearJCostReggeCert L341
theorem nonlinearJCostReggeCert L367