logicNat_initial
plain-language theorem explainer
LogicNat supplies the initial Peano algebra among all Peano objects. A researcher working on categorical foundations or the natural-numbers object extracted from a logic realization would cite this to obtain the universal property for recursion. The definition is a one-line wrapper that installs the lift map and delegates uniqueness to the companion theorem on function agreement.
Claim. Let $P$ be the Peano algebra whose carrier is the type LogicNat, with zero element LogicNat.zero and successor LogicNat.succ. Then $P$ is initial: for every Peano algebra $B$ there exists a homomorphism $P$ to $B$, and any two such homomorphisms have identical underlying functions.
background
PeanoObject is the structure consisting of a carrier type together with a zero element and a successor map. IsInitial A is the data package that supplies, for any target PeanoObject B, a homomorphism from A to B together with the assertion that any two such homomorphisms agree on their underlying maps. The module ArithmeticOf extracts arithmetic from an abstract Law-of-Logic realization; its central claim is that the arithmetic object forced by the realization's identity-step orbit is precisely the initial Peano algebra generated by that data, which supplies the mechanism for Universal Forcing.
proof idea
The definition directly assigns the lift component to logicNatLift. Uniqueness is obtained by rewriting both candidate homomorphisms with the theorem logicNatLift_unique_fun, which establishes agreement by induction on the underlying LogicNat element.
why it matters
The declaration supplies the initiality witness used by canonical to produce the realization-independent arithmetic object and by logicNatNNO to realize the Lawvere natural-numbers object. It therefore closes the extraction step that turns a logic realization into the initial Peano algebra, directly supporting the universal-forcing step in the Recognition Science chain. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Absence of units makes linearly distributive categories coherent
"Categorical Coherence Theorem (Theorem 5.7): The free unitless linearly distributive category on a set is thin. Equivalently, every formal diagram in a unitless linearly distributive category commutes."