PhiLadderHypothesis
plain-language theorem explainer
The φ-ladder hypothesis asserts that privileged physical scales satisfy X = B ⋅ φ^n for base B and integer n. Recognition Science researchers cite it when deriving mass ladders or timescale predictions from the self-similar fixed point. The declaration packages this as a Lean class with base, scale map, and on-ladder existence condition, serving as an explicit assumption rather than a derived result.
Claim. The φ-ladder hypothesis for a collection α of scales states that there exists a base scale B ∈ ℝ and a function scale : α → ℝ such that ∀ x ∈ α, ∃ n ∈ ℤ with scale(x) = B ⋅ φ^n.
background
In the RRF module the φ-ladder organizes physical quantities such as particle masses m = B ⋅ E_coh ⋅ φ^r and timescales τ = τ₀ ⋅ φ^n. This rests on the phi-forcing structure from PhiForcingDerived.of, which encodes J-cost, and on PrimitiveDistinction.from, which reduces seven axioms to four structural conditions plus three definitional facts. Upstream, NucleosynthesisTiers.of places nuclear densities on discrete φ-tiers while LargeScaleStructureFromRS.scale defines scale(k) := phi^k.
proof idea
The declaration is a Lean class that directly introduces three fields: a base real, a scale extractor α → ℝ, and the on-ladder predicate ∀ x, ∃ n, scale x = base ⋅ phi^n. No tactics or lemmas are applied; it is a pure definitional structure.
why it matters
This hypothesis supplies the assumption used by the downstream theorem ratio_is_phi_power, which shows that any two scales on the ladder differ by an integer power of φ. It supplies the explicit hypothesis slot required by the RRF framework for scale organization, connecting to the self-similar fixed point T6 and the eight-tick octave T7. It leaves open the empirical identification of which observed scales qualify as privileged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.