realization_initial
plain-language theorem explainer
The definition shows that the Peano algebra generated by the identity-step orbit of any LogicRealization is initial in the category of Peano algebras. Researchers deriving arithmetic from logic realizations cite it to secure the universal property that enables unique forcing. The construction is a structure instance that supplies the lift map from realizationLift and obtains uniqueness by reduction to realizationLift_unique_fun.
Claim. For any realization $R$ of the law of logic, the Peano algebra $P$ generated by the identity-step orbit of $R$ is initial: there is a homomorphism from $P$ to every other Peano algebra $B$, and any two such homomorphisms are identical.
background
A Peano algebra is a carrier type equipped with a distinguished zero element and a successor map. The IsInitial structure on a Peano algebra consists of a lift operation that produces a homomorphism into any target Peano algebra together with a uniqueness clause asserting that all such homomorphisms coincide on the underlying functions. The module extracts arithmetic from an abstract realization of the law of logic; the central claim is that the forced arithmetic object is precisely the initial Peano algebra generated by the supplied identity and step data. This initiality supplies the uniqueness-up-to-isomorphism that underpins universal forcing.
proof idea
The definition constructs an IsInitial instance. The lift field is set directly to the realizationLift map. The uniq field is discharged by a single rewrite that replaces both candidate maps with the canonical lift via the realizationLift_unique_fun theorem.
why it matters
This declaration supplies the initiality data required by the extracted definition, which assembles the full arithmetic object from a LogicRealization. It thereby completes the initiality step in the extraction of arithmetic from logic realizations, as stated in the module documentation. The result sits inside the forcing chain that begins with LogicRealization and produces the initial Peano algebra; downstream structures rely on this uniqueness to obtain canonical arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.