logicNatLift_unique_fun
plain-language theorem explainer
Any homomorphism from the Peano algebra carried by the logic-forced naturals to an arbitrary Peano algebra B agrees with the canonical recursive lift on underlying functions. Researchers establishing initiality of logic-forced arithmetic in Recognition Science cite this result to secure uniqueness up to unique isomorphism. The proof reduces the claim to pointwise equality via function extensionality, then applies structural induction on LogicNat while invoking the homomorphism preservation rules at each constructor.
Claim. Let $B$ be a Peano algebra and let $f$ be a homomorphism from the Peano algebra carried by the logic-forced naturals to $B$. Then the underlying function of $f$ equals the underlying function of the canonical recursive lift of the logic-forced naturals into $B$.
background
A Peano algebra is a carrier type equipped with a zero element and a step (successor) map. A homomorphism between two Peano algebras is a function that sends zero to zero and commutes with the step operation. LogicNat is the inductive type with an identity constructor (the zero-cost element) and a step constructor, serving as the arithmetic object forced directly by the Law of Logic.
proof idea
The proof opens with function extensionality to reduce the equality of functions to equality at each natural-number argument. It then performs induction on the LogicNat structure. The identity case applies the map-zero property of the given homomorphism. The step case rewrites via the map-step property, substitutes the inductive hypothesis, and closes by reflexivity.
why it matters
This theorem supplies the uniqueness direction required by the initiality statement for the logic-forced naturals. It is invoked inside the definition of logicNat_initial, which asserts that the logic-forced naturals form the initial Peano algebra. In the Recognition Science framework this initiality furnishes the uniqueness mechanism behind Universal Forcing, ensuring that arithmetic extracted from any Law-of-Logic realization is canonically determined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.