fast_radio_burst_one_statement
plain-language theorem explainer
The declaration packages four properties of the fast-radio-burst period ladder into one theorem: the base carrier period lies in (0.12, 0.13) s, the per-rung amplification equals 360, adjacent rungs differ by exactly that factor, and periods increase strictly with rung index. Astrophysicists modeling repeating FRBs would cite the resulting closed-form P(k) = (1/(5 phi)) * 360^k. The proof is a four-tuple term that directly invokes the four supporting lemmas already established in the module.
Claim. Let $P_0 := 1/(5 phi)$. Then $0.12 < P_0 < 0.13$, the amplification factor equals 360, $P(k+1) = P(k) * 360$ for every natural number $k$, and $P(k) < P(m)$ whenever $k < m$, where $P(k) := P_0 * 360^k$.
background
The module derives FRB periods from the BIT carrier band in Recognition Science. BIT_carrier_period is defined as 1/(5 phi) and shown to lie in (0.12, 0.13) s. FRB_amplification_factor is defined as 8 * 45 and equals 360. FRB_period_at_rung(k) is then BIT_carrier_period * 360^k. MODULE_DOC states: 'In RS, FRB periods sit on the φ-ladder of the BIT carrier band. The fundamental carrier frequency 5 phi Hz ≈ 8.09 Hz corresponds to period 1/(5 phi) ≈ 0.124 s. Multi-day periods are obtained by canonical 8-tick × gap-45 amplification.'
proof idea
The proof is a term-mode construction that supplies the four conjuncts directly: BIT_carrier_period_band for the base interval, FRB_amplification_factor_eq for the factor value, FRB_period_geometric for the recurrence, and a lambda that applies FRB_period_strict_increasing to the hypothesis.
why it matters
This is the capstone one-statement theorem for Track AS8. It closes the structural derivation from the phi-ladder and eight-tick octave (T7) to observable periods, supplying the sharp prediction that adjacent rungs differ by exactly 360. The parent result is the module certification FastRadioBurstFromBITCert. It supplies the geometric ratio that should be detectable in any multi-rung repeater catalog.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.