succ_ne_zero
plain-language theorem explainer
Every successor in the LogicNat structure differs from zero, giving the contrapositive form of Peano's first axiom inside the derivation of arithmetic from the Law of Logic. Researchers verifying discrete orbit constructions in Recognition Science cite the result when confirming that zero and positive elements remain distinct. The proof is a direct case split on the equality hypothesis that immediately exposes the disjoint constructors of the inductive type.
Claim. For every $n$ in the inductive type whose constructors are the zero-cost identity and the generator step, the successor of $n$ is unequal to the identity element.
background
The module ArithmeticFromLogic extracts Peano arithmetic as theorems from the functional equation that Recognition Science uses to force natural numbers. LogicNat is the inductive type with constructors identity (the multiplicative identity at zero cost) and step (one further application of the generator), realizing the smallest subset of positive reals closed under multiplication by the generator and containing 1. The definition succ simply wraps the step constructor. This theorem is listed among the Peano axioms realized as theorems rather than axioms.
proof idea
The term proof introduces the assumption that succ n equals zero and immediately performs case analysis on that equality. The two constructors of LogicNat are disjoint, so the case where a step term equals the identity term is impossible and the goal is discharged.
why it matters
The result supplies the first Peano primitive required by the faithful arithmetic interpretation in OrderedLogicRealization. It sits inside the chain that derives arithmetic from the Law of Logic before the forcing steps that produce J-uniqueness, the phi fixed point, and the eight-tick octave. The declaration closes a basic non-collapse property that later lemmas rely on when embedding the arithmetic structure into physical models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.