modular_arithmetic_invariant
plain-language theorem explainer
The definition shows that the Peano carrier extracted from any modular realization is equivalent to the Peano carrier extracted from an arbitrary LogicRealization. Researchers on Universal Forcing cite it to separate the forced arithmetic from the choice of periodic carrier. It is obtained by direct application of the equivalence between initial Peano objects.
Claim. Let $k$ be a natural number and let $R$ be any Law-of-Logic realization. Then the Peano carrier of the arithmetic object extracted from the modular realization with parameter $k$ is equivalent to the Peano carrier of the arithmetic object extracted from $R$.
background
LogicRealization supplies a carrier type, cost type, zero element, comparison map, and the structural laws required by the Universal Forcing program; the invariant target is the arithmetic object extracted from the identity and step data rather than the ambient carrier. ArithmeticOf packages a PeanoObject together with a proof that it is initial. modularRealization builds a finite cyclic realization whose carrier is Fin(modulus k) and whose cost is Nat. The module states that the internal orbit remains free while the carrier interpretation is periodic, demonstrating that Universal Forcing does not require every realization to embed arithmetic faithfully into its carrier. equivOfInitial supplies the natural equivalence between any two initial Peano objects.
proof idea
One-line wrapper that applies ArithmeticOf.equivOfInitial to the arithmetic objects of the modular realization and the given realization R.
why it matters
This definition supports the downstream claim that modular realizations carry the universal forced arithmetic. It fills the module's demonstration that periodic carriers suffice without faithful embedding of arithmetic. It touches the question of how different realizations relate to the forced arithmetic while preserving the extracted Peano structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.