no_exact_phi_computation

formal source

  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
 118  apply mul_pos
 119  · norm_num
 120  · exact hT
 121  · exact Real.log_pos (by norm_num)
 122
 123/-- **THEOREM IC-002.9**: The Landauer energy grows linearly with temperature. -/
 124theorem landauer_scales_with_temp (T₁ T₂ : ℝ) (hT₁ : T₁ > 0) (hT₂ : T₂ > 0) (h : T₂ > T₁) :
 125    k_B * T₂ * Real.log 2 > k_B * T₁ * Real.log 2 := by
 126  unfold k_B
 127  have hlog : Real.log 2 > 0 := Real.log_pos (by norm_num)
 128  have hkB : (1.380649e-23 : ℝ) > 0 := by norm_num
 129  nlinarith
 130
 131/-- **THEOREM IC-002.10**: The Landauer bound is strictly greater than zero.
 132    No computation can be done for free (in thermodynamic equilibrium). -/