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

down_generation_spacing

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)

 113theorem down_generation_spacing :
 114    r_down "s" - r_down "d" = 11 ∧ r_down "b" - r_down "d" = 17 := by

proof body

Term-mode proof.

 115  simp only [r_down, tau, Anchor.E_passive, Anchor.W, passive_field_edges,
 116             cube_edges, active_edges_per_tick, D, wallpaper_groups]
 117  omega
 118
 119/-! ## Mass Ratio Predictions (Sector-Internal)
 120
 121Within each sector, the mass ratio between generations is a pure phi-power:
 122  m(gen2) / m(gen1) = φ^{tau(1)} = φ^11 ≈ 199
 123  m(gen3) / m(gen1) = φ^{tau(2)} = φ^17 ≈ 3571
 124
 125These are the same ratios already verified for leptons. -/
 126

used by (2)

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

depends on (25)

Lean names referenced from this declaration's body.