pith. sign in
module module high

IndisputableMonolith.PhiSupport.Alternatives

show as:
view Lean formalization →

This module collects algebraic counterexamples showing that common constants fail the phi selection criterion. Researchers deriving constants from the recognition framework cite it to exclude non-phi candidates. The module structure consists of separate lemmas, each performing a direct substitution check against the defining equation.

claimThe constants $x = 2^{1/2}$, $x = 3^{1/2}$, $x = 5^{1/2}$, $x = 3.14159...$, and $x = 2.71828...$ each fail to satisfy $x^2 = x + 1$ with $x > 0$.

background

PhiSelectionCore supplies the selection criterion that any admissible constant must obey $x^2 = x + 1$ together with $x > 0$. Constants supplies the RS-native time quantum as the unit tick. The Alternatives module applies this criterion to a short list of familiar numbers that arise in physical modeling, showing each violates the fixed-point relation.

proof idea

The module contains no single proof but a collection of independent lemmas. Each lemma (sqrt2_fails_selection and its siblings) executes a direct algebraic comparison of the candidate's square against the candidate plus one, using either exact identities or decimal approximations to exhibit the mismatch.

why it matters in Recognition Science

The module supports the forcing of phi as the unique self-similar fixed point by eliminating common alternatives. It feeds the constant-selection step that precedes the eight-tick octave and the derivation of spatial dimension three. The explicit failures reinforce that only the golden ratio satisfies the J-cost and recognition-composition requirements.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)