zero_ne_succ
plain-language theorem explainer
zero_ne_succ establishes that the zero element of LogicNat is distinct from the successor of any n. Workers constructing arithmetic carriers from the Law of Logic cite it as the first derived Peano axiom. The proof assumes equality and applies case analysis on the constructors of LogicNat, which yields an immediate contradiction.
Claim. In the inductive type LogicNat generated by the Law of Logic, with zero as the identity constructor and successor as the step constructor, zero is not equal to succ n for any n.
background
LogicNat is the inductive type whose constructors are identity (the zero-cost element, the multiplicative identity in the orbit under the generator) and step (one further iteration of the generator). This mirrors the smallest subset of positive reals closed under multiplication by γ and containing 1. The successor function is defined by succ n := step n, while zero is the identity constructor.
proof idea
The proof is a one-line tactic wrapper. It introduces the assumption zero = succ n and applies case analysis on the equality. The distinct constructors identity and step produce an immediate contradiction.
why it matters
This supplies the base case for induction in every downstream LogicRealization, including canonicalCategoricalRealization, logicNatNNO, boolRealization, and positiveRatio_faithful. It realizes Peano P1 as a theorem inside the derivation of arithmetic from the functional equation, feeding the constructions that later reach the eight-tick octave and spatial dimension D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.