realization_initial
plain-language theorem explainer
The definition shows that for any LogicRealization R the associated Peano algebra is initial among all Peano algebras. Workers on the universal forcing chain cite it to guarantee that arithmetic is uniquely determined by the logic realization. The construction supplies the lift homomorphism directly from realizationLift and proves uniqueness by reduction to realizationLift_unique_fun.
Claim. For any LogicRealization $R$, the Peano algebra generated by the orbit of $R$ admits a unique homomorphism to every other Peano algebra $B$ (a type equipped with a zero element and successor map).
background
In the ArithmeticOf module arithmetic is extracted from an abstract Law-of-Logic realization. A PeanoObject is a structure consisting of a carrier type together with a zero element and a step map. The IsInitial structure on such an algebra supplies a lift homomorphism to any target Peano algebra together with a uniqueness clause asserting that any two lifts agree as functions.
proof idea
The definition is a one-line wrapper that sets the lift field to realizationLift R. The uniqueness clause is discharged by rewriting both candidate homomorphisms with realizationLift_unique_fun R B f and realizationLift_unique_fun R B g.
why it matters
This declaration supplies the initiality data required by the extracted definition, which packages the Peano algebra and its initiality into an ArithmeticOf structure. It realizes the module's key point that initial objects are unique up to unique isomorphism, providing the mechanism behind Universal Forcing. It connects directly to the forcing chain by ensuring the arithmetic extracted from any logic realization is canonical.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.