modulus_pos
The theorem proves that the cyclic carrier size for any natural number k is strictly positive. Researchers constructing finite periodic realizations of Universal Forcing cite it to ensure Fin types are well-defined. The proof is a one-line wrapper that unfolds the definition of modulus as k + 2 and applies the omega tactic.
claimFor every natural number $k$, the cyclic carrier size $m(k) := k + 2$ satisfies $0 < m(k)$.
background
The module supplies a periodic finite-cyclic realization for Universal Forcing. The free LogicNat orbit is interpreted periodically on a finite carrier whose size is given by the modulus function. This shows that Universal Forcing permits realizations whose carrier does not embed arithmetic faithfully.
proof idea
The proof is a one-line wrapper. It unfolds the definition of modulus to k + 2, then invokes the omega tactic to discharge the strict inequality for any natural number k.
why it matters in Recognition Science
The result is required by the downstream definitions of cycStep, modularInterpret, and modularRealization, which construct the finite cyclic carrier and its successor and interpretation maps. It fills the basic positivity obligation in the modular realization path, consistent with the module's demonstration that periodic carriers suffice for the forcing framework.
scope and limits
- Does not establish any upper bound on the carrier size.
- Does not relate the modulus to the J-cost or phi-ladder.
- Does not address infinite or non-periodic carriers.
- Does not connect to the eight-tick octave or spatial dimension D = 3.
Lean usage
example (k : ℕ) : Fin (modulus k) := ⟨0, modulus_pos k⟩formal statement (Lean)
34theorem modulus_pos (k : ℕ) : 0 < modulus k := by
proof body
Term-mode proof.
35 unfold modulus
36 omega
37