IndisputableMonolith.Gravity.SevenGaps.LedgerEnergyBridge

declarations in this module (31)

• def quadraticCurvatureEnergy L79
• theorem quadraticCurvatureEnergy_nonneg L85
• theorem quadraticCurvatureEnergy_pos L93
• theorem sinh_le_self_mul_cosh L112
• theorem abs_sinh_le_abs_mul_cosh L128
• theorem cosh_sub_one_le_half_sq_mul_cosh L137
• theorem cosh_remainder_nonneg L160
• theorem cosh_remainder_le L167
• theorem cosh_one_lt_two L177
• theorem Jcost_exp_sub_half_sq_abs_le L191
• def IsCoboundary L214
• theorem rclGate_Jcost_eq L230
• def coboundaryStrainLedger L249
• def gateViolatingStrain L287
• theorem gateViolatingStrain_antisymm L292
• theorem gateViolatingStrain_vals L300
• theorem general_antisymmetric_strain_can_violate_rcl L317
• theorem coboundary_totalCost_quadratic_matching L348
• def strainHingeAreas L408
• def strainHingeDeficits L414
• theorem quadraticCurvatureEnergy_strainHinges L419
• structure LedgerToQuadraticEnergyBridge L441
• def canonicalQuadraticEnergyBridge L467
• def rectangleShearPotential L497
• theorem rectangleShearPotential_strains L503
• theorem rectangleShear_ledgerEnergy_pos L524
• theorem rectangleShear_quadraticEnergy_pos L554
• def rectangleShearBridge L569
• structure LedgerEnergyBridgeStatus L606
• def ledgerEnergyBridgeStatus L628
• theorem ledgerEnergyBridgeStatus_flags L639