modular_arithmetic_invariant
plain-language theorem explainer
The modular realization of a logic law produces an arithmetic object whose Peano carrier is canonically equivalent to the Peano carrier of any other realization. Workers on finite cyclic models of the forced arithmetic would cite this invariance. The definition is a direct application of the equivalence between initial Peano objects.
Claim. For any natural number $n>1$ and any Law-of-Logic realization $R$, the Peano carrier of the arithmetic object extracted from the modular realization of $n$ is equivalent to the Peano carrier of the arithmetic object extracted from $R$.
background
The module treats modular realizations whose carrier is the cyclic group ZMod n with equality cost; the semantic orbit may close while the forced arithmetic remains the universal iteration object. A LogicRealization supplies a carrier, a cost type with zero, a comparison map, and a zero element together with the structural laws required by the Universal Forcing program. ArithmeticOf extracts from any such realization a PeanoObject together with the proof that it is initial. The upstream lemma ArithmeticOf.equivOfInitial states that any two initial Peano objects are equivalent via their universal lifting properties.
proof idea
One-line wrapper that applies ArithmeticOf.equivOfInitial to the arithmetic objects of the modular realization and the given R.
why it matters
This definition shows that the arithmetic forced by the modular realization is identical to that forced by any realization, confirming invariance of the extracted Peano object. It directly supports the modular_arithmetic_invariant declaration in ModularLogicRealization. The result sits inside the Universal Forcing module and therefore participates in the T0-T8 forcing chain by guaranteeing that finite modular carriers still yield the universal initial arithmetic object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.