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

mass_from_phi_ladder

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)

 125theorem mass_from_phi_ladder :
 126    1 < phi := by linarith [Constants.phi_gt_onePointFive]

proof body

Term-mode proof.

 127
 128/-! ## Why Not 2 or 4 Generations? -/
 129
 130/-- Could we have 2 generations? No - D=3 requires 3 dimensions.
 131    Could we have 4? No - 8 = 2³ gives exactly 3 bits.
 132    
 133    **Proved**: 8 = 2^3 and the number of bits in a byte is 3 (log₂ 8 = 3). -/

depends on (13)

Lean names referenced from this declaration's body.