pith. sign in
module module high

IndisputableMonolith.RecogSpec.PhiSelectionCore

show as:
view Lean formalization →

The PhiSelectionCore module states the selection criterion φ² = φ + 1 with φ > 0. Modules testing alternative constants cite it to demonstrate uniqueness of φ. The module is purely definitional with no proofs or derivations.

claimThe selection criterion requires a positive real number φ satisfying the equation φ² = φ + 1.

background

This module belongs to the RecogSpec domain and introduces the φ selection criterion as the core condition φ² = φ + 1 with φ > 0. It operates in the setting of the Recognition Science forcing chain where T6 identifies φ as the self-similar fixed point. The criterion is the mathematical object referenced by sibling definitions such as PhiSelection.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The criterion supplies the equation used by the Alternatives module to show that e, π, √2, √3 and √5 fail the selection, proving φ is the only positive real satisfying x² = x + 1 and addressing the numerology objection.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (1)