pith. machine review for the scientific record. sign in
theorem proved term proof

recycling_rung_shift_eq

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 109theorem recycling_rung_shift_eq : recycling_rung_shift = 8 := rfl

proof body

Term-mode proof.

 110
 111/-! ## §2. Closed-form periods on the φ-ladder
 112
 113Each pulsar family has a base period `P_base`; the period at rung
 114`k` is `P_base · φ^k`. The normal family has base `τ_neutron`; the
 115ms family has base `τ_neutron / φ^8` (the recycling shift).
 116-/
 117
 118/-- Period at rung `k` given a base period. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (12)

Lean names referenced from this declaration's body.