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

closure_forces_golden_equation

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 closure_forces_golden_equation (S : GeometricScaleSequence)
 114    (h_closed : S.isClosed) : S.ratio ^ 2 = S.ratio + 1 := by

proof body

Term-mode proof.

 115  -- Unfold the closure condition
 116  unfold GeometricScaleSequence.isClosed at h_closed
 117  unfold ledgerCompose at h_closed
 118  unfold GeometricScaleSequence.scale at h_closed
 119  -- h_closed : r^0 + r^1 = r^2
 120  -- This simplifies to: 1 + r = r^2
 121  simp only [pow_zero, pow_one] at h_closed
 122  -- Rearrange to r^2 = r + 1
 123  linarith
 124
 125/-- **THEOREM**: The unique positive closed ratio is φ.
 126
 127Combining with the previous theorem: the only positive ratio that
 128makes a geometric scale sequence closed is φ = (1 + √5)/2. -/

used by (3)

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

depends on (10)

Lean names referenced from this declaration's body.