pith. sign in
module module high

IndisputableMonolith.PhiSupport

show as:
view Lean formalization →

PhiSupport supplies the algebraic identity φ² = φ + 1 together with the fixed-point and ordering properties of the golden ratio. Mass and mixing derivations in the Recognition framework (T9–T12) cite these relations when constructing the phi-ladder. The module consists of three short declarations that verify the quadratic equation by direct substitution, confirm the fixed point, and establish 1 < φ.

claimThe golden ratio satisfies $\phi^2 = \phi + 1$ with $\phi > 1$ and the self-similar fixed-point relation under the J-cost.

background

Recognition Science forces φ as the unique positive fixed point of the self-similar map in the T0–T8 chain (T6). The module imports the RS time quantum τ₀ = 1 tick from Constants and supplies the minimal algebraic support needed by later physics modules. Its doc-comment records the classical verification: φ = (1 + √5)/2 implies φ² = (3 + √5)/2 = φ + 1.

proof idea

This is a definition module; the three sibling declarations perform direct algebraic substitution for the quadratic identity, a one-line fixed-point check, and a numeric inequality proof.

why it matters in Recognition Science

The module feeds the core definitions for electron mass (T9), lepton generations (T10), CKM geometry (T11), and quark masses (T12). It supplies the phi-ladder foundation required by the mass formula yardstick · φ^(rung − 8 + gap(Z)) and the eight-tick octave structure.

scope and limits

used by (9)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (3)