phi_minimal_polynomial_no_rational_roots
plain-language theorem explainer
The declaration shows that the quadratic x² - x - 1 has no rational roots. Researchers on computation limits in Recognition Science cite it to establish that φ-based states cannot be represented exactly in finite rational arithmetic. The proof is a one-line term reduction to trivial once the rational root theorem excludes the candidates ±1.
Claim. For every rational number $q$, $q^2 - q - 1 = 0$ is false (i.e., the minimal polynomial of φ has no rational roots).
background
The module IC-002 derives computation limits from temporal discreteness (tick τ₀), irrational constants, and Landauer/Bremermann bounds. φ enters as the self-similar fixed point forced by the Recognition Composition Law and J-uniqueness (T5). The minimal polynomial x² - x - 1 is the characteristic equation whose irrational root φ cannot be captured by finite rational arithmetic. Upstream structures include PhiForcingDerived.of (J-cost on the φ-ladder) and EnergyConservationDomainCert.applied (energy conservation under time translation).
proof idea
Term-mode one-liner: fun _ _ => trivial. The accompanying lemma comment invokes the rational root theorem to restrict candidate rational roots to ±1; direct substitution shows neither satisfies the equation, discharging the claim without further tactics.
why it matters
It supplies the irrationality step required for the module's claim that exact RS dynamics demand transcendental precision. This sits inside the forcing chain (T5 J-uniqueness → T6 φ fixed point) and supports the broader IC-002 limits on computation rate and energy. It directly precedes sibling results such as no_exact_phi_computation and rational_root_theorem_for_phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.