phi_minimal_polynomial
The golden ratio satisfies the quadratic equation φ² - φ - 1 = 0. Researchers modeling computation limits in Recognition Science cite this to show that φ-based states require infinite precision and cannot be simulated exactly with finite rational arithmetic. The proof is a one-line wrapper that imports the identity φ² = φ + 1 and rearranges it by linear arithmetic.
claimThe golden ratio φ satisfies the equation φ² - φ - 1 = 0.
background
Module IC-002 derives fundamental computation limits from temporal discreteness, irrational constants, and thermodynamic costs. One source is that φ is irrational, so φ-based states cannot be represented exactly with finite rational arithmetic. The upstream lemma phi_sq_eq states the key identity φ² = φ + 1, obtained from the definition of φ as (1 + √5)/2 and verified by algebraic simplification in both Constants and PhiLadderLattice.
proof idea
The term proof imports the lemma phi_sq_eq (φ² = φ + 1) and applies linarith to rearrange the equation into φ² - φ - 1 = 0.
why it matters in Recognition Science
This is theorem IC-002.6, confirming that φ is a root of the irreducible quadratic x² - x - 1 = 0. It supports the module's claim that irrational constants force transcendental precision in RS dynamics and underpins sibling results on the absence of exact φ computation. The result aligns with the framework's emphasis on φ as the self-similar fixed point whose irrationality bounds exact simulation.
scope and limits
- Does not prove irrationality of φ (separate theorem phi_not_rational).
- Does not derive the polynomial from the forcing chain or RCL.
- Does not address physical units or mass ladder applications.
- Does not establish minimality over the integers beyond the quadratic form.
formal statement (Lean)
87theorem phi_minimal_polynomial : phi ^ 2 - phi - 1 = 0 := by
proof body
Term-mode proof.
88 have := phi_sq_eq
89 linarith
90