carrier_frequency_band
plain-language theorem explainer
The theorem establishes that the carrier frequency in asteroid trajectory shaping lies strictly between 8.05 Hz and 8.10 Hz. Engineers modeling phantom-cavity drives for near-Earth object deflection would cite this interval to anchor the operating point at five times the golden ratio. The proof unfolds the definition of carrier frequency and invokes the known bounds 1.61 < phi < 1.62 to obtain the result by linear arithmetic.
Claim. $8.05 < 5phi < 8.10$, where $phi$ is the golden ratio.
background
The Asteroid Trajectory Shaping module treats a phantom-cavity drive that produces per-cycle impulse Delta p = m * v_recoil with v_recoil = hbar_R * omega_carrier / c^2 at carrier frequency omega_carrier = 5 phi Hz. The definition carrier_frequency := 5 * phi is imported from the same module and appears in sibling engineering files for cortical neuromodulation and phantom-coupled GW antennas. Upstream lemmas supply the tight bounds 1.61 < phi and phi < 1.62 that scale directly under multiplication by five.
proof idea
The term proof unfolds carrier_frequency to expose 5 * phi, obtains the two phi-bound lemmas, and applies linarith to each side of the resulting inequalities.
why it matters
This bound is required by the one-statement summary asteroid_one_statement and by the certification record asteroidTrajectoryShapingCert. It anchors the engineering derivation inside the Recognition Science framework where phi is the self-similar fixed point forced at step T6 of the unified forcing chain. The interval supports the claim that cumulative deflection scales as t squared with lead time.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.