FRB_period_at_rung_pos
plain-language theorem explainer
The theorem proves that the fast radio burst period at any natural-number rung k is strictly positive. Astrophysicists modeling repeating FRB periodicity on the phi-ladder would cite this result to confirm physical viability of the predicted timescales. The argument is a direct term-mode wrapper that unfolds the period definition, applies positivity of the base carrier and of powers, substitutes the amplification factor 360, and normalizes.
Claim. For every natural number $k$, the FRB period at rung $k$ defined by $P(k) = P_0 · 360^k$, where $P_0$ is the BIT carrier period, satisfies $P(k) > 0$.
background
The module treats FRB periods as points on the phi-ladder of the BIT carrier band. The fundamental carrier period lies near 0.124 s; multi-day repeater periods arise by scaling this base by the per-rung factor 360, which encodes the eight-tick octave combined with gap-45 amplification. The definition FRB_period_at_rung k therefore reads BIT_carrier_period multiplied by 360 to the power k.
proof idea
The proof unfolds FRB_period_at_rung, applies mul_pos to BIT_carrier_period_pos and the power term, invokes pow_pos, rewrites the amplification factor to 360 via FRB_amplification_factor_eq, and finishes with norm_num.
why it matters
The result supplies the positivity field required by the master certificate fastRadioBurstFromBITCert. It closes the structural claim that FRB periods obey the closed form 0.124 s · 360^k on the phi-ladder, consistent with the eight-tick octave and gap-45 steps of the Recognition Science forcing chain. The theorem thereby supports the sharp prediction that adjacent rungs differ by exactly 360.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.