lt_def
plain-language theorem explainer
The strict order on LogicNat satisfies n precedes m precisely when m equals n plus the successor of some k. Researchers building arithmetic from the Recognition functional equation cite this equivalence to ground ordering without external axioms. The proof is a one-line reflexivity that matches the predicate definition directly.
Claim. For elements $n,m$ of the logic naturals, $n < m$ if and only if there exists $k$ such that $n + s(k) = m$, where $s$ denotes the successor operation.
background
LogicNat is the inductive type with identity (zero-cost multiplicative identity) and step (one generator iteration), mirroring the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by γ and containing 1. Successor is defined by applying the generator once more: succ n := step n. The module derives arithmetic from the Law of Logic by treating these constructors as primitives and proving Peano properties as theorems.
proof idea
One-line wrapper that applies reflexivity to the biconditional, confirming the stated equivalence coincides with the definition of the order predicate on LogicNat.
why it matters
This equivalence supplies the ordering infrastructure required for the arithmetic development inside the Recognition framework. It supports later proofs of addition properties and induction without positing number axioms, aligning with the forcing chain that extracts discrete structure from the functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.