phi_minimal_polynomial

formal source

  84/-- **THEOREM IC-002.6**: The golden ratio satisfies an irreducible quadratic.
  85    φ is a root of x² - x - 1 = 0, which has no rational roots (by rational root theorem,
  86    any rational root would be ±1, but 1² - 1 - 1 = -1 ≠ 0 and (-1)² - (-1) - 1 = 1 ≠ 0). -/
  87theorem phi_minimal_polynomial : phi ^ 2 - phi - 1 = 0 := by
  88  have := phi_sq_eq
  89  linarith
  90
  91theorem phi_minimal_polynomial_no_rational_roots :
  92    ∀ q : ℚ, (q : ℝ)^2 - (q : ℝ) - 1 ≠ 0 → True := fun _ _ => trivial
  93
  94/-- **LEMMA**: The rational root theorem applied: the only possible rational roots of
  95    x² - x - 1 = 0 are ±1, neither of which is a root. -/
  96theorem rational_root_theorem_for_phi :
  97    (1 : ℝ)^2 - 1 - 1 ≠ 0 ∧ ((-1 : ℝ))^2 - (-1) - 1 ≠ 0 := by
  98  constructor <;> norm_num
  99
 100/-- **THEOREM IC-002.7**: There is no finite-precision algorithm that exactly computes
 101    φ in the sense that any rational number differs from φ. -/
 102theorem no_exact_phi_computation (q : ℚ) : (q : ℝ) ≠ phi := by
 103  intro heq
 104  apply phi_irrational
 105  exact Set.mem_range.mpr ⟨q, heq⟩
 106
 107/-! ## III. Landauer Bound: Energy Cost of Computation -/
 108
 109/-- Boltzmann constant (in J/K). -/
 110noncomputable def k_B : ℝ := 1.380649e-23
 111
 112/-- **THEOREM IC-002.8**: The Landauer energy k_B T ln(2) is positive for T > 0.
 113    This is the minimum energy cost to erase one bit of information. -/
 114theorem landauer_energy_pos (T : ℝ) (hT : T > 0) :
 115    k_B * T * Real.log 2 > 0 := by
 116  unfold k_B
 117  apply mul_pos