computation_limits_structure
plain-language theorem explainer
The theorem asserts that the irrationality of φ supplies the structural constraint on computation limits in Recognition Science. Researchers modeling information bounds or Church-Turing limits in physics would cite this when linking algebraic irrationality to simulation requirements. The proof is a one-line wrapper that applies the established irrationality of the golden ratio.
Claim. The proposition that the golden ratio φ is irrational holds, where this proposition encodes the constraint that φ-based states cannot be exactly represented by finite rational arithmetic.
background
The module IC-002 treats computation limits as arising from temporal discreteness (minimum time per operation is one tick), irrational constants, Landauer erasure, and the Bremermann bound. The sibling definition computation_limits_from_ledger is the Prop Irrational phi, presented as the core structural constraint on RS computation. The upstream theorem phi_irrational states that φ equals Real.goldenRatio and is irrational because √5 is irrational.
proof idea
The proof is a one-line wrapper that applies the theorem phi_irrational to discharge computation_limits_from_ledger.
why it matters
This result carries the irrationality fact into the computation limits structure and is invoked by has_computation_limits_structure (ChurchTuringPhysicsStructure) and physics_complexity_structure (PhysicsComplexityStructure). It supplies the IC-002.5 step that no rational approximation equals φ exactly, reinforcing the framework claim that irrational constants force transcendental precision in RS dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.