FRB_amplification_factor_eq
plain-language theorem explainer
FRB_amplification_factor_eq establishes that the per-rung amplification for fast radio burst periods equals 360. Modelers of FRB periodicities in the Recognition Science framework cite it to justify the geometric ratio when computing rung steps from the BIT carrier band. The proof reduces to unfolding the definition and normalizing the arithmetic product.
Claim. Let $A$ be the canonical fast radio burst per-rung amplification factor defined by the product of the eight-tick window and the consciousness gap, $A = 8 × 45$. Then $A = 360$.
background
The Fast Radio Burst From BIT module develops closed-form predictions for FRB periods on the phi-ladder. The base carrier period is 1/(5 phi) ≈ 0.124 s, and multi-rung periods follow by amplification with the per-rung factor 360^k. The factor itself is introduced as the product 8 * 45, corresponding to the eight-tick window combined with the gap-45 consciousness factor. The module documentation states that this yields the closed form P_FRB(k) = 0.124 s · 360^k, with the ratio between consecutive rungs being exactly 360.
proof idea
The proof is a one-line wrapper that unfolds the definition FRB_amplification_factor and applies norm_num to confirm the numerical equality 8 * 45 = 360.
why it matters
The equality is invoked by fastRadioBurstFromBITCert to populate the master certificate and by fast_radio_burst_one_statement to assert the full period formula P_FRB(k) = (1/(5 phi)) · 360^k. It implements the rung-step prediction highlighted in the module documentation that P_FRB(6)/P_FRB(5) = 360. This connects directly to the eight-tick octave landmark (T7) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.