theorem proved term proof

`simulation_substrate_must_be_real`

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

formal statement (Lean)

 185theorem simulation_substrate_must_be_real :
 186    ∀ (q : ℚ), (q : ℝ) ≠ phi := no_exact_phi_computation

Term-mode proof.

 187
 188/-! ## Summary Certificate -/
 189

Lean names referenced from this declaration's body.

no_exact_phi_computation in IndisputableMonolith.Information.ComputationLimitsStructure decl_use