deflection_pos_of_ne_zero
plain-language theorem explainer
The theorem establishes that cumulative deflection δ(t) is strictly positive whenever lead time t is nonzero. Engineers modeling phantom-cavity drives on near-Earth objects cite this to guarantee measurable trajectory change over any nonzero observation window. The proof is a term-mode wrapper that unfolds the deflection definition and applies div_pos together with mul_pos on the positive impulse coefficient and the positivity of t squared.
Claim. Let $k > 0$ be the impulse coefficient. For every real number $t ≠ 0$, the cumulative deflection satisfies $δ(t) = (k · t²)/2 > 0$.
background
The AsteroidTrajectoryShaping module derives deflection from a phantom-cavity drive that produces per-cycle impulse Δp = m · v_recoil at carrier frequency 5φ Hz. The deflection function is defined by δ(t) = (impulseCoefficient · t²)/2, where impulseCoefficient is shown positive by the upstream theorem impulseCoefficient_pos that reduces to carrier_frequency_pos. This local setting treats deflection as quadratic in lead time t (in dimensionless units) and collects positivity, nonnegativity, and doubling properties into a master certificate.
proof idea
The term proof first unfolds the definition of deflection. It then applies the div_pos lemma, supplying mul_pos impulseCoefficient_pos (by positivity) for the numerator and norm_num for the positive denominator 2.
why it matters
This theorem supplies the strict positivity leg required by the AsteroidTrajectoryShapingCert definition, which packages carrier_band, impulse_pos, deflection_zero, deflection_nonneg, and deflection_double. It directly supports the module claim that deflection scales as t² and that Δp remains positive for nonzero asteroid mass and drive cycles, consistent with the RS engineering derivation for RS_PAT_032. The result touches the module's stated falsifier of 3σ inconsistency with δ ∝ t² over a 12-month NEO tracking window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.