Astrophysics Pulsar Period From Rung

The rung ladder for pulsar periods

Pulsars are rapidly spinning neutron stars that emit beams of radiation; their rotation periods, measured from the pulse arrival times, are famously bimodal. Normal pulsars have periods from about 16 milliseconds to 10 seconds, peaking near 0.5 to 1 second. Millisecond pulsars, which have been spun up by accreting matter from a companion, cluster between 1 and 30 milliseconds, peaking near 3 to 5 milliseconds. Between these two populations lies a clear gap at roughly 30 to 100 milliseconds, where very few pulsars are found (Lorimer & Kramer 2004; Manchester et al., ATNF Catalog 2024).

In Recognition Science, the framework models these periods as lying on a discrete ladder: each period is a base time multiplied by a power of the golden ratio φ ≈ 1.618. The normal pulsar family uses the neutron recognition time as its base, and the millisecond family uses a base that is smaller by a factor of φ^8, reflecting an eight-tick recycling shift from accretion. The framework's machine-checked library of formal theorems proves that the ratio of the two median periods is exactly φ^8, which is greater than 30 and less than φ^9. This 47-fold ratio is sharply distinguishable from a continuous distribution, and the library also proves that the gap between the families spans seven unstable intermediate rungs, matching the observed empty band.

The central theorem, named pulsar_period_one_statement, bundles four facts: both families have median rung 4, the recycling shift is 8 ticks, the bimodal ratio exceeds 30, and the structural gap has size 7. Each fact is proved from the definition of the golden ratio and the eight-tick shift, with no additional assumptions. The library does not prove the empirical bimodality itself; it exposes the structural gap as a consequence of the rung ladder, leaving the match to observation as a separate check.

The practical consequence is a sharp prediction: any pulsar period should fall on one of the two rung families, and the empty band between 30 and 100 milliseconds should remain empty. A statistically significant peak inside that band would falsify the structure. The framework's account thus turns a catalogued empirical pattern into a testable geometric constraint on neutron-star spin periods.

/-- The bimodal ratio is strictly greater than 30 (sharply distinguishable
from a continuous distribution). -/
theorem bimodal_ratio_gt_thirty : 30 < bimodal_ratio := by
  unfold bimodal_ratio recycling_rung_shift
  -- phi^8 ≥ (1.61)^8 = ?
  have h_phi : 1.61 < phi := phi_gt_onePointSixOne
  have h_pow : (1.61 : ℝ)^8 ≤ phi^8 := by
    have h_pos : (0 : ℝ) ≤ 1.61 := by norm_num
    exact pow_le_pow_left₀ h_pos (le_of_lt h_phi) 8
  -- (1.61)^8 = 45.39... > 30
  have h_compute : (30 : ℝ) < (1.61 : ℝ)^8 := by norm_num
  linarith

/-- The bimodal ratio is strictly less than `φ^9` (the next rung). -/
theorem bimodal_ratio_lt_phi_nine : bimodal_ratio < phi ^ 9 := by
  unfold bimodal_ratio recycling_rung_shift
  have h_phi : 1 < phi := one_lt_phi
  exact pow_lt_pow_right₀ h_phi (by norm_num : 8 < 9)

theorem gap_size_eq : gap_size = 7 := by
  unfold gap_size recycling_rung_shift
  norm_num

/-- **PULSAR PERIOD FROM RECOGNITION-RUNG: ONE-STATEMENT THEOREM
(Track AS7).**

The pulsar-period bimodal distribution is forced by the canonical
8-tick recycling shift between two φ-ladder families: normal
pulsars at base period `τ_neutron · φ^k`, millisecond pulsars at
base period `τ_neutron · φ^(k-8)`. The bimodal ratio
`P_normal_median / P_ms_median = φ^8 > 30` is sharply distinguishable
from a continuous distribution. The structural gap of 7 unstable
intermediate rungs explains the empirical "pulsar period gap" at
`P ≈ 30–100 ms`. -/
theorem pulsar_period_one_statement :
    -- (1) Both families have median rung 4.
    (normal_median_rung = 4 ∧ ms_median_rung = 4) ∧
    -- (2) Recycling shift is 8 ticks.
    recycling_rung_shift = 8 ∧
    -- (3) Bimodal ratio strictly > 30.
    30 < bimodal_ratio ∧
    -- (4) Structural gap of 7 unstable rungs.
    gap_size = 7 :=
  ⟨⟨rfl, rfl⟩, rfl, bimodal_ratio_gt_thirty, gap_size_eq⟩

What this page does not claim

The empirical bimodality of pulsar periods is not proved; the module only exposes a structural gap. The value of the neutron recognition time is not derived here. The recycling shift is taken as a definition, not derived from accretion physics.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Astrophysics/PulsarPeriodFromRung.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: