module module

`IndisputableMonolith.Gravity.SevenGaps.Gap5ChartFromLedgerMomentum`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Cost.SymplecticAction module_import

declarations in this module (48)

abbrev LedgerState L160
def balanced L164
def imbalance L168
def total L171
def casimir L175
theorem below L180
def orbitPoint L181
def linFunctional L186
def VanishesAtBalanced L190
def Balanced L197
theorem vanishesAtBalanced_iff L210
theorem imbalance_is_the_unique_linear_selection L220
theorem imbalance_vanishesAtBalanced L230
theorem linFunctional_one_neg_one L233
theorem vanishesOnBalancedLocus_iff L250
theorem imbalance_forced_by_balance_locus L265
theorem tolerated_family_is_a_scale_ray L281
def toVec L302
def imbalanceTotalMap L305
theorem imbalanceTotalMap_apply L307
theorem imbalanceTotalMap_det L314
theorem imbalance_total_is_a_canonical_pair L321
theorem Jlog_eq_two_sinh_half_sq L335
theorem orbitPoint_casimir L343
theorem orbitPoint_imbalance L355
theorem Jlog_eq_imbalance_sq_div_two_casimir L366
theorem chart_variable_is_the_normalized_imbalance L376
theorem chart_is_the_imbalance_coordinate L387
theorem sinh_two_arsinh L398
def powTwoJlog L408
theorem powTwoJlog_not_quadratic_in_imbalance L415
def nlP L451
def nlQ L455
theorem nlP_factor L457
theorem nlP_eq_zero_iff L462
theorem nlP_strictMono L471
theorem nlP_hasDerivAt L476
theorem nlP_hasDerivAt_snd L483
theorem nlQ_hasDerivAt_snd L486
theorem nl_jacobian_det_eq_one L499
theorem cost_not_quadratic_in_nlP L508
theorem chart_not_forced_without_linearity L523
theorem event_cost_differs_from_state_cost L539
theorem orbitPoint_is_reached_by_event L551
theorem additive_continuous_balanced_is_imbalance L593
theorem imbalance_is_additive_continuous_balanced L626
structure ChartStipulatedVerdict L648
theorem chartStipulatedVerdict L708