simultaneous_differs_from_sequential

formal source

 179/-- **Key structural fact**: Sequential single-bond descent (take v = n₁, then v = n₂,
 180    etc.) converges toward the arithmetic mean, while simultaneous descent converges
 181    to the geometric mean. The two differ for distinct neighbors. -/
 182theorem simultaneous_differs_from_sequential {n₁ n₂ : ℝ}
 183    (hn₁ : 0 < n₁) (hn₂ : 0 < n₂) (hne : n₁ ≠ n₂) :
 184    Real.sqrt (n₁ * n₂) ≠ arithmeticMean n₁ n₂ :=
 185  geometric_ne_arithmetic hn₁ hn₂ hne
 186
 187/-! ## §5. Derived identities -/
 188
 189/-- **F1.5.1**: Recognition Composition Law (RCL) -/
 190theorem rcl_identity {x y : ℝ} (hx : x ≠ 0) (hy : y ≠ 0) :
 191    Jcost (x * y) + Jcost (x / y) = 2 * Jcost x * Jcost y + 2 * Jcost x + 2 * Jcost y := by
 192  have hxy : x * y ≠ 0 := mul_ne_zero hx hy
 193  have hxdy : x / y ≠ 0 := div_ne_zero hx hy
 194  simp only [Jcost]
 195  field_simp [hx, hy, hxy]
 196  ring
 197
 198/-- **F1.5.2**: The golden ratio -/
 199noncomputable def phi : ℝ := (1 + Real.sqrt 5) / 2
 200
 201/-- phi satisfies φ² = φ + 1 -/
 202theorem phi_sq : phi ^ 2 = phi + 1 := by
 203  unfold phi
 204  have h5 : (0 : ℝ) ≤ 5 := by norm_num
 205  have hsq : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt h5
 206  nlinarith [hsq]
 207
 208/-- phi > 0 -/
 209theorem phi_pos : 0 < phi := by
 210  unfold phi
 211  have : 0 < Real.sqrt 5 := Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 5)
 212  linarith