categorical_arithmetic_invariant
plain-language theorem explainer
The definition states that the Peano carrier extracted from the canonical categorical realization of a Law-of-Logic structure is naturally equivalent to the Peano carrier from any other realization R. Researchers working on the Universal Forcing program would cite it to confirm arithmetic stability across categorical and discrete models. The proof is a direct one-line application of the equivalence between any two initial Peano objects.
Claim. For any Law-of-Logic realization $R$, the carrier of the initial Peano object induced by the canonical categorical realization is equivalent to the carrier of the initial Peano object induced by $R$.
background
LogicRealization supplies a carrier type, a cost type with zero, a comparison map, and a zero element; these data encode the structural laws needed to extract arithmetic. ArithmeticOf packages the resulting Peano object together with a proof that it is initial in the category of Peano objects. The module packages the natural-number object idea in the same initial-Peano-algebra language used by ArithmeticOf, providing a categorical/Lawvere-style hook for the Universal Forcing program without rebuilding category theory.
proof idea
One-line wrapper that applies equivOfInitial to the ArithmeticOf instance built from canonicalCategoricalRealization and the ArithmeticOf instance built from R.
why it matters
The definition records that arithmetic extracted from any Law-of-Logic realization is independent of the concrete carrier chosen. It supports the invariance claim in the Universal Forcing program and the categorical realization hook described in the module documentation. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.