ratio_is_phi_power
plain-language theorem explainer
Under the φ-ladder hypothesis, the ratio of scales for any two elements is an integer power of φ. Researchers testing discrete hierarchies in masses or timescales would cite this to convert the ladder assumption into a concrete ratio prediction. The proof extracts the integer rungs for each element and subtracts them after clearing the nonzero base and φ factors.
Claim. Assuming the φ-ladder hypothesis for a type α, for any x, y in α with scale(y) ≠ 0 there exists an integer k such that scale(x)/scale(y) = φ^k.
background
The φ-ladder hypothesis asserts that privileged physical scales satisfy X = X₀ · φ^n for integer n. The class supplies a base scale, a scale extraction map, and the on_ladder predicate that every element lands on some integer rung of this ladder. The module treats the hypothesis as explicit rather than derived, generating empirical obligations such as the ratio condition proved here.
proof idea
Obtain the rung integers m and n for x and y via the on_ladder field. Set k to m minus n. Establish that the base is nonzero by contradiction with the given scale(y) ≠ 0 and zero_mul, then apply field_simp and zpow_sub₀ to reduce the ratio to φ^{m-n}.
why it matters
This discharges the second falsification criterion listed in the module documentation: under the hypothesis, no two privileged scales can have a ratio outside the φ-powers. It therefore supports the mass formula on the phi-ladder and the self-similar fixed point φ from the forcing chain. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.