158theorem bimodal_ratio_lt_phi_nine : bimodal_ratio < phi ^ 9 := by
proof body
Term-mode proof.
159 unfold bimodal_ratio recycling_rung_shift 160 have h_phi : 1 < phi := one_lt_phi 161 exact pow_lt_pow_right₀ h_phi (by norm_num : 8 < 9) 162 163/-! ## §4. The bimodality gap: no pulsars at intermediate rungs 164 165The empirical pulsar-period distribution shows almost no pulsars at 166`P ≈ 30–100 ms`. In RS, this corresponds to rungs `k_ms ∈ {1, ..., 7}` 167of the millisecond family — these are *unstable* under J-cost 168minimisation (each is exactly one φ-step from a stable rung, costing 169J(φ) per step). 170 171We don't formally prove the empirical bimodality; we expose the 172structural gap as a sub-cert. 173-/ 174 175/-- The structural rung gap: rungs 1–7 of the ms family are 176unstable. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.