logicNatLift
plain-language theorem explainer
The definition constructs the canonical homomorphism from the Peano algebra carried by LogicNat into an arbitrary Peano algebra B via the primitive recursive fold. Algebraists working on initial objects in the category of Peano algebras cite it when establishing uniqueness up to unique isomorphism for the arithmetic extracted from a logic realization. The construction sets the carrier map to the fold and confirms the homomorphism axioms by reflexivity on the base and step clauses.
Claim. For any Peano algebra $B$, the map $f$ from the carrier of the logic-natural Peano algebra to the carrier of $B$ defined by $f(0)=0_B$ and $f(s(n))=s_B(f(n))$ is a homomorphism of Peano algebras.
background
A Peano algebra is a carrier type equipped with a zero element and a successor map. A homomorphism between two Peano algebras is a function that sends zero to zero and commutes with successor. The logic-natural Peano algebra has carrier LogicNat together with its zero and successor. The fold into a target algebra B sends the identity element to B's zero and recurses by applying B's successor at each step.
proof idea
This is a direct definition that installs logicNatFold as the underlying function. Zero preservation holds by reflexivity on the base case. Successor preservation holds by reflexivity on the inductive clause of the fold.
why it matters
The definition supplies the lift required to prove that the logic-natural Peano algebra is initial. It is invoked directly in the statement that LogicNat is initial among Peano algebras and in the subsequent realization fold and lift constructions. This realizes the initiality mechanism that extracts arithmetic from any law-of-logic realization, the step that underpins universal forcing in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.