lt_iff_succ_le
The equivalence between strict inequality and successor being at most the target holds for the logic-forced natural numbers. Researchers deriving Peano arithmetic inside Recognition Science cite this when building order from successor and addition. The proof is a direct biconditional via constructor that rewrites both directions with the successor-addition commutation lemmas to match the addition-based definitions of the relations.
claimLet $n, m$ belong to the logic-forced natural numbers. Then $n < m$ if and only if the successor of $n$ is at most $m$.
background
LogicNat is the inductive type whose constructors are 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. Addition on LogicNat is defined recursively, and the successor operation is the step constructor. The upstream lemmas add_succ and succ_add state that addition commutes with successor: $n +$ successor $m =$ successor $(n + m)$ and successor $n + m =$ successor $(n + m)$.
proof idea
The term-mode proof opens with constructor to split the biconditional. The forward direction assumes $n +$ successor $k = m$ for some $k$, then rewrites via succ_add followed by add_succ to obtain successor $n + k = m$. The reverse direction assumes successor $n + k = m$, rewrites via add_succ followed by succ_add to recover $n +$ successor $k = m$. Both directions invoke the two successor-addition theorems exactly once.
why it matters in Recognition Science
This fills a basic order axiom in the derivation of arithmetic from the Law of Logic. It is invoked directly by lt_trans to establish transitivity of < and by toNat_lt to embed the order into ordinary natural numbers. The result therefore supports the discrete structure required for the eight-tick octave and the subsequent forcing of three spatial dimensions in the Recognition Science chain.
scope and limits
- Does not define the less-than or less-than-or-equal relations.
- Does not treat multiplication or exponentiation on LogicNat.
- Does not extend the order to real numbers or continuous structures.
- Does not prove induction, well-ordering, or completeness properties.
Lean usage
rw [lt_iff_succ_le] at hab hbc ⊢formal statement (Lean)
356theorem lt_iff_succ_le {n m : LogicNat} : n < m ↔ succ n ≤ m := by
proof body
Term-mode proof.
357 constructor
358 · rintro ⟨k, hk⟩
359 refine ⟨k, ?_⟩
360 show succ n + k = m
361 rw [succ_add]
362 show succ (n + k) = m
363 rw [← add_succ]
364 -- need n + succ k = m, but we have n + succ k = m via hk; succ_add transforms
365 -- Wait: hk : n + succ k = m, and succ (n + k) = n + succ k by add_succ. So succ (n + k) = m.
366 exact hk
367 · rintro ⟨k, hk⟩
368 refine ⟨k, ?_⟩
369 show n + succ k = m
370 rw [add_succ]
371 show succ (n + k) = m
372 rw [← succ_add]
373 exact hk
374