pith. sign in
module module high

IndisputableMonolith.PhiSupport.Alternatives

show as:
view Lean formalization →

This module collects explicit counterexamples showing that common constants fail the phi selection criterion. Researchers tracing the uniqueness of the golden ratio through the Recognition Science forcing chain would cite these lemmas to rule out alternatives. Each sibling performs a direct algebraic check that the candidate's square does not equal the candidate plus one.

claimThe constants $\sqrt{2}$, $\sqrt{3}$, $\sqrt{5}$, $\pi$, and $e$ fail the equation $x^2 = x + 1$ with $x > 0$.

background

The module imports the RS time quantum $\tau_0 = 1$ tick from Constants and the phi selection criterion $\phi^2 = \phi + 1$, $\phi > 0$ from RecogSpec.PhiSelectionCore. Its sibling declarations supply concrete failures for each listed constant, using the same algebraic test that defines the selection rule.

proof idea

The module consists of separate lemmas, each a direct algebraic verification that the candidate constant violates the defining equation of the phi selection criterion.

why it matters in Recognition Science

These counterexamples support the forcing of phi as the unique self-similar fixed point at T6 by eliminating common alternatives. They feed the broader uniqueness argument in the Recognition Science chain, though no downstream uses are recorded in the current graph.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)