realizationLift_unique_fun
plain-language theorem explainer
Any homomorphism from the Peano object of a logic realization to another Peano algebra agrees pointwise with the canonical lift on underlying functions. Researchers formalizing initial objects or universal forcing in algebraic logic cite this for uniqueness up to isomorphism. The proof applies function extensionality, builds an auxiliary homomorphism from LogicNat via orbit composition, invokes its uniqueness, and chains equalities through the orbit equivalence.
Claim. Let $R$ be a logic realization and $B$ a Peano algebra. For any homomorphism $f$ from the Peano algebra extracted from $R$'s orbit to $B$, the underlying map of $f$ equals the underlying map of the canonical lift from the extracted algebra to $B$.
background
The module extracts arithmetic from an abstract Law-of-Logic realization by treating its identity-step orbit as the carrier of a Peano algebra. A PeanoObject is a structure with a carrier type, a zero element, and a step map. A Hom between two PeanoObjects is a function that preserves zero and step. The local theoretical setting states that the forced arithmetic object is the initial Peano algebra generated by the realization's data; initial objects are unique up to unique isomorphism, which is the mechanism behind Universal Forcing.
proof idea
The tactic proof begins with funext to reduce to pointwise equality on orbit elements. It constructs an auxiliary homomorphism from LogicNat to $B$ by composing the given map with the inverse orbit equivalence, verifies zero and step preservation using the original map's properties and orbit axioms, then applies logicNatLift_unique_fun to obtain equality of the composed maps. A final calc rewrites the original map through the orbit equivalence to match the canonical lift.
why it matters
This result supplies the uniqueness clause for the IsInitial structure on the extracted Peano object, which is assembled in realization_initial. It completes the initiality argument that the module identifies as the core of Universal Forcing. In the Recognition framework it supports the emergence of arithmetic from logic realizations without additional axioms, consistent with the forcing chain that derives Peano structure from orbit data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.