218def pulsarPeriodFromRungCert : PulsarPeriodFromRungCert where 219 normal_median_rung_eq := rfl
proof body
Definition body.
220 ms_median_rung_eq := rfl 221 recycling_rung_shift_eq := rfl 222 period_geometric := period_geometric 223 bimodal_ratio_pos := bimodal_ratio_pos 224 bimodal_ratio_gt_thirty := bimodal_ratio_gt_thirty 225 bimodal_ratio_lt_phi_nine := bimodal_ratio_lt_phi_nine 226 gap_size_eq := gap_size_eq 227 228/-! ## §6. One-statement summary -/ 229 230/-- **PULSAR PERIOD FROM RECOGNITION-RUNG: ONE-STATEMENT THEOREM 231(Track AS7).** 232 233The pulsar-period bimodal distribution is forced by the canonical 2348-tick recycling shift between two φ-ladder families: normal 235pulsars at base period `τ_neutron · φ^k`, millisecond pulsars at 236base period `τ_neutron · φ^(k-8)`. The bimodal ratio 237`P_normal_median / P_ms_median = φ^8 > 30` is sharply distinguishable 238from a continuous distribution. The structural gap of 7 unstable 239intermediate rungs explains the empirical "pulsar period gap" at 240`P ≈ 30–100 ms`. -/
depends on (30)
Lean names referenced from this declaration's body.