443theorem origin_question_resolved : 444 (PhiForcing.φ ^ 2 = PhiForcing.φ + 1) 445 ∧ (∀ r : ℝ, r > 0 → r ^ 2 = r + 1 → r = PhiForcing.φ) 446 ∧ (0 < LawOfExistence.J PhiForcing.φ ∧ LawOfExistence.J PhiForcing.φ < 1) 447 ∧ (∀ a b : ℤ, 448 Jcost (phi_ladder (a + b)) ≤ 449 2 * Jcost (phi_ladder a) + 2 * Jcost (phi_ladder b) + 450 2 * Jcost (phi_ladder a) * Jcost (phi_ladder b)) 451 ∧ (∀ n : ℤ, n ≠ 0 → 0 < Jcost (phi_ladder n)) := by
proof body
Term-mode proof.
452 exact ⟨ 453 PhiForcing.phi_equation, 454 fun r hr heq => PhiForcing.phi_forced r hr heq, 455 ⟨phi_cost_pos, phi_perturbation_bounded⟩, 456 ladder_cascade_bound, 457 fun n hn => phi_ladder_positive_cost hn 458 ⟩ 459 460/-- **Symmetry Breaking**: The ground state (rung 0, J = 0) is forced 461 off the trivial rung by T4 + T7. The broken-symmetry states 462 (rungs n ≠ 0, J > 0) are connected by the d'Alembert cascade. -/
depends on (19)
Lean names referenced from this declaration's body.