rational_root_theorem_for_phi
plain-language theorem explainer
The lemma verifies that neither 1 nor -1 satisfies x² - x - 1 = 0. Researchers establishing irrationality of the golden ratio φ for computation bounds in Recognition Science cite it to rule out finite rational representations. The proof is a direct term-mode check that splits the conjunction and normalizes the two arithmetic evaluations.
Claim. $1^2 - 1 - 1 ≠ 0 ∧ (-1)^2 - (-1) - 1 ≠ 0$, showing that the only candidate rational roots of the minimal polynomial $x^2 - x - 1 = 0$ fail to satisfy the equation.
background
Module IC-002 derives fundamental computation limits in Recognition Science from temporal discreteness of the tick, irrational constants such as φ, and thermodynamic costs. The golden ratio φ arises as the self-similar fixed point satisfying φ² = φ + 1, equivalently the quadratic x² - x - 1 = 0. By the rational root theorem any rational root must be ±1, the divisors of the constant term.
proof idea
The term proof uses constructor to split the conjunction into two independent goals, then applies norm_num to evaluate the polynomial at the candidate points 1 and -1, confirming both results are nonzero.
why it matters
The result supports the claim in IC-002 that φ-based states cannot be exactly represented with finite rational arithmetic, thereby bounding exact simulation of RS dynamics. It aligns with the forcing chain step T6 that forces φ as the fixed point and with the phi-ladder lattice structures used in upstream results on Poisson summation and empirical programs. No direct downstream theorems are recorded, but the lemma feeds sibling declarations on phi irrationality and absence of exact phi computation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.