pith. sign in
module module high

IndisputableMonolith.RRF.Hypotheses.PhiLadder

show as:
view Lean formalization →

The module defines the golden ratio φ = (1 + √5)/2 together with scaling functions and ladder predicates for the RRF phi-ladder. Researchers deriving constants or testing the tau-gate hypothesis reference these objects to construct mass and energy scales. The module supplies direct definitions plus elementary lemmas establishing positivity, ordering, and additivity properties.

claim$φ = (1 + √5)/2$, with auxiliary map $φScale : ℝ → ℝ$, predicate $OnPhiLadder : ℤ → Prop$, rung calculator $computeRung$, and explicit claim $PhiLadderHypothesis$.

background

This module opens the RRF Hypotheses section and introduces φ as the golden ratio. It records the standard algebraic definition, proves φ > 1 and φ > 0, defines the scaling operation φScale, and states the predicates OnPhiLadder and nearPhiRung together with the top-level claim PhiLadderHypothesis. The surrounding RRF framework treats φ as the self-similar fixed point that generates the ladder used for all subsequent constant derivations.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions feed the constant derivation chain φ → E_coh → τ₀ → c → ℏ → G → α⁻¹ in RRF.Foundation.Constants, the tau-gate hypothesis in TauGate, the umbrella hypotheses file, and the ultimate isomorphism theorem. They supply the initial mathematical object required by the φ-ladder theory.

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)