toNat_le
plain-language theorem explainer
LogicNat carries the partial order recovered from the Law of Logic. The theorem states that this order on the orbit coincides exactly with the standard order on natural numbers under the toNat counting map. Researchers recovering arithmetic embeddings cite it when transferring inequalities through the equivalence. The tactic proof splits the biconditional and reduces both directions to Nat arithmetic via additivity and round-trip lemmas.
Claim. For $a, b$ in the inductive type LogicNat generated by the identity element and the successor step, $a$ is less than or equal to $b$ if and only if the iteration count of $a$ is less than or equal to the iteration count of $b$.
background
LogicNat is the inductive type with constructors identity (the zero-cost multiplicative identity) and step (one iteration of the generator), forming the smallest subset of positive reals closed under multiplication by the generator and containing 1. The module ArithmeticFromLogic recovers Peano arithmetic structures from the functional equation, including addition and the order relation. Upstream, equivNat witnesses the bijection LogicNat ≃ Nat with left and right inverses fromNat_toNat and toNat_fromNat; toNat_add shows that toNat preserves the addition operation defined on LogicNat.
proof idea
Tactic-mode proof that constructs the biconditional. Forward direction: from the witness k with a + k = b, apply congrArg toNat, rewrite by toNat_add, and close with omega. Reverse direction: construct the candidate witness fromNat (toNat b - toNat a), establish the addition identity via toNat_add and toNat_fromNat with omega, then apply congrArg fromNat together with the round-trip fromNat_toNat twice to obtain equality by injectivity.
why it matters
The result is invoked by embed_le_iff_of_one_lt to transfer the order through the embedding when the generator exceeds 1, by toNat_lt for the strict case, and by ordered_interpret_le_iff to equate the recovered order with the interpretation order. It completes the order-recovery step in the arithmetic-from-logic development, supporting the passage from the functional equation to ordered arithmetic structures used in later embedding and realization theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.