AsteroidTrajectoryShapingCert
plain-language theorem explainer
The AsteroidTrajectoryShapingCert structure records the carrier frequency band 8.05 to 8.10, positive impulse coefficient, and the four deflection properties for the quadratic model δ(t) = (I t²)/2. Engineers applying phantom-cavity drives to NEO deflection cite it to certify compliance with the RS trajectory derivation. The structure is assembled directly from the module's sibling theorems on zero value, non-negativity, doubling, and strict positivity.
Claim. A record asserting carrier frequency satisfies $8.05 < 5φ < 8.10$, impulse coefficient $I > 0$, and deflection function $δ(t) = (I t^2)/2$ obeys $δ(0) = 0$, $δ(t) ≥ 0$ for all $t$, $δ(2t) = 4 δ(t)$ for all $t$, and $δ(t) > 0$ whenever $t ≠ 0$.
background
The module defines deflection at lead time t as δ(t) = (impulseCoefficient · t²)/2, where impulseCoefficient encodes recoil from a phantom-cavity drive at carrier frequency 5φ Hz. This quadratic form follows from cumulative per-cycle impulses Δp = m · v_recoil with v_recoil proportional to carrier frequency. Upstream results include the explicit carrier_frequency definition and the deflection_pos theorem from gravitational lensing that supplies the underlying positivity pattern.
proof idea
Structure definition that directly references the module theorems deflection_zero, deflection_nonneg, deflection_double, and deflection_pos_of_ne_zero for its fields, together with the carrier_frequency_band and impulseCoefficient_pos predicates. No separate tactics or reductions are performed inside the structure itself.
why it matters
It supplies the master certificate for the engineering derivation in Track J1, instantiated by the downstream asteroidTrajectoryShapingCert definition. The record closes the falsifier clause that observed deflection must match t² scaling to 3σ over twelve months. It applies the quadratic scaling forced by the self-similar fixed point and eight-tick octave to concrete trajectory control.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.