ordered_arithmetic_invariant
plain-language theorem explainer
Ordered arithmetic extracted from any logic realization is equivalent to the natural-number version. Researchers working on universal forcing or ordered models cite this invariance to establish carrier independence. The definition reduces directly to the equivalence of initial Peano objects in the arithmetic construction.
Claim. Let $R$ be any logic realization. The Peano carrier of the arithmetic object induced by the natural-number ordered realization is naturally equivalent to the Peano carrier of the arithmetic object induced by $R$.
background
A logic realization supplies a carrier type, a cost type with zero, a comparison map, and a zero element, together with the structural laws required by universal forcing. The arithmetic object associated to a realization consists of a Peano object plus a proof that the object is initial in the category of Peano objects. The natural-number ordered realization is the concrete instance whose carrier is the type of natural numbers and whose comparison cost is the natural-number cost function.
proof idea
One-line wrapper that applies the equivalence of initial Peano objects to the arithmetic structures of the natural ordered realization and the given realization.
why it matters
The definition records that ordered arithmetic is invariant across realizations, confirming model independence inside the ordered fragment of the forcing program. It completes the ordered case begun by the natural-number realization and the arithmetic extraction, supporting the broader claim that arithmetic structure survives changes of realization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.