pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.PhiSupport

show as:
view Lean formalization →

PhiSupport establishes the golden ratio φ and its key algebraic properties for use throughout the Recognition Science mass and geometry derivations. Modules computing electron masses, lepton generations, CKM angles, and quark masses import it to access φ² = φ + 1 and related facts. The module performs direct algebraic checks using the closed-form expression of φ.

claimLet $φ = (1 + √5)/2$. Then $φ² = φ + 1$ and $φ > 1$.

background

The module introduces the golden ratio φ as the self-similar fixed point forced by the Recognition Composition Law and J-uniqueness (T5). It defines supporting facts for the phi-ladder used in mass formulas: yardstick * φ^(rung - 8 + gap(Z)). The upstream Constants module supplies the base time quantum τ₀ = 1 tick, which sets the RS-native units for all subsequent derivations.

proof idea

This is a definition module, no proofs. The three sibling declarations are established by substituting the closed-form expression for φ into the target identities and simplifying with real arithmetic.

why it matters in Recognition Science

PhiSupport supplies the algebraic foundation for the lepton mass derivations in T9 and T10, the CKM geometry in T11, and the quark masses in T12. It closes the T6 step of the forcing chain by providing the concrete properties of φ needed to compute the phi-ladder rungs and the alpha band bounds.

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)