theorem proved term proof

`phi_not_finitely_simulable`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 179theorem phi_not_finitely_simulable : ¬ ∃ q : ℚ, (q : ℝ) = phi :=

proof body

Term-mode proof.

 180  fun ⟨q, hq⟩ => no_exact_phi_computation q hq
 181
 182/-- **THEOREM IC-004.10**: Any universe that exactly reproduces RS dynamics
 183    (including the irrational φ) must operate on real numbers, not rationals.
 184    This constrains "simulation" substrates to real-number computers. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

ic004_certificate in IndisputableMonolith.Information.SimulationHypothesisStructure decl_use

depends on (2)

Lean names referenced from this declaration's body.

no_exact_phi_computation in IndisputableMonolith.Information.ComputationLimitsStructure decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use