module module

`IndisputableMonolith.Gravity.SevenGaps.Gap5EnergyEqualsCostDerivation`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumMagnitudeBridge module_import

declarations in this module (21)

def orbitHamiltonian L117
def hamiltonianVectorField L122
def poissonLin L127
theorem hasDerivAt_exp_half L131
theorem hasDerivAt_exp_neg_half L138
theorem orbitPoint_is_hamiltonian_flow L148
theorem orbitHamiltonian_constant_on_orbit L178
theorem poisson_imbalance_total L186
theorem poisson_imbalance_total_eq_frame_det L191
theorem not_energyEqualsCost_nlP L198
theorem imbalance_momentum_package L217
theorem nlP_momentum_package L229
theorem energyEqualsCost_independent_of_hamiltonian_data L248
theorem energyEqualsCost_of_additive_continuous_balanced_unit L268
theorem energyEqualsCost_iff_pointwise_ratio_cost L294
theorem orbitPoint_eq_zero_of_nonpos L327
theorem neg_orbit_coverage L335
theorem imbalance_sq_eq_two_casimir_jcost L354
theorem quadrant_signs L366
structure EnergyEqualsCostDerivationVerdict L384
theorem energyEqualsCostDerivationVerdict L424