PhiLadderFalsifier
plain-language theorem explainer
PhiLadderFalsifier packages an observed real scale, a base, a tolerance, and a proof that the scale lies outside every phi-rung generated by the base. Experimentalists checking the Recognition Science claim that privileged scales follow integer powers of phi would cite this record to document a counterexample. The definition is a plain four-field structure whose last field negates the nearPhiRung predicate supplied by sibling definitions.
Claim. A falsification witness consists of an observed real number $x$, a base real number $b$, a tolerance real number $t > 0$, and a proof that $x$ is not within distance $t$ of any value $b · φ^n$ for integer $n$.
background
The module states that the φ-ladder hypothesis is an explicit claim, not a definitional truth: privileged physical scales satisfy $X = X_0 · φ^n$ for integer $n$. Falsification criteria include any privileged scale that fails to land near a φ-rung. Sibling definitions supply phi, computeRung, and nearPhiRung; upstream constants such as rung and scale provide the concrete ladder construction used to evaluate the negated predicate.
proof idea
The declaration is a record definition. Its four fields are declared directly; the final field simply asserts the negation of nearPhiRung applied to the first three fields. No tactics or lemmas are invoked.
why it matters
The structure is the witness type consumed by the downstream theorem falsifier_falsifies, which concludes that the phi-ladder hypothesis fails whenever such a record exists. It implements the first falsification criterion listed in the module documentation. Within the Recognition Science framework it supplies the concrete test object for the phi-ladder hypothesis that follows from the T6 self-similar fixed point and the mass formula on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.