one_lt_modulus
plain-language theorem explainer
The theorem shows that the cyclic carrier size for any modular realization is strictly greater than 1. Researchers constructing finite periodic models of logic in Recognition Science cite it to guarantee that Fin types for carriers are well-formed with at least two elements. The proof is a one-line wrapper that unfolds the modulus definition and applies arithmetic simplification.
Claim. For every natural number $k$, the cyclic carrier size satisfies $1 < k + 2$.
background
The module supplies a periodic finite-cyclic realization of Universal Forcing. The internal orbit stays free as LogicNat while the carrier interpretation is made periodic; this demonstrates that Universal Forcing need not embed arithmetic faithfully into every carrier. The central definition is modulus(k) := k + 2, which fixes the size of the finite cyclic carrier Fin(modulus k). Upstream carrier definitions in the engineering modules set frequencies to 5 phi Hz but are not invoked by this inequality.
proof idea
The proof is a one-line wrapper. It unfolds the definition of modulus to obtain the arithmetic statement 1 < k + 2 and then applies the omega tactic to discharge the inequality.
why it matters
The result is invoked by modularInterpret_step and modularRealization to ensure the Fin carrier type is valid. It fills a foundational step in the periodic finite-cyclic realization path for Universal Forcing, consistent with the framework's allowance for non-faithful arithmetic embeddings. No open scaffolding remains at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.