modular_arithmetic_invariant
Modular arithmetic invariant defines an equivalence showing that the Peano carrier extracted from the modular realization of any n greater than 1 matches the carrier from an arbitrary LogicRealization. Researchers tracing invariance in the universal forcing chain cite this to confirm that cyclic carriers preserve the same initial arithmetic object. The definition is a direct one-line wrapper applying equivOfInitial to the two arithmetic objects.
claimFor any natural number $n > 1$ and any LogicRealization $R$, the carrier of the Peano object in the arithmetic structure forced by the modular realization of $n$ is equivalent to the carrier of the Peano object in the arithmetic structure forced by $R$.
background
A LogicRealization supplies a carrier type, a cost type equipped with zero, a comparison map between carriers, and a distinguished zero element, together with the structural propositions required by the universal forcing program. ArithmeticOf extracts from any such realization a PeanoObject that is initial in the category of Peano objects. The modular realization takes the carrier to be ZMod n with equality cost, so that the semantic orbit may close inside the finite set while the forced iteration object remains universal.
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 in Recognition Science
The definition confirms that the arithmetic extracted from modular realizations is invariant and therefore interchangeable with the arithmetic from any other realization. It feeds the modular logic realization result that records the same invariance at the level of the full modular structure. Within the forcing chain this step shows that the initial Peano object is insensitive to the choice between infinite and finite cyclic carriers.
scope and limits
- Does not construct the explicit ZMod n carrier or its cost function.
- Does not address equivalence of cost structures or comparison maps.
- Does not extend the equivalence beyond initial Peano objects.
- Does not constrain the concrete value of n beyond the hypothesis 1 < n.
formal statement (Lean)
82noncomputable def modular_arithmetic_invariant (n : ℕ) [Fact (1 < n)]
83 (R : LogicRealization.{0, 0}) :
84 (arithmeticOf (modularRealization n)).peano.carrier
85 ≃ (arithmeticOf R).peano.carrier :=
proof body
Definition body.
86 ArithmeticOf.equivOfInitial (arithmeticOf (modularRealization n)) (arithmeticOf R)
87
88end ModularRealization
89end UniversalForcing
90end Foundation
91end IndisputableMonolith