carrier_frequency_pos
plain-language theorem explainer
The carrier frequency equals five times the positive self-similar fixed point phi and is therefore strictly positive. Asteroid trajectory modelers cite the result to guarantee that recoil velocity and impulse remain positive before integrating deflection over lead time. The proof is a one-line wrapper that unfolds the definition and applies the positivity of multiplication with a norm_num fact for the constant 5 together with the established positivity of phi.
Claim. $0 < 5phi$, where $phi$ is the positive self-similar fixed point of the Recognition Composition Law.
background
The Asteroid Trajectory Shaping module treats a phantom-cavity drive whose carrier frequency is set to five times the self-similar fixed point phi (in hertz). This frequency enters the recoil velocity formula $v_recoil = hbar_R * omega_carrier / c^2$ and thereby controls the sign of the per-cycle impulse delivered to the asteroid. The module works in RS-native units where $c=1$ and the forcing chain has already fixed $D=3$ and the eight-tick octave structure.
proof idea
The proof is a one-line wrapper. It unfolds the definition of carrier frequency to the product 5 * phi, then invokes mul_pos with a norm_num proof that 5 is positive and the upstream fact that phi is positive.
why it matters
The result supplies the positivity hypothesis required by the downstream theorem impulseCoefficient_pos, which in turn justifies the quadratic deflection formula delta(t) proportional to t squared. It directly imports the positivity of phi forced by J-uniqueness (T5) and the self-similar fixed point (T6) in the Recognition Science chain. The module's stated falsifier is an observed deflection inconsistent with the t-squared scaling to within 3 sigma over a twelve-month window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.