lt_def
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove totality or well-foundedness of the order.
- Does not extend the relation to reals or continuous structures.
- Does not incorporate J-cost, defect distance, or the phi-ladder.
- Does not address mass formulas or the eight-tick octave.
formal statement (Lean)
334@[simp] theorem lt_def (n m : LogicNat) : n < m ↔ ∃ k, n + succ k = m := Iff.rfl
proof body
335