IndisputableMonolith.Astrophysics.FastRadioBurstFromBIT
This module supplies the BIT carrier period and derived FRB quantities in Recognition Science. It sets the base period to 1/(5 phi) and constructs rung-dependent periods plus amplification factors via geometric scaling on the phi ladder. The module contains only definitions and elementary lemmas on positivity and monotonicity.
claimThe canonical BIT carrier period is defined as $1/(5 phi)$, where $phi$ is the self-similar fixed point. FRB periods at rung $r$ are obtained by geometric scaling of this base period, and the amplification factor satisfies the relation derived from the Recognition Composition Law.
background
Recognition Science takes the fundamental time quantum tau_0 = 1 tick from the Constants module. The Cost module supplies the J-cost function whose fixed point yields phi. This astrophysics module applies those primitives to fast radio bursts by introducing the BIT carrier period 1/(5 phi) and building a ladder of periods indexed by rung.
proof idea
This is a definition module, no proofs. It consists of direct definitions for BIT_carrier_period, FRB_amplification_factor, FRB_period_at_rung and supporting lemmas that verify positivity and strict increase using only the ordering properties of phi.
why it matters in Recognition Science
The module supplies the core objects used by FastRadioBurstFromBITCert and fast_radio_burst_one_statement. It applies the eight-tick octave (T7) and spatial dimension D=3 (T8) from the forcing chain to observable radio-burst timing, closing the link between the phi-ladder and astrophysical periods.
scope and limits
- Does not derive phi from the Recognition Composition Law inside this module.
- Does not compute numerical frequencies or dispersion measures for observed FRBs.
- Does not address propagation, redshift or host-galaxy effects.
- Does not prove uniqueness of the BIT carrier period among possible carriers.
depends on (2)
declarations in this module (12)
-
def
BIT_carrier_period -
theorem
BIT_carrier_period_pos -
theorem
BIT_carrier_period_band -
def
FRB_amplification_factor -
theorem
FRB_amplification_factor_eq -
def
FRB_period_at_rung -
theorem
FRB_period_at_rung_pos -
theorem
FRB_period_geometric -
theorem
FRB_period_strict_increasing -
structure
FastRadioBurstFromBITCert -
def
fastRadioBurstFromBITCert -
theorem
fast_radio_burst_one_statement