FRB_period_strict_increasing
plain-language theorem explainer
The FRB period function is strictly monotone increasing with rung index. Astrophysicists modeling repeating fast radio bursts would cite this to establish that higher-rung carriers produce longer observed periods. The proof reduces the claim to the positivity and magnitude of the amplification factor via power and multiplication inequalities.
Claim. Let $P(k)$ denote the fast radio burst period at rung $k$, defined by $P(k) = T_0 · 360^k$ where $T_0$ is the base carrier period. For natural numbers $k < m$, $P(k) < P(m)$.
background
In the Fast Radio Burst from BIT module the period at rung $k$ is defined as the product of the base carrier period and $360^k$. The amplification factor equals 360 by the theorem FRB_amplification_factor_eq, which encodes the canonical per-rung step from the eight-tick window times the gap-45 factor. The base carrier period is positive by the upstream theorem BIT_carrier_period_pos and lies in the numerical band (0.12, 0.13) s.
proof idea
The proof unfolds the definition of FRB_period_at_rung. It establishes that the amplification factor is positive and strictly greater than one using FRB_amplification_factor_eq together with norm_num. The power inequality follows from pow_lt_pow_right₀ applied to the base greater than one and the hypothesis $k < m$. The final step multiplies both sides by the positive carrier period via mul_lt_mul_of_pos_left.
why it matters
This monotonicity result completes the set of structural properties required for the FastRadioBurstFromBITCert master certificate, which collects positivity, band membership, amplification equality, geometric ratio, and strict increase. It supports the one-statement theorem fast_radio_burst_one_statement that summarizes the closed-form FRB period $P_{FRB}(k) = (1/(5φ)) · 360^k$. Within the Recognition framework it instantiates the eight-tick octave and gap-45 amplification on the phi-ladder for astrophysical predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.