 119  linarith
 120
 121/-- **THEOREM.** `1/φ` is the unique positive solution of `x + x² = 1`. -/
 122theorem phi_inv_unique {x : ℝ} (hx : 0 < x) (h : x + x ^ 2 = 1) :
 123    x = phi_inv := by
 124  -- Use strict monotonicity of f(x) = x + x² on (0, ∞).
 125  -- f(phi_inv) = 1 (by phi_inv_fibonacci_fixed_point) and f(x) = 1 (by h).
 126  -- So f(x) = f(phi_inv); strict monotonicity forces x = phi_inv.
 127  have h_phi : phi_inv + phi_inv ^ 2 = 1 := phi_inv_fibonacci_fixed_point
 128  have h_phi_pos : 0 < phi_inv := phi_inv_pos
 129  by_contra h_ne
 130  rcases lt_or_gt_of_ne h_ne with h_lt | h_gt
 131  · have := fib_fn_strict_mono hx h_phi_pos h_lt
 132    linarith
 133  · have := fib_fn_strict_mono h_phi_pos hx h_gt
 134    linarith
 135
 136/-! ## §4. Active and passive fractions -/
 137
 138/-- The passive fraction is `1 - phi_inv = 1/φ²`. -/
 139def passive_fraction : ℝ := 1 - phi_inv
 140
 141theorem passive_fraction_pos : 0 < passive_fraction := by
 142  unfold passive_fraction
 143  have := phi_inv_lt_one; linarith
 144
 145theorem passive_fraction_eq_phi_sq_inv :
 146    passive_fraction = phi_inv ^ 2 := by
 147  unfold passive_fraction
 148  have h := phi_inv_fibonacci_fixed_point
 149  linarith
 150
 151/-- **σ-CONSERVATION ON LEXICON.** Active + passive = 1. -/
 152theorem fractions_sum_to_one :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.