nearPhiRung
plain-language theorem explainer
The nearPhiRung definition states that a real scale x lies near a φ-rung for given base and tolerance precisely when the rung computed from that base differs from an integer by at most the tolerance. Researchers testing mass spectra or timescale hierarchies against the Recognition Science φ-ladder would cite this predicate to quantify empirical agreement with integer powers. The definition is supplied directly as an existential statement over the integers with no auxiliary lemmas.
Claim. A real number $x$ lies near a φ-rung relative to base $b$ and tolerance $ε$ if and only if there exists an integer $n$ such that the absolute difference between the rung of $x$ computed from $b$ and $n$ is at most $ε$.
background
The module formalizes the explicit φ-ladder hypothesis that privileged physical scales are organized by integer powers of φ. Module documentation states: 'Privileged physical scales satisfy: X = X₀ · φⁿ for integer n.' Examples include particle masses m = B · E_coh · φ^r and timescales τ = τ₀ · φ^n. This supplies a relaxed predicate allowing small deviations from exact integer rungs for measurement or approximation purposes.
proof idea
The definition is given directly by existential quantification over ℤ. It applies the sibling rung-computation function to obtain a real value and checks its distance to the nearest integer against the supplied tolerance bound. No lemmas from upstream results are invoked; the body is the complete specification.
why it matters
This predicate supports the explicit φ-ladder hypothesis and feeds the falsification witness structure PhiLadderFalsifier. It aligns with framework landmarks T6 (φ as self-similar fixed point) and the mass formula on the phi-ladder, while generating the prediction obligations listed in the module documentation. The declaration closes scaffolding for empirical checks of scale organization without deriving the ladder from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.