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

closed_ratio_is_phi

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)

 129theorem closed_ratio_is_phi (S : GeometricScaleSequence)
 130    (h_closed : S.isClosed) : S.ratio = phi := by

proof body

Tactic-mode proof.

 131  have h_eq := closure_forces_golden_equation S h_closed
 132  have h_pos := S.ratio_pos
 133  -- Both S.ratio and φ satisfy x² = x + 1
 134  -- For x > 0, this equation has unique solution φ
 135  have h_phi_eq : phi ^ 2 = phi + 1 := phi_sq_eq
 136  -- The difference (r - φ) satisfies: (r-φ)(r+φ) = r² - φ² = (r+1) - (φ+1) = r - φ
 137  -- So (r - φ)(r + φ - 1) = 0
 138  have h_factor : (S.ratio - phi) * (S.ratio + phi - 1) = 0 := by
 139    have := h_eq  -- r² = r + 1
 140    have := h_phi_eq  -- φ² = φ + 1
 141    ring_nf
 142    nlinarith [sq_nonneg S.ratio, sq_nonneg phi]
 143  -- Since r > 0 and φ > 1, we have r + φ - 1 > 0, so r - φ = 0
 144  rcases mul_eq_zero.mp h_factor with h_diff | h_sum
 145  · linarith
 146  · -- If r + φ - 1 = 0, then r = 1 - φ < 0, contradiction with r > 0
 147    have : S.ratio = 1 - phi := by linarith
 148    have : S.ratio < 0 := by
 149      have hphi : phi > 1 := one_lt_phi
 150      linarith
 151    linarith
 152
 153/-! ## Why Additive Composition? A J-Cost Argument -/
 154
 155/-- The J-cost of a scale ratio -/

used by (3)

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.