pith. sign in
module module high

IndisputableMonolith.RRF.Hypotheses.PhiLadder

show as:
view Lean formalization →

The PhiLadder module supplies the golden ratio φ and ladder predicates that anchor all RRF hypotheses. Researchers deriving constants or testing rung predictions cite it as the shared mathematical base. It consists entirely of definitions and elementary properties with no deductive proofs.

claim$\phi = \frac{1 + \sqrt{5}}{2}$ together with the scaling map $\phi$Scale and the predicate OnPhiLadder that marks integer rungs on the discrete $\phi$-ladder.

background

The module sits inside the RRF hypotheses umbrella and supplies the self-similar fixed point required by the forcing chain. It defines $\phi$ as the positive root of $x^2 - x - 1 = 0$ and introduces phiScale for multiplication by integer powers of $\phi$, together with OnPhiLadder and computeRung for locating mass or energy values on the ladder. The setting is the explicit-hypothesis layer of Recognition Science, where $\phi$ is treated as the generator of all subsequent constants via gate identities.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Definitions here are imported by RRF.Foundation.Constants to realize the chain $\phi \to E_{\rm coh} \to \tau_0 o c \to \hbar \to G \to \alpha^{-1}$, by UltimateIsomorphism for the final universal-structure theorem, by the Hypotheses umbrella, and by TauGate for the tau-lepton rung prediction. The module therefore supplies the concrete mathematical object that turns the abstract forcing chain into testable numerical claims.

scope and limits

used by (4)

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

declarations in this module (15)