toNat_le
plain-language theorem explainer
The equivalence between the partial order on LogicNat and the standard order on natural numbers via the iteration-counting map toNat. Order-embedding arguments in the Recognition framework cite this to transfer inequalities between the logic-derived naturals and ordinary arithmetic. The proof splits into two directions: one uses the definition of ≤ via addition of a witness and applies toNat_add with omega; the other constructs the witness using fromNat on the difference and invokes round-trip lemmas to recover equality.
Claim. For all $a, b$ in the inductive type LogicNat, $a ≤ b$ if and only if toNat$(a) ≤$ toNat$(b)$, where toNat sends the identity element to 0 and each step to the successor in $ℕ$.
background
LogicNat is defined inductively with two constructors: identity, representing the zero-cost multiplicative identity, and step, which iterates the generator. This structure encodes the orbit {1, γ, γ², ...} as the smallest subset closed under multiplication by γ starting from 1. The map toNat extracts the iteration count: identity maps to 0, step n to succ(toNat n). Its inverse fromNat builds the corresponding LogicNat from a natural number. This theorem is part of the recovery of Peano arithmetic from the functional equation, relying on the equivalence equivNat : LogicNat ≃ Nat and the compatibility toNat_add : toNat(a + b) = toNat a + toNat b.
proof idea
The proof uses constructor to split the biconditional. In the forward direction, it assumes a ≤ b witnessed by some k with a + k = b, applies congrArg toNat, rewrites with toNat_add, and concludes with omega. In the reverse direction, it introduces the witness fromNat(toNat b - toNat a), proves the addition recovers b using toNat_add, toNat_fromNat, and omega, then applies congrArg fromNat and the round-trip fromNat_toNat to obtain equality.
why it matters
This result completes the order recovery for LogicNat, feeding directly into embed_le_iff_of_one_lt which transfers the order through the embedding when γ > 1, and into toNat_lt for strict inequalities. It also supports ordered_interpret_le_iff in the realization module. Within the framework, it realizes the Peano order as part of the arithmetic extracted from the Law of Logic, enabling the phi-ladder and mass formulas downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.