FastRadioBurstFromBITCert
plain-language theorem explainer
The FastRadioBurstFromBITCert structure bundles eight properties that certify the fast-radio-burst period model derived from the BIT carrier on the phi-ladder. Astrophysicists modeling repeating FRB periodicities would cite this certificate when deriving multi-day timescales from the 0.124 s carrier via exact 360-fold amplification per rung. The structure is populated by direct substitution of the explicit carrier formula together with the already-proved geometric-progression and monotonicity lemmas.
Claim. Let $P_0 = 1/(5 phi)$ be the BIT carrier period and let $A=360$ be the per-rung amplification factor. The certificate asserts: $0 < P_0$, $0.12 < P_0 < 0.13$, $A=360$, the period $P(k)=P_0 A^k$ satisfies $0 < P(k)$ for every natural number $k$, $P(k+1)=P(k) A$, $k < m$ implies $P(k) < P(m)$, $P_0 = 1/(5 phi)$, and $phi > 1$.
background
The BIT carrier period is defined as $1/(5 phi)$ seconds. The FRB amplification factor is the integer 360 obtained as the product of the eight-tick window and the gap-45 factor. The period at rung $k$ is obtained by multiplying the carrier by $360^k$ (FRB_period_at_rung).
proof idea
The structure is a pure definition that collects the eight required fields. Each field is supplied by a sibling lemma or definition already proved in the same module: positivity and band membership follow from the explicit formula for BIT_carrier_period together with the numerical bounds on phi; the amplification equality is the definition of FRB_amplification_factor; the geometric and increasing properties are the theorems FRB_period_geometric and FRB_period_strict_increasing.
why it matters
This certificate closes Track AS8 of the Recognition Science plan. It is instantiated by the downstream definition fastRadioBurstFromBITCert, which demonstrates that the certificate is inhabited. The construction relies on the eight-tick octave (T7) and the phi-ladder period formulas; it supplies the concrete prediction that adjacent rungs differ by exactly the factor 360, a testable signature for multi-rung FRB catalogs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.