toNat_le
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish order properties for operations beyond addition.
- Does not extend to real-valued embeddings without additional assumptions on γ.
- Does not prove uniqueness of the order or antisymmetry separately.
- Does not address non-standard models or other interpretations.
formal statement (Lean)
452theorem toNat_le (a b : LogicNat) : a ≤ b ↔ toNat a ≤ toNat b := by
proof body
Tactic-mode proof.
453 constructor
454 · rintro ⟨k, hk⟩
455 have := congrArg toNat hk
456 rw [toNat_add] at this
457 omega
458 · intro h
459 refine ⟨fromNat (toNat b - toNat a), ?_⟩
460 have hroundtrip : ∀ n : LogicNat, fromNat (toNat n) = n := fromNat_toNat
461 -- toNat (a + fromNat (toNat b - toNat a)) = toNat a + (toNat b - toNat a) = toNat b
462 have hadd : toNat (a + fromNat (toNat b - toNat a)) = toNat b := by
463 rw [toNat_add, toNat_fromNat]
464 omega
465 -- Apply equivNat injectivity
466 have : a + fromNat (toNat b - toNat a) = b := by
467 have h1 := congrArg fromNat hadd
468 rw [hroundtrip, hroundtrip] at h1
469 exact h1
470 exact this
471