theorem
proved
rs_dynamics_approximable
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Information.ChurchTuringPhysicsStructure on GitHub at line 164.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
161/-- **THEOREM IC-003.13**: However, RS dynamics can be approximated to arbitrary
162 precision by rational arithmetic (since ℝ is the completion of ℚ).
163 This places approximate RS computations within Turing-machine computation. -/
164theorem rs_dynamics_approximable : ∀ ε > 0, ∃ q : ℚ, |phi - (q : ℝ)| < ε := by
165 intro ε hε
166 obtain ⟨q, hq1, hq2⟩ := exists_rat_btwn (show phi - ε < phi + ε by linarith)
167 exact ⟨q, by rw [abs_lt]; exact ⟨by linarith, by linarith⟩⟩
168
169/-! ## Summary Certificate -/
170
171def ic003_certificate : String :=
172 "═══════════════════════════════════════════════════════════\n" ++
173 " IC-003: CHURCH-TURING PHYSICS — STATUS: DERIVED\n" ++
174 "═══════════════════════════════════════════════════════════\n" ++
175 "✓ phase_space_finite: |Phase| = 8\n" ++
176 "✓ phase_functions_finite: |Phase→Phase| = 8^8\n" ++
177 "✓ ledger_state_space_finite: |DiscreteLedger| = 2^8\n" ++
178 "✓ church_turing_physics: Irrational φ (structural constraint)\n" ++
179 "✓ phase_space_bounded: phases ≤ 8 per tick\n" ++
180 "✓ tick_rate_bounded: τ₀ > 0 (no infinite rate)\n" ++
181 "✓ computation_takes_time: n steps ≥ n τ₀\n" ++
182 "✓ finite_function_computable: finite functions = lookup tables\n" ++
183 "✓ eight_tick_step_computable: step function = table\n" ++
184 "✓ rs_dynamics_beyond_rational: exact φ not Turing-computable\n" ++
185 "✓ rs_dynamics_approximable: approx φ is Turing-computable\n"
186
187end ChurchTuringPhysicsStructure
188end Information
189end IndisputableMonolith