module module

`IndisputableMonolith.Gravity.SevenGaps.DescentPrincipleUniversality`

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.StrainDynamicsKernelReach module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.StrainDescent module_import

declarations in this module (25)

theorem sourceCost1_hasDerivAt L99
theorem deriv_sourceCost1 L108
theorem sourceCost1_continuous L112
theorem self_le_sinh L117
theorem one_add_sq_div_two_le_cosh L132
theorem sourceCost1_coercive L153
theorem sourceCost1_strictMonoOn L170
theorem sourceCost1_strictAntiOn L183
theorem sourceCost1_lt_of_ne L196
theorem sourceCost1_min_le L202
def descentField L213
theorem descentField_zero_iff L218
theorem descentField_descends L240
theorem metric_not_forced L256
theorem cost_decreasing_dynamics_converges L285
theorem rest_state_forced L372
theorem cost_decreasing_dynamics_converges' L401
theorem continuity_is_load_bearing L413
theorem strainResidual_continuous L456
theorem strainEnvelope_continuous L460
theorem strainStepSize_continuous L465
theorem strainStep1_continuous L470
theorem strainStep1_converges_by_universality L478
theorem descent_principle_residue L499
theorem link_channels_converge L515