OnPhiLadder
plain-language theorem explainer
The OnPhiLadder structure encodes the predicate that a real number x equals a chosen base scaled by an integer power of phi. Workers on discrete scale hierarchies in Recognition Science cite it when testing whether masses or timescales occupy phi-rungs. The declaration is a bare structure definition whose two fields directly capture the hypothesis without further computation.
Claim. A real number $x$ lies on the phi-ladder relative to base $b$ when there exists an integer $n$ such that $x = b · ϕ^n$.
background
The module states the phi-ladder hypothesis explicitly: privileged physical scales satisfy X = X₀ · ϕⁿ for integer n. This is posited rather than derived and generates empirical obligations for particle masses m = B · E_coh · ϕ^r, timescales τ = τ₀ · ϕⁿ, and semantic amplitudes A = ϕ^level. Upstream structures supply instances, including NucleosynthesisTiers.of which places nuclear densities on phi-tiers as ρ_nuc ~ ϕ^{n_nuclear} × ρ_Planck, and PhiForcingDerived.of which calibrates the J-cost whose fixed point produces ϕ.
proof idea
The declaration is a structure definition. It introduces the integer field rung together with the equality field eq that enforces x = base * phi ^ rung. No lemmas or tactics are invoked; the structure itself serves as the interface for the hypothesis.
why it matters
This definition supplies the precise interface for the phi-ladder hypothesis in the RRF module. It bridges the forcing-chain step T5 (J-uniqueness yielding ϕ) to concrete predictions for D=3 physics and mass formulas, even though no direct downstream users are recorded. It keeps the hypothesis open to the falsification criteria listed in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.