module module

`IndisputableMonolith.Engineering.AsteroidTrajectoryShaping`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (13)

def carrier_frequency L39
theorem carrier_frequency_pos L41
theorem carrier_frequency_band L44
def impulseCoefficient L53
theorem impulseCoefficient_pos L55
def deflection L62
theorem deflection_zero L64
theorem deflection_nonneg L67
theorem deflection_double L74
theorem deflection_pos_of_ne_zero L80
structure AsteroidTrajectoryShapingCert L89
def asteroidTrajectoryShapingCert L97
theorem asteroid_one_statement L108