log_phi_computable

formal source

 274  exact computable_mul (computable_mul h1 h2) h3
 275
 276/-- ln φ is computable. -/
 277theorem log_phi_computable : Computable (Real.log Constants.phi) := by
 278  have hphi : Computable Constants.phi := phi_computable
 279  have hpos : Constants.phi > 0 := Constants.phi_pos
 280  exact computable_log hphi hpos
 281
 282/-- The curvature term 103/(102π⁵) is computable. -/
 283theorem curvature_computable : Computable ((103 : ℝ) / (102 * Real.pi ^ 5)) := by
 284  have h103 : Computable ((103 : ℕ) : ℝ) := inferInstance
 285  have h102 : Computable ((102 : ℕ) : ℝ) := inferInstance
 286  simp only [Nat.cast_ofNat] at h103 h102
 287  have hpi : Computable Real.pi := pi_computable
 288  have hpi5 : Computable (Real.pi ^ 5) := computable_pow hpi 5
 289  have hdenom : Computable (102 * Real.pi ^ 5) := computable_mul h102 hpi5
 290  have hne : (102 : ℝ) * Real.pi ^ 5 ≠ 0 := by
 291    apply mul_ne_zero
 292    · norm_num
 293    · exact pow_ne_zero 5 Real.pi_ne_zero
 294  exact computable_div h103 hdenom hne
 295
 296/-! ## Summary -/
 297
 298/-- Gap 2 Resolution: Classical proofs ≠ non-computable outputs.
 299
 300    The "algorithmic" claim of RS is about the DERIVED CONSTANTS being computable,
 301    not about the proof machinery being constructive.
 302
 303    - Lean's `classical` tactic: OK (doesn't affect output values)
 304    - Lean's `noncomputable`: OK (Lean limitation, not Turing limitation)
 305    - Using Real.pi: OK (π is computable)
 306    - Using Classical.choice: OK (only in proofs, not in computed values)
 307