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

three_generations

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)

  84theorem three_generations : (List.length [Generation.first, Generation.second, Generation.third]) = 3 := rfl

proof body

Term-mode proof.

  85
  86/-! ## The 3 from 8 = 2³ Argument -/
  87
  88/-- The key insight: 8 = 2³ gives us 3 "independent directions" in tick-space.
  89    Each direction corresponds to one generation. -/

used by (7)

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

depends on (15)

Lean names referenced from this declaration's body.