succ_injective
plain-language theorem explainer
The successor map on the natural numbers forced by the Law of Logic is injective. Constructions of arithmetic in categorical, discrete, modular, and ordered realizations cite this result to verify the Peano surface. The proof applies case analysis to the equality of two successors and reduces immediately to reflexivity.
Claim. Let $s$ denote the successor operation on the orbit generated by the logic law. Then $s$ is injective: $s(a)=s(b)$ entails $a=b$.
background
LogicNat is the inductive type with constructors identity (the zero-cost multiplicative identity) and step (one iteration of the generator), representing the smallest subset of positive reals closed under multiplication by the generator and containing 1. Successor is defined by applying the step constructor once. This setting derives arithmetic directly from the functional equation without positing Peano axioms as primitives.
proof idea
The term proof introduces the two arguments and the equality hypothesis, then cases on that hypothesis. The case reduces to reflexivity because the equality must arise from matching step constructors.
why it matters
This declaration supplies Peano axiom P2 for arithmetic extracted from logic. It feeds the canonical Peano surface theorem and supports realizations including categorical, discrete, modular, ordered, and physics ones. In the framework it enforces orbit injectivity required by the forcing chain from the functional equation to the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.