succ
plain-language theorem explainer
The succ definition equips LogicNat with its successor by direct application of the step constructor. Researchers building reachability predicates or inductive arguments in the Recognition framework cite it when constructing ballP or ReachN over the forced naturals. The implementation is a one-line abbreviation that inherits the inductive structure without proof obligations.
Claim. Let LogicNat be the inductive type generated by the constructors identity (zero-cost element) and step (one iteration of the generator). The successor operation is the function succ : LogicNat → LogicNat defined by succ(n) := step(n).
background
LogicNat is the type of natural numbers forced by the Law of Logic, with identity as the zero-cost multiplicative identity and step as the generator that produces the orbit {1, γ, γ², …} under multiplication by γ. The ArithmeticFromLogic module derives Peano primitives as theorems from this inductive structure rather than positing them axiomatically. The definition depends on the LogicNat inductive type itself together with compatibility utilities such as iterate.
proof idea
The definition is a one-line wrapper that applies the step constructor of LogicNat to the input.
why it matters
This supplies the successor primitive used by downstream results including ballP and reach_mem_ballP in Causality.BallP together with ReachN in Causality.Basic, which support cone-bound cardinality arguments. It completes the Peano successor in the foundation, enabling inductive derivations that connect to the forcing chain T0–T8 and the Recognition Composition Law. It touches no open scaffolding questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Models learn to reason only when time cues demand it
"tick turns that contain only a <time> tag—marks silent time-advances"