nat_succ_iterate_zero
plain-language theorem explainer
Iterating natural-number successor k times from 0 recovers k exactly. Anyone identifying a countable minimal orbit with ℕ cites this. The proof is ordinary induction on k, using the iterate-successor rewrite and the inductive hypothesis.
Claim. For every natural number $k$, applying the successor map $k$ times to zero returns $k$: $(\mathrm{succ}^{[k]})(0) = k$.
background
The module UnifiedForcingChain aims to force the full T-1 through T8 ladder from the cost foundation (Recognition Composition Law, normalization, calibration), so that logic, discreteness, the ledger, unique J, φ, the eight-tick period, and D = 3 appear as inevitabilities rather than assumptions.
In that setting one needs a countable state space carrying a minimal orbit. The natural numbers with ordinary successor supply the canonical discrete clock: start at 0 and step. The doc-comment states the elementary fact used here: iterating successor from zero returns the iteration index.
Upstream name collisions in the graph (LogicNat successor, reachability successor, ledger-closure predicates) are not used in the body. The argument is pure Mathlib iteration on Nat.succ.
proof idea
Introduce k and induct on it.
- Zero case:
simpreduces zero iterates of successor at 0 to 0. - Successor case: rewrite with
Function.iterate_succ_apply'so one more iterate is successor of the k-fold iterate; thensimpwith the inductive hypothesis closes(succ^{[k+1]})(0) = k+1.
No Recognition-specific lemmas appear; it is a short tactic induction.
why it matters
The sole recorded consumer is canonicalMinimalOrbitFramework_realization: the canonical closed observable framework on the countable state space ℕ realizes its target sequence definitionally along the orbit from 0. That realization needs the orbit point after k steps to be definitionally the index k; this theorem supplies that equality.
Inside the forcing chain, the minimal orbit is the discrete skeleton on which recognition cost, hierarchy minimality, and later T6–T8 timing (φ self-similarity, eight-tick octave) are staged. Without aligning iterate-count with the natural label, the “definitional along the orbit” claim would not type-check as an equality of sequences.
It is scaffolding arithmetic for the complete inevitability chain, not a physics law by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.