computeRung
plain-language theorem explainer
The definition supplies the explicit formula for the exponent n in the relation x = base * phi^n. Researchers testing the phi-ladder hypothesis cite it when checking whether observed masses or timescales land near integer rungs, including in the tau-gate identity. The implementation is the direct change-of-base logarithm formula.
Claim. The rung index $r(x, b)$ of a scale $x$ relative to base $b$ is given by $r(x, b) = (ln(x/b)) / (ln phi)$.
background
The module states that the φ-ladder hypothesis organizes privileged physical scales by powers of φ, with examples including particle masses of the form m = B · E_coh · φ^r and timescales τ = τ₀ · φ^n. This supplies the computational step for the explicit hypothesis, which generates empirical prediction obligations rather than definitional truths. Upstream results include integer rung assignments in spectroscopy and fermion contexts together with the active edge count A used in integration-gap identities.
proof idea
The definition is a one-line wrapper that applies the change-of-base formula, dividing the natural logarithm of the ratio x/base by the natural logarithm of phi.
why it matters
This definition is required by the nearPhiRung predicate and the falsifier_falsifies theorem in the same module. It enables the TauGateIdentity structure (rung 19 for tau mass and gate time) and the TauGatePredictions that follow from it. It implements the computational core of the explicit φ-ladder hypothesis, allowing the Recognition Science framework to generate testable predictions against observed scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.