pith. sign in
module module high

IndisputableMonolith.RecogSpec.PhiSelectionCore

show as:
view Lean formalization →

The module codifies the φ selection criterion as the equation φ² = φ + 1 with φ > 0. It supplies the definitional core that later results use to demonstrate uniqueness of the golden ratio. Researchers following the Recognition Science forcing chain cite it when grounding the self-similar fixed point. The module contains no proofs and functions solely as a specification.

claimThe φ selection criterion requires that the positive real number φ satisfy the equation φ² = φ + 1.

background

Recognition Science selects the golden ratio through a self-similar fixed-point condition arising from the J-uniqueness property in the forcing chain. This module isolates the minimal algebraic requirement that any candidate must meet: the quadratic relation φ² = φ + 1 together with positivity. The criterion is the mathematical object imported by downstream modules that test alternative constants.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the selection criterion imported by the Alternatives module. That module then proves that e, π, √2, √3 and √5 all fail the equation, establishing that φ is the unique positive real satisfying x² = x + 1. The result directly addresses the numerology objection by showing the choice of φ is forced by the Recognition structure rather than arbitrary.

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)