modulus
plain-language theorem explainer
modulus supplies the cyclic carrier size m(k) = k + 2 for the k-th periodic realization of the free LogicNat orbit under Universal Forcing. Workers constructing finite models cite it to fix the period of the carrier interpretation. The definition is introduced directly as k + 2 with no further computation.
Claim. For each natural number $k$, define the modulus by $m(k) := k + 2$.
background
The module develops periodic finite-cyclic realizations for Universal Forcing. The internal orbit remains the free LogicNat while the carrier interpretation is made periodic; this shows that Universal Forcing does not require every realization to embed arithmetic faithfully into the carrier. The modulus fixes the size of the finite cyclic carrier that appears in the definitions of cycStep and modularInterpret.
proof idea
Direct definition: modulus k := k + 2.
why it matters
Referenced by 22 downstream declarations, including modularInterpret (which maps LogicNat into Fin(modulus k)), modular_interpret_periodic, modularInterpret_step, and coupledOperatorInner in CoupledRecognitionCores. It supplies the carrier-size parameter that enables the modular arithmetic invariant and the demonstration of periodic realizations without full arithmetic embedding. It fills the carrier-size role inside the modular logic realization for the forcing framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.