`fast_radio_burst_one_statement`

proved

show as: view math explainer →

module: IndisputableMonolith.Astrophysics.FastRadioBurstFromBIT
domain: Astrophysics
line: 211 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Astrophysics.FastRadioBurstFromBIT on GitHub at line 211.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 208with adjacent rungs differing by exactly 360 and strict monotone
 209increase in `k`. The base BIT carrier period `1 / (5φ) ∈ (0.12,
 2100.13)` s is forced by the recognition lattice. -/
 211theorem fast_radio_burst_one_statement :
 212    -- (1) Base carrier period in band.
 213    (0.12 < BIT_carrier_period ∧ BIT_carrier_period < 0.13) ∧
 214    -- (2) Amplification factor = 360.
 215    FRB_amplification_factor = 360 ∧
 216    -- (3) Per-rung geometric ratio.
 217    (∀ k, FRB_period_at_rung (k + 1) =
 218      FRB_period_at_rung k * (FRB_amplification_factor : ℝ)) ∧
 219    -- (4) Strict monotone in rung count.
 220    (∀ {k m : ℕ}, k < m → FRB_period_at_rung k < FRB_period_at_rung m) :=
 221  ⟨BIT_carrier_period_band,
 222   FRB_amplification_factor_eq,
 223   FRB_period_geometric,
 224   fun h => FRB_period_strict_increasing h⟩
 225
 226end
 227
 228end FastRadioBurstFromBIT
 229end Astrophysics
 230end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.