theorem
proved
alpha_seed_computable
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Meta.ConstructiveNote on GitHub at line 269.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
266/-! ## RS Constants Are Computable -/
267
268/-- The geometric seed 4π·11 is computable. -/
269theorem alpha_seed_computable : Computable (4 * Real.pi * 11) := by
270 have h1 : Computable ((4 : ℕ) : ℝ) := inferInstance
271 have h2 : Computable Real.pi := pi_computable
272 have h3 : Computable ((11 : ℕ) : ℝ) := inferInstance
273 simp only [Nat.cast_ofNat] at h1 h3
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