BIT_carrier_period_pos
plain-language theorem explainer
The theorem establishes positivity of the BIT carrier period 1/(5 phi) in the Recognition Science phi-ladder. Astrophysicists deriving FRB periodicities from the canonical carrier band would cite this result to guarantee all rung-amplified periods remain positive. The proof is a term-mode reduction that unfolds the definition and applies div_pos together with mul_pos using phi_pos and a norm_num check on the constant 5.
Claim. $0 < 1/(5 phi)$ where $phi$ is the golden-ratio fixed point of the Recognition Composition Law.
background
In the FastRadioBurstFromBIT module the BIT carrier period is defined as the reciprocal of five times phi, placing the fundamental carrier at frequency 5 phi Hz with period approximately 0.124 s. This definition anchors the phi-ladder construction for FRB periods, where each rung multiplies by the factor 360 arising from the eight-tick octave and gap-45 amplification.
proof idea
Term-mode proof: unfold BIT_carrier_period to expose the division 1/(5*phi), apply div_pos one_pos to reduce to positivity of the denominator, then discharge the product via mul_pos with a norm_num proof that 5 > 0 and the upstream phi_pos lemma.
why it matters
The result supplies the base positivity witness required by fastRadioBurstFromBITCert and by the inductive statements FRB_period_at_rung_pos and FRB_period_strict_increasing. It closes the carrier-band case for the structural FRB prediction on the phi-ladder (T6 fixed point, T7 eight-tick octave) before any rung amplification is applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.