zero_lt_succ
plain-language theorem explainer
Proves that the zero element is strictly less than the successor of any element in the naturals forced by the law of logic. Researchers deriving arithmetic from the Recognition Science functional equation would cite this when establishing basic order facts. The proof is a term construction that pairs the witness n with a rewriting step invoking the zero_add lemma to satisfy the order definition.
Claim. $0 < succ(n)$ for every $n$ in the inductive naturals whose constructors are the identity (zero-cost element) and the step (generator iteration), the smallest subset of positive reals closed under multiplication by the generator and containing 1.
background
LogicNat is the inductive type with constructors identity (the zero-cost multiplicative identity in the orbit) and step (one more iteration of the generator). This mirrors the orbit {1, γ, γ², γ³, ...} as the smallest subset of ℝ₊ closed under multiplication by γ and containing 1, as stated in its definition. The successor is one further application of the generator. The zero_add result states that zero plus any such number equals the number itself and is established by induction on the inductive structure. This declaration occurs inside the module that extracts arithmetic primitives directly from the law of logic viewed as a functional equation.
proof idea
The proof is a term-mode construction supplying the pair consisting of witness n together with a proof that zero plus succ n equals succ n. The equality is obtained by rewriting with the zero_add lemma, which matches the existential form required by the definition of the strict order on these naturals.
why it matters
The result is used in the structure of cycles inside the graded ledger algebra and in the definition of possibility spaces for modal configurations. It supplies a basic ordered-arithmetic fact in the derivation chain from the functional equation, supporting later steps toward the phi-ladder and the eight-tick octave in the forcing sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.