order_arithmetic_invariant
plain-language theorem explainer
The definition shows that the arithmetic object extracted from the ordered realization on the integers has a Peano carrier canonically equivalent to the Peano carrier of the arithmetic object extracted from any Law-of-Logic realization R. Researchers following the universal forcing chain would cite it to establish invariance of the forced arithmetic across realizations. The definition is a direct one-line application of the equivalence between initial Peano objects.
Claim. Let $R$ be any Law-of-Logic realization. There is a canonical equivalence between the carrier of the Peano object in the arithmetic structure forced by the ordered realization and the carrier of the Peano object in the arithmetic structure forced by $R$.
background
The module defines an order-theoretic realization on the integers using equality cost and unit step. This is a lightweight realization whose forced arithmetic is carried by the certified internal orbit while the carrier is the standard embedding of LogicNat into the integers. A Law-of-Logic realization supplies a carrier type, a cost type with zero, a comparison function, and a zero element, together with the structural laws required by the forcing program. The arithmetic object of a realization is the structure containing a Peano object together with the proof that this Peano object is initial.
proof idea
One-line wrapper that applies equivOfInitial to the arithmetic objects of the ordered realization and of R.
why it matters
The definition confirms that the ordered realization carries the universal forced arithmetic. It supports invariance of the extracted arithmetic under choice of realization inside the Universal Forcing program. No downstream uses are recorded, so the declaration closes a local invariance step rather than feeding a larger parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.