theorem proved term proof

`rs_dynamics_beyond_rational`

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

formal statement (Lean)

 158theorem rs_dynamics_beyond_rational : ¬ ∃ q : ℚ, (q : ℝ) = phi :=

proof body

Term-mode proof.

 159  fun ⟨q, hq⟩ => no_exact_phi_computation q hq
 160
 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. -/

used by (1)

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

ic003_certificate in IndisputableMonolith.Information.ChurchTuringPhysicsStructure decl_use

depends on (10)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
no_exact_phi_computation in IndisputableMonolith.Information.ComputationLimitsStructure decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use