modulus
plain-language theorem explainer
The modulus definition supplies the finite cyclic carrier size m(k) = k + 2 for the kth modular realization of the free LogicNat orbit. Researchers constructing periodic finite models for Universal Forcing cite this carrier size when demonstrating that forcing permits non-faithful arithmetic embeddings. The definition is a direct arithmetic assignment with no lemmas or reductions applied.
Claim. The cyclic carrier size for the kth modular realization is given by $m(k) := k + 2$.
background
ModularLogicRealization constructs periodic finite-cyclic realizations for Universal Forcing. The internal orbit remains the free LogicNat, while the carrier interpretation is made periodic on a finite set. This shows that Universal Forcing does not require every realization to embed arithmetic faithfully into the carrier.
proof idea
Direct definition that sets the carrier size to k + 2. No lemmas or tactics are applied.
why it matters
This definition is referenced by the cyclic step function, modular interpretation, periodicity theorems in the same module, and coupled recognition cores. It supplies the finite carrier sizes required for modular realizations, illustrating the periodic interpretation option within the Recognition framework. No open questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.