toNat_lt
plain-language theorem explainer
The strict order on LogicNat is equivalent to the standard order on natural numbers under the iteration-count map. Researchers recovering Peano structure from the Law of Logic cite this to transfer inequalities into concrete arithmetic. The proof reduces the strict case to the non-strict equivalence via successor rewriting and finishes with the omega tactic.
Claim. Let $a, b$ be elements of the logic-forced naturals (inductive type with identity and step constructors). Then $a < b$ if and only if the iteration count of $a$ is strictly less than the iteration count of $b$.
background
LogicNat is the inductive type whose constructors are identity (the zero-cost multiplicative identity in the orbit) and step (one further iteration of the generator). The forward map toNat reads off the iteration count: identity maps to 0 and step n maps to the successor of toNat n. The module ArithmeticFromLogic recovers abstract Peano arithmetic from the Law of Logic; it imports LogicAsFunctionalEquation and builds order, addition, and embedding on top of this type. Upstream results include the non-strict order equivalence toNat_le and the rewriting lemma lt_iff_succ_le that expresses strict inequality as successor less-or-equal.
proof idea
Tactic-mode proof. Rewrite the goal with lt_iff_succ_le and toNat_le to obtain a statement about successors. For each direction, introduce the hypothesis, rewrite with toNat_succ, and apply the omega tactic to discharge the resulting arithmetic comparison on natural numbers.
why it matters
This equivalence supplies the order transfer used by embed_lt_iff_of_one_lt to obtain strict monotonicity of the real embedding when the generator exceeds 1, and by prime_logic_is_positive_ledger_state to certify that recovered primes are positive ledger states. It closes the recovery of linear order on the abstract naturals forced by the Law of Logic, enabling downstream transfer of Nat properties into the Recognition framework's arithmetic layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.