zero_lt_succ
zero_lt_succ shows that the successor of any element in the logic-forced naturals is strictly positive. Workers deriving Peano structure from the functional equation cite it when establishing the order on LogicNat. The proof is a term-mode construction that supplies the witness n and reduces the defining equality with the zero_add lemma.
claimFor every $n$ in the logic-forced natural numbers, $0 < succ(n)$.
background
LogicNat is the inductive type whose identity constructor is the zero-cost element and whose step constructor generates the orbit under repeated multiplication by the generator gamma. The succ definition simply wraps the step constructor. The zero_add theorem states that adding zero on the left leaves any LogicNat element unchanged and is itself proved by induction on the structure of LogicNat.
proof idea
The declaration is a term proof that directly constructs the less-than witness. It supplies n as the difference and reduces the equality zero + succ n = succ n by rewriting with the zero_add lemma.
why it matters in Recognition Science
The result supplies a basic ordering fact required by the Cycle structure in LedgerAlgebra and the PossibilitySpace definition in Modal.Possibility. It belongs to the block that converts the inductive LogicNat into full Peano arithmetic as theorems rather than axioms, consistent with the Recognition Science program of deriving arithmetic from the single functional equation.
scope and limits
- Does not establish transitivity or totality of the order on LogicNat.
- Does not apply the inequality to any structure other than LogicNat.
- Does not derive further arithmetic identities such as addition or multiplication rules.
formal statement (Lean)
387theorem zero_lt_succ (n : LogicNat) : zero < succ n :=
proof body
Term-mode proof.
388 ⟨n, by show zero + succ n = succ n; rw [zero_add]⟩
389