computation_limits_from_ledger
Recognition Science computation limits rest on the irrationality of the golden ratio φ, which blocks exact finite rational encoding of phi-ladder states and forces transcendental arithmetic for RS constants. Modelers of discrete physical computation cite this when bounding simulation fidelity below Bremermann or Landauer thresholds. The declaration is a one-line definition that equates the limits proposition directly to Irrational φ.
claimThe proposition that the golden ratio φ (the unique positive self-similar fixed point satisfying J(φ) = φ with J(x) = (x + x^{-1})/2 - 1) is irrational.
background
The module IC-002 derives fundamental computation limits from temporal discreteness (the tick τ₀ as minimum time quantum), irrational constants such as φ, Landauer erasure energy, and the Bremermann bound E t ≥ ℏ/2. The declaration sets the computation limits proposition exactly equal to the statement that φ is irrational, so that φ-based states cannot be represented exactly in finite rational arithmetic. This sits downstream of the unified forcing chain (T0-T8) that forces φ via J-uniqueness and self-similarity at T6, and upstream of Church-Turing results that use it to bound the discrete ledger state space.
proof idea
The declaration is a direct abbreviation that sets computation_limits_from_ledger equal to Irrational φ. No tactics or lemmas are applied inside the definition itself; the supporting demonstration that φ is irrational is supplied by the sibling theorem phi_irrational via the rational root theorem on the minimal polynomial.
why it matters in Recognition Science
This supplies the core proposition IC-002.4 that anchors the computation limits structure and appears as the right-hand side in definitions such as church_turing_physics_from_ledger and physics_complexity_from_ledger. It enforces the requirement for transcendental arithmetic in RS simulations, consistent with the eight-tick octave and the irrationality constraint on the phi-ladder. The result closes one link from forcing axioms to physical computability bounds, leaving open the quantitative rate of rational approximation to φ in finite-precision models.
scope and limits
- Does not prove φ irrational; that requires the minimal polynomial argument in phi_irrational.
- Does not derive numerical bounds on computation rate or energy cost.
- Does not incorporate the specific value of the fundamental tick or Planck constants.
- Does not address whether approximate rational models suffice for observable physics.
Lean usage
def church_turing_physics_from_ledger : Prop := computation_limits_from_ledgerformal statement (Lean)
74def computation_limits_from_ledger : Prop := Irrational phi
proof body
Definition body.
75