lt_iff_succ_le
plain-language theorem explainer
The equivalence relating strict order on logic-forced naturals to the successor lying below the upper bound. Researchers deriving Peano structure from the functional equation would cite this when building transitivity and standard embeddings. The proof is a bidirectional constructor that rewrites each direction via the two successor-addition commutation lemmas.
Claim. For elements $n, m$ of the logic-forced natural numbers, $n < m$ holds if and only if the successor of $n$ satisfies successor$(n) ≤ m$.
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), mirroring the smallest subset of positive reals closed under multiplication by γ and containing 1. Successor is the single application of the step constructor. The module derives arithmetic operations and order as theorems from the Law of Logic rather than positing them, importing Mathlib and the functional-equation foundation. Upstream commutation results are the theorems stating n + succ m = succ (n + m) and succ n + m = succ (n + m).
proof idea
Constructor splits the biconditional into two implications. The forward direction destructures the witness k for n < m, rewrites the equality n + succ k = m first by succ_add then by the inverse of add_succ to obtain succ n + k = m. The reverse direction performs the symmetric rewrites, applying add_succ followed by the inverse of succ_add to recover the strict inequality witness.
why it matters
The lemma supplies the order relation needed for the transitivity theorem on strict inequality and for the order-embedding theorem that compares LogicNat to standard natural numbers. It completes one link in the chain that realizes Peano axioms as theorems inside the Recognition Science foundation, supporting consistent ordering on the phi-ladder. No open scaffolding questions are addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.