pith. machine review for the scientific record. sign in
def definition def or abbrev

asteroidTrajectoryShapingCert

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

formal statement (Lean)

  97def asteroidTrajectoryShapingCert : AsteroidTrajectoryShapingCert where
  98  carrier_band := carrier_frequency_band

proof body

Definition body.

  99  impulse_pos := impulseCoefficient_pos
 100  deflection_zero := deflection_zero
 101  deflection_nonneg := deflection_nonneg
 102  deflection_double := deflection_double
 103  deflection_pos := @deflection_pos_of_ne_zero
 104
 105/-- **ASTEROID TRAJECTORY ONE-STATEMENT.** Carrier frequency
 106`5φ ∈ (8.05, 8.10) Hz`; cumulative deflection scales as `t²` with
 107lead time; doubling lead time quadruples deflection. -/

depends on (12)

Lean names referenced from this declaration's body.