ArithmeticOf
plain-language theorem explainer
ArithmeticOf packages a Peano algebra together with its initiality witness for any given LogicRealization. Researchers on universal forcing and categorical realizations cite this structure to extract realization-independent arithmetic. The definition is a direct structure bundling the PeanoObject carrier with zero and successor against the IsInitial lift and uniqueness data.
Claim. For a logic realization $R$, an arithmetic object consists of a Peano algebra $P$ (a type equipped with a zero element and a successor map) together with initiality data: a homomorphism from $P$ to every other Peano algebra that is unique among all such homomorphisms.
background
PeanoObject is a structure with a carrier type, a zero element, and a successor map; it models the basic algebra of natural numbers. IsInitial equips such an object with a lift producing a homomorphism to any target Peano algebra and a uniqueness clause on those homomorphisms. LogicRealization supplies an abstract carrier, zero element, and comparison cost from which arithmetic is extracted. The module setting states that initiality guarantees the arithmetic object is unique up to unique isomorphism, serving as the mechanism behind universal forcing.
proof idea
Direct structure definition that bundles the Peano algebra supplied by the realization with its initiality data; no tactics or reductions are applied.
why it matters
This structure is the central data type for arithmetic extraction. It is instantiated by the canonical and extracted definitions and used to establish equivalences such as categorical_arithmetic_invariant across realizations. It supplies the initial Peano algebra required by the forcing program, ensuring arithmetic content is invariant once identity and step data are given.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.