pith. machine review for the scientific record. sign in
def definition def or abbrev high

modulus

show as:
view Lean formalization →

The modulus definition supplies the finite carrier size k + 2 for each modular realization indexed by k. Workers on periodic interpretations of Universal Forcing cite it when constructing cyclic carriers that keep the internal LogicNat orbit free. The definition is a direct arithmetic expression with no further reduction.

claimFor each natural number $k$, the cyclic carrier size of the $k$-th modular realization is $k + 2$.

background

The ModularLogicRealization module constructs periodic finite-cyclic realizations for Universal Forcing. The internal orbit stays the free LogicNat while the carrier interpretation is forced to be periodic; this shows Universal Forcing does not require every realization to embed arithmetic faithfully into the carrier. The modulus function fixes the size of that finite cyclic carrier and is used to type the Fin carrier in cycStep and modularInterpret.

proof idea

Direct definition returning k + 2.

why it matters in Recognition Science

This definition supports the family of modular realizations that demonstrate flexibility of Universal Forcing. It is referenced by modularInterpret, cycStep, modularRealization and downstream coupled-operator constructions in CoupledRecognitionCores. It illustrates that carrier periodicity can be imposed independently of the free LogicNat orbit.

scope and limits

formal statement (Lean)

  32def modulus (k : ℕ) : ℕ := k + 2

proof body

Definition body.

  33

used by (22)

From the project-wide theorem graph. These declarations reference this one in their body.