pith. machine review for the scientific record. sign in
structure definition def or abbrev

PulsarPeriodFromRungCert

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)

 205structure PulsarPeriodFromRungCert where
 206  normal_median_rung_eq : normal_median_rung = 4
 207  ms_median_rung_eq : ms_median_rung = 4
 208  recycling_rung_shift_eq : recycling_rung_shift = 8
 209  period_geometric :
 210    ∀ P_base k, period_at_rung P_base (k + 1) =
 211      period_at_rung P_base k * phi
 212  bimodal_ratio_pos : 0 < bimodal_ratio
 213  bimodal_ratio_gt_thirty : 30 < bimodal_ratio
 214  bimodal_ratio_lt_phi_nine : bimodal_ratio < phi ^ 9
 215  gap_size_eq : gap_size = 7
 216
 217/-- The master certificate is inhabited. -/

used by (1)

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

depends on (18)

Lean names referenced from this declaration's body.