BIT_carrier_period
plain-language theorem explainer
The definition sets the fundamental BIT carrier period to the reciprocal of five times the golden ratio phi. Astrophysicists modeling repeating fast radio bursts in the Recognition Science framework cite this as the base scale on the phi-ladder before 360-fold rung amplification. It is introduced as a direct one-line real-number assignment with no lemmas or proof steps.
Claim. The canonical BIT carrier period is defined by $P = 1/(5 phi)$, where $phi$ is the golden ratio satisfying the self-similar fixed-point equation from the forcing chain.
background
In the Recognition Science setting the phi-ladder supplies discrete scaling for physical quantities, with the eight-tick octave (T7) and gap-45 amplification generating the factor 360 per rung. The module imports phi from Constants and treats the carrier period as the fundamental frequency scale (approximately 8.09 Hz) whose reciprocal yields the base period of roughly 0.124 s. FRB repeaters are then placed at higher rungs via multiplication by 360^k, recovering the observed multi-day to multi-month periodicities from the single structural rule.
proof idea
The declaration is a direct definition that assigns the real number obtained by dividing 1 by the product of 5 and phi. No lemmas are invoked and no tactics are applied; it functions as a one-line abbreviation that subsequent theorems unfold to obtain positivity, numerical bounds, and the geometric FRB period formula.
why it matters
This definition supplies the base period required by FastRadioBurstFromBITCert and fast_radio_burst_one_statement, which together assert that FRB periods obey P(k) = (1/(5 phi)) * 360^k. It realizes the RS structural prediction for FRB periodicity on the phi-ladder amplified by the eight-tick octave, closing the zero-sorry part of Track AS8. The parent theorems then derive the band (0.12, 0.13) s and the per-rung geometric ratio without further hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.