fastRadioBurstFromBITCert
plain-language theorem explainer
This definition inhabits the master certificate asserting that fast radio burst periods lie on the phi-ladder with exact 360-fold rung amplification. Astrophysicists modeling repeating FRB periodicities would cite the resulting closed-form P_FRB(k) = (1/(5 phi)) * 360^k. The construction is a structure literal that directly references pre-proved lemmas for positivity, numerical band, geometric progression, and strict monotonicity.
Claim. The master certificate is inhabited: the BIT carrier period satisfies $0 < P < 0.13$ and lies in $(0.12, 0.13)$ s; the amplification factor equals 360; periods at rung $k$ are positive, obey the recurrence $P(k+1) = P(k) * 360$, and increase strictly with $k$.
background
The module derives FRB repeater periods from the BIT carrier band inside the Recognition Science phi-ladder. The carrier period is defined as $1/(5 phi)$ and forced into the interval $(0.12, 0.13)$ s by real-arithmetic properties of phi. The canonical amplification per rung is the product of the eight-tick octave and gap-45 factor, yielding the integer 360. The FastRadioBurstFromBITCert structure packages eight clauses that together assert positivity, band membership, exact geometric scaling, and strict increase of the period sequence.
proof idea
The definition is a structure literal that populates each field of FastRadioBurstFromBITCert by direct reference: BIT_carrier_pos is assigned the theorem BIT_carrier_period_pos, BIT_carrier_band is assigned BIT_carrier_period_band, FRB_amplification_eq is assigned FRB_amplification_factor_eq, and the remaining fields are assigned the corresponding rung-positivity, geometric, and monotonicity theorems. The strict-increase clause is wrapped in a lambda that applies FRB_period_strict_increasing.
why it matters
This definition closes the structural theorem for FRB periods on Track AS8, supplying the explicit certificate that downstream results can invoke without additional hypotheses. It rests on the phi constant and the eight-tick amplification already established in the upstream forcing chain. The one-statement summary in the module records the concrete prediction P_FRB(k) = (1/(5 phi)) * 360^k that follows once the certificate is inhabited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.