asteroidTrajectoryShapingCert
plain-language theorem explainer
The certificate definition for asteroid trajectory shaping assembles a record verifying carrier frequency in (8.05, 8.10) Hz together with positive impulse and quadratic deflection scaling under lead time. Engineers working on near-Earth object deflection models would cite it to confirm the t-squared law and the quadrupling property upon doubled lead time. The construction is a direct structure fill-in that references the pre-established carrier band theorem and the positivity plus scaling lemmas for the deflection function.
Claim. The asteroid trajectory shaping certificate asserts that the carrier frequency satisfies $8.05 < f < 8.10$, the impulse coefficient is positive, and the deflection function obeys $δ(0)=0$, $δ(t)≥0$ for all real $t$, $δ(2t)=4δ(t)$ for all $t$, and $δ(t)>0$ whenever $t≠0$, where $δ(t)=(I·t^2)/2$ and $I$ denotes the impulse coefficient.
background
In this module the deflection at lead time $t$ is defined by $δ(t)=(impulseCoefficient·t^2)/2$. The carrier frequency is obtained from the golden-ratio constant phi via the factor 5 phi, which the carrier_frequency_band theorem places inside (8.05, 8.10) using the known bounds phi > 1.61 and phi < 1.62. The module also records that impulseCoefficient is positive and proves the four deflection properties (zero at origin, non-negative everywhere, doubling rule, and strict positivity for nonzero argument) by direct algebraic manipulation of the quadratic expression.
proof idea
The definition is a structure constructor that assigns the carrier band field to the carrier_frequency_band theorem, the impulse positivity field to impulseCoefficient_pos, the zero field to deflection_zero, the non-negativity field to deflection_nonneg, the doubling field to deflection_double, and the strict-positivity field to deflection_pos_of_ne_zero. It is therefore a one-line wrapper that assembles already-proved module lemmas into the required certificate record.
why it matters
This definition supplies the complete certificate realizing the engineering derivation stated in the module header: a phantom-cavity drive produces positive per-cycle impulse and cumulative deflection that scales quadratically with lead time, with the explicit falsifier that observed NEO deflection must match the t-squared law to within 3 sigma over a twelve-month window. It closes the engineering application of the Recognition Science constants (phi-derived carrier frequency) and supplies the concrete claim that would be cited by any downstream trajectory-shaping calculation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.