modulus_pos
plain-language theorem explainer
modulus_pos asserts that the cyclic carrier size for any natural k is strictly positive. Constructions of finite periodic carriers in modular realizations of Universal Forcing cite it to justify well-defined Fin types. The proof is a one-line term wrapper that unfolds the definition and reduces the inequality by arithmetic.
Claim. For every natural number $k$, the cyclic carrier size $m(k) := k + 2$ satisfies $m(k) > 0$.
background
The module supplies a periodic finite-cyclic realization for Universal Forcing. The free orbit LogicNat is retained internally while the carrier interpretation is made periodic on a finite cycle; this shows that Universal Forcing does not require every realization to embed arithmetic faithfully into the carrier. The central definition is modulus k := k + 2, the size of the cyclic carrier for the k-th realization.
proof idea
One-line wrapper that unfolds modulus and applies the omega tactic to the resulting arithmetic goal.
why it matters
The result is invoked by cycStep, modularInterpret, modularInterpret_zero and modularRealization to construct the finite cyclic Law-of-Logic realization and its modular arithmetic invariant. It thereby supports the module's demonstration that periodic carriers suffice for the forcing chain without faithful arithmetic embedding into the carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.