modular_arithmetic_invariant
plain-language theorem explainer
The definition asserts that for any n>1 the Peano carrier extracted from the arithmetic of the modular realization of n is naturally equivalent to the Peano carrier extracted from the arithmetic of an arbitrary logic realization. Workers on the universal forcing program cite it to confirm that cyclic carriers preserve the forced initial arithmetic. The proof is a direct one-line application of the equivalence of initial Peano objects.
Claim. For any natural number $n>1$ and any logic realization $R$, the carrier of the Peano object in the arithmetic forced by the modular realization of $n$ is equivalent to the carrier of the Peano object in the arithmetic forced by $R$.
background
LogicRealization is the structure supplying a carrier type, a cost type with zero, a comparison map, and a zero element; each realization supplies its own topology or order through the propositions it carries. ArithmeticOf extracts from any such realization a Peano object together with a proof that the object is initial. The modular realization takes ZMod n as carrier with equality cost; its semantic orbit may close, yet the forced arithmetic remains the universal iteration object certified by that orbit. The key upstream lemma is equivOfInitial, which constructs the natural equivalence between the carriers of any two initial Peano objects.
proof idea
One-line wrapper that applies ArithmeticOf.equivOfInitial to the arithmetic objects of the modular realization of n and of the given R.
why it matters
The definition establishes invariance of the extracted arithmetic under modular realizations, confirming that different carriers (including cyclic ones) yield the same forced Peano structure. It is referenced by the modular_arithmetic_invariant declaration in ModularLogicRealization. The result supports the claim that the universal forcing program produces realization-independent arithmetic, consistent with the modular/cyclic setting described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.