nno_universal_uniqueness
plain-language theorem explainer
Uniqueness of maps out of LogicNat: any two functions from the forced naturals to an arbitrary type that agree on the base element and commute with the successor operation must be identical. Category theorists and foundation researchers cite it when confirming that recursive definitions on LogicNat are canonical. The argument applies functional extensionality to reduce to pointwise equality, then inducts on the LogicNat argument, matching the base case directly and propagating via the successor hypotheses.
Claim. Let $α$ be any type, $b ∈ α$, and $s : α → α$. Suppose $f, g : LogicNat → α$ satisfy $f(0) = b$, $f(n+1) = s(f(n))$ for all $n$, and likewise for $g$, where $0$ and $n+1$ are the identity and step constructors on LogicNat. Then $f = g$.
background
LogicNat is the inductive type with constructors identity (the zero-cost multiplicative identity) and step (one further application of the generator), the smallest subset of positive reals closed under multiplication by the generator and containing 1. The module CategoricalMathlib bridges the strict categorical realization on LogicNat to Mathlib's CategoryTheory API, proving that LogicNat carries the universal property of a natural number object in the category of types: unique recursion via the two commuting-square equations. This rests on the arithmetic-from-logic construction in which the Peano axioms are theorems of the inductive structure.
proof idea
The tactic script first invokes funext to obtain pointwise equality for arbitrary n : LogicNat. It then performs induction on n. The identity case rewrites both functions to the shared base element using the zero hypotheses. The step case applies the successor hypotheses to both sides and invokes the induction hypothesis to equate the predecessors.
why it matters
Together with nno_universal_existence this result completes the NNO universal property for LogicNat and is packaged directly into categoricalMathlibCert_holds. It supplies the uniqueness half of the bridge to Mathlib's Nat.rec via transport along equivNat, confirming the algebraic content of an NNO in Type. In the Recognition framework it anchors the arithmetic layer derived from the law of logic and the forcing chain from primitive distinction onward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.