modular_arithmetic_invariant
plain-language theorem explainer
The definition states that the Peano carrier extracted from the arithmetic of any modular realization is equivalent to the Peano carrier extracted from the arithmetic of an arbitrary law-of-logic realization. Researchers on universal forcing cite it to establish that the forced arithmetic is independent of the concrete realization. The body is a direct one-line application of the equivalence between any two initial Peano objects.
Claim. For every natural number $k$ and every law-of-logic realization $R$, the carrier of the Peano object in the arithmetic forced by the finite-cyclic modular realization of parameter $k$ 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, a zero element, and the structural propositions required by the universal forcing program. ArithmeticOf packages a PeanoObject together with a proof that the object is initial in the category of Peano objects. The modularRealization constructs a concrete finite-cyclic realization whose carrier is Fin(modulus k) and whose step action is periodic. The module setting is that the internal orbit remains free (LogicNat) while the carrier interpretation is periodic, showing that universal forcing does not demand faithful arithmetic embedding in every realization.
proof idea
One-line wrapper that applies ArithmeticOf.equivOfInitial to the two ArithmeticOf instances obtained by wrapping modularRealization k and R.
why it matters
The definition supplies the invariance statement that feeds the parent theorem modular_arithmetic_invariant in UniversalForcing.ModularRealization, which asserts that the modular realization carries the universal forced arithmetic. It directly illustrates the module claim that universal forcing tolerates periodic carrier interpretations without losing the extracted arithmetic, consistent with the eight-tick octave and the separation between internal orbit and carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.