modular_arithmetic_invariant
The modular realization of a law-of-logic structure yields an arithmetic object whose Peano carrier is canonically equivalent to the Peano carrier of any other realization. Workers on universal forcing cite this to establish that the forced arithmetic is independent of the concrete carrier chosen. The definition is a direct one-line application of the equivalence between initial Peano objects.
claimFor any natural number $k$ and any logic realization $R$, the Peano carrier of the arithmetic object induced by the modular realization with parameter $k$ is equivalent to the Peano carrier of the arithmetic object induced by $R$.
background
The module defines periodic finite-cyclic realizations for the universal forcing program. A logic realization supplies a carrier type, cost type, zero element, comparison map, and the structural propositions required by the forcing chain. The arithmetic object extracted from any realization is a Peano object equipped with an initiality witness. The modular realization uses the finite cyclic carrier Fin(modulus k) with natural-number costs and the finCost comparison. Upstream, equivOfInitial supplies the canonical bijection between the carriers of any two initial Peano objects.
proof idea
One-line wrapper that applies equivOfInitial to the arithmetic objects extracted from the modular realization and from R.
why it matters in Recognition Science
This definition shows that the arithmetic forced by universal forcing remains the same when the realization is replaced by the modular finite-cyclic case. It directly supports the module claim that universal forcing does not require every realization to embed arithmetic faithfully into its carrier. The result is referenced by the corresponding statement in UniversalForcing.ModularRealization.
scope and limits
- Does not assert that the finite cyclic carrier itself contains an embedded copy of the naturals.
- Does not construct an explicit computational isomorphism beyond the initiality lift.
- Does not impose extra constraints on the modulus k beyond those already present in modularRealization.
formal statement (Lean)
100noncomputable def modular_arithmetic_invariant (k : ℕ) (R : LogicRealization.{0, 0}) :
101 (UniversalForcing.arithmeticOf (modularRealization k)).peano.carrier
102 ≃ (UniversalForcing.arithmeticOf R).peano.carrier :=
proof body
Definition body.
103 ArithmeticOf.equivOfInitial
104 (UniversalForcing.arithmeticOf (modularRealization k))
105 (UniversalForcing.arithmeticOf R)
106
107/-- The modular interpretation is periodic on the carrier. -/