FRB_period_geometric
plain-language theorem explainer
FRB periods form a geometric sequence with common ratio exactly 360 across adjacent rungs on the BIT carrier ladder. Modelers of repeating fast radio bursts in the Recognition Science framework cite this to obtain the closed-form P(k) = base * 360^k. The algebraic identity follows immediately from unfolding the period definition and applying power successor plus ring normalization.
Claim. Let $P(k)$ denote the FRB period at rung $k$, defined by $P(k) = P_0 · 360^k$ where $P_0$ is the base carrier period. Then $P(k+1) = P(k) · 360$.
background
In the FastRadioBurstFromBIT module the FRB period at rung $k$ is defined as the base BIT carrier period multiplied by the amplification factor to the power $k$. The amplification factor is the constant 8 × 45, which the module identifies with the eight-tick window times the gap-45 per-rung step. The module doc states that this yields the closed form $P_{FRB}(k) = (1/(5φ)) · 360^k$ and supplies the structural prediction that adjacent rungs differ by exactly 360.
proof idea
The proof is a one-line wrapper that unfolds FRB_period_at_rung on both sides, rewrites the successor power, and normalizes the resulting polynomial identity with ring.
why it matters
The result supplies the geometric clause required by the FastRadioBurstFromBITCert structure and by the one-statement theorem fast_radio_burst_one_statement. It encodes the per-rung amplification step that follows from the eight-tick octave and gap-45 construction in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.