falsifier_falsifies
plain-language theorem explainer
Existence of a falsifier for the phi-ladder directly implies that no integer rung satisfies both the exact phi-power scaling and the tolerance bound on the computed rung. Physicists examining whether masses or periods follow phi multiples would cite the result to validate a falsifying observation. The proof reduces immediately to the not_near assertion packaged in the falsifier record.
Claim. Let $f$ be a structure with observed scale $o$, base $b$, tolerance $t$, and a proof that $o$ lies outside any phi-rung of $b$ within $t$. Then there is no integer $n$ such that $o = b · ϕ^n$ and $|computeRung(o, b) - n| ≤ t$.
background
The phi-ladder hypothesis states that privileged scales obey $X = X_0 · ϕ^n$ for integer $n$. The module treats this as an explicit, testable claim rather than a derived identity, with falsification triggered by any scale that misses the rungs. computeRung is the logarithmic measure $log(x/b)/log ϕ$ that locates a value relative to the base in phi-units. nearPhiRung is the predicate that some integer lies within the supplied tolerance of this computed value. The PhiLadderFalsifier structure bundles an observed value, its base, a tolerance, and the explicit proof that nearPhiRung fails.
proof idea
The proof assumes an integer $n$ together with the scaling equality and the tolerance witness. It then feeds the pair $(n, tolerance witness)$ directly into the not_near field of the supplied falsifier, producing an immediate contradiction.
why it matters
The result supplies the logical closure for the phi-ladder falsification criteria listed in the module: a concrete witness negates the scale condition. It therefore completes the explicit-hypothesis machinery that the RRF section uses to generate empirical obligations. No downstream theorems depend on it, confirming its role as a terminal rejection step rather than an intermediate lemma in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.