other_pairs_larger
plain-language theorem explainer
For positive integers a and b not both equal to 1, the larger value is at least 2. This arithmetic fact is cited inside the minimal-coefficients argument that forces uniform scaling in the HierarchyForcing module. The proof is a direct one-line application of the omega tactic to the negation hypothesis together with the two lower-bound assumptions.
Claim. Let $a,b$ be positive integers with $a,bgeq1$. If $(a,b)neq(1,1)$, then $max(a,b)geq2$.
background
The HierarchyForcing module closes Gap 2 by showing that a zero-parameter ledger forces hierarchical structure. Its central claim is that (1,1) is the unique positive-integer pair minimizing max(a,b); the present theorem supplies the complementary statement that every other pair has max at least 2. Upstream results include the scale function scale(k) = phi^k from LargeScaleStructureFromRS and the uniform distribution from ShannonEntropy, both used to embed the arithmetic fact into the larger derivation of self-similar ratios. The PrimitiveDistinction.from theorem supplies the bridge from seven axioms to the four structural conditions that make the arithmetic minimality physically meaningful.
proof idea
The proof is a one-line wrapper that invokes the omega tactic. Omega discharges the goal by linear integer arithmetic once the hypothesis that not both a and b equal 1 is combined with the two lower bounds 1 leq a and 1 leq b.
why it matters
The lemma completes the pure-arithmetic half of additive_composition_is_minimal inside the Gap 2 forcing chain. It thereby supports uniform_scaling_forced and the subsequent hierarchy_forced_gives_phi results that place the phi-ladder on the eight-tick octave. Because the statement is fully proved with no hypotheses, it closes the scaffolding for the minimal-coefficient step without leaving an open question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.