leq_eq_false_iff
plain-language theorem explainer
Boolean order on finite distinction orbits is false exactly when the verifier Nat order is reversed: leq(a,b)=false iff b maps to a strictly smaller natural than a. Companion to the true-case agreement lemma. Cited by Euclidean-algorithm fuel proofs that need the complementary branch. Proof is a one-line rewrite through Boolean negation plus omega on Nat order.
Claim. For finite distinction-orbit positions $a,b$, the internal Boolean comparison $\mathrm{leq}(a,b)$ equals false if and only if the verifier natural number of $b$ is strictly less than that of $a$: $\mathrm{leq}(a,b)=\mathsf{false}\iff b^{\mathbb{N}}<a^{\mathbb{N}}$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with zero and succ, standing for K2.12 in the primitive recognition calculus. Its verifier map toNat sends zero to 0 and succ to Nat.succ, so orbit depth is read as an ordinary natural number.
The internal Boolean order leq is defined by structural recursion alone: leq(zero,_)=true, leq(succ _, zero)=false, and leq(succ a, succ b)=leq(a,b). It never consults Lean Nat comparison; it only peels successors.
The sibling theorem leq_eq_true_iff already equates the true branch with verifier inequality: leq(a,b)=true iff a.toNat ≤ b.toNat. Its proof is choice-free structural induction with axiom footprint [propext] (audit tier FORCED). The present result is the complementary false branch needed wherever case splits on the Boolean appear.
proof idea
Term-mode proof in two steps. First rewrite the goal using Bool.not_eq_true, turning leq a b = false into ¬(leq a b = true). Then apply leq_eq_true_iff to replace the Boolean equality by the Nat inequality a.toNat ≤ b.toNat. The resulting goal ¬(a.toNat ≤ b.toNat) is definitionally equivalent to b.toNat < a.toNat; omega closes it.
why it matters
Feeds the Euclidean layer on distinction orbits. Both divModFuel_toNat_aux and gcdFuel_toNat_aux case-split on the internal Boolean order while proving that fuel-bounded division/modulo and gcd on DistinctionNat agree with Nat./, Nat.%, and Nat.gcd after toNat. The false branch of those splits needs exactly this equivalence.
In the Recognition foundation stack this keeps arithmetic on δ-orbits choice-free and aligned with verifier Nat, so later integer/rational constructions (signed orbits, absolute difference, truncated subtraction) inherit a coherent order. It is not itself a forcing-chain landmark (T0–T8), but it is infrastructure for the arithmetic-from-logic path that those landmarks eventually use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.