module module

`IndisputableMonolith.Gravity.SevenGaps.HingeStationarityCore`

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.StationarityBridgeClosure module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Gravity.SevenGaps.LedgerEnergyBridge module_import

declarations in this module (28)

theorem closedCycle_coboundary_sum_eq_zero L114
def naiveLogRatio L129
theorem budget_implies_ratio_without_stationarity L137
theorem cosh_tangent_line_le L149
theorem cosh_tangent_line_lt L170
theorem sourced_pointwise_le L191
theorem sourced_pointwise_lt L200
def sourcedAction L218
def sourcedMinimizer L223
theorem sourcedAction_eq_sum L228
theorem sourcedAction_eq_jcost_sum L242
theorem sourced_minimizer_le L250
theorem sourced_minimizer_unique L259
theorem sourced_unique_minimizer L282
theorem arsinh_le_self_of_nonneg L292
theorem self_sub_cube_le_arsinh L301
theorem abs_arsinh_sub_self_le L346
theorem sourced_ratio_cubic_error L371
theorem constrained_equal_split L398
theorem constrained_equal_split_eq_iff L437
structure RecognitionRatioFamily L493
def sourcedRatioFamily L516
theorem sourced_ratio_isAdmissible L537
theorem J_exp_quadratic_band L589
def sourcedValue L614
theorem sourcedValue_eq_action_min L620
theorem sourced_costTerm_hasDerivAt L635
theorem valueFn_deriv L662