isInitial
plain-language theorem explainer
Any Lawvere natural-number object yields an initial Peano algebra by supplying a unique homomorphism to every other Peano algebra. Researchers tracing how the Law of Logic forces arithmetic would cite this when establishing that iteration structures satisfy the universal property of the naturals. The definition builds the lift directly from the recursor and obtains uniqueness from the recursor_unique clause together with function extensionality.
Claim. Let $(N, z, s)$ be a Lawvere natural-number object. Then the Peano algebra with carrier $N$, zero element $z$ and successor $s$ is initial: for every other Peano algebra $B$ there exists a unique homomorphism $N$ to $B$ that preserves zero and successor.
background
The module characterises the natural numbers forced by the Law of Logic via the Lawvere universal property. A triple $(N, z, s)$ is an IsNaturalNumberObject when, for every pointed endomap $(X, x, f)$, there exists a unique map $h : N$ to $X$ satisfying the zero and step equations; the recursor field packages this data while recursor_unique encodes the uniqueness clause. PeanoObject is simply a carrier equipped with a zero and a successor map. IsInitial then asserts that a given Peano algebra admits a unique homomorphism into every other Peano algebra. The upstream result LogicNat supplies the concrete orbit {identity, step, step step, …} that realises this structure.
proof idea
The definition constructs the lift homomorphism by feeding the target algebra's zero and step into the recursor of the given IsNaturalNumberObject. Zero and step preservation are immediate from the recursor_zero and recursor_step fields. The uniq clause applies recursor_unique to both candidate maps, obtains pointwise equality, and concludes by function extensionality.
why it matters
The construction converts the categorical NNO property into initiality inside the category of Peano algebras, which is the precise link needed to show that LogicNat with identity and step forms a natural-number object and that every realization preserves the forced arithmetic. It therefore occupies the step in the module that answers the objection that iteration counting was smuggled in rather than derived. The result sits inside the forcing chain that extracts arithmetic from the J-cost minimum and the recognition orbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.