strictModularRealization
plain-language theorem explainer
strictModularRealization supplies a StrictLogicRealization whose carrier is the cyclic group ZMod n for each n greater than 1, with cost equal to the equality indicator and composition given by addition. Researchers constructing modular embeddings inside logic-based foundations cite it when they need a periodic carrier that still yields a free arithmetic orbit. The body is a direct record construction that wires zmodCost together with its self and symmetry lemmas into the required laws.
Claim. For each natural number $n>1$, the strict modular realization is the StrictLogicRealization whose carrier is the cyclic group $ZMod n$, whose cost function returns $0$ on equal elements and $1$ otherwise, whose composition operation is addition, whose identity element is $0$, and whose generator is $1$.
background
The module builds strict modular realizations on periodic carriers. The auxiliary zmodCost assigns equality cost on a cyclic carrier by returning $0$ when the arguments coincide and $1$ otherwise. Upstream lemmas establish that this cost vanishes on the diagonal (zmodCost_self) and is symmetric (zmodCost_symm). The module documentation states that the carrier interpretation remains periodic while the forced arithmetic stays the derived free orbit. Related one-elements from IntegersFromLogic and RationalsFromLogic supply the ambient logic foundation in which the realization sits.
proof idea
The definition is a record construction that directly sets Carrier to ZMod n, Cost to Nat, compare to zmodCost, compose to addition, one to 0 and generator to 1. It assigns zmodCost_self to identity_law, zmodCost_symm to non_contradiction_law, and the constant True to the remaining laws. The nontrivial_law is discharged by a short tactic that assumes $1=0$ in ZMod n, extracts a contradiction from the valuation map, and simplifies the cost expression.
why it matters
This definition realizes the modular case of StrictLogicRealization and is invoked by the downstream strictModular_arith_equiv_logicNat to produce an equivalence between the arithmetic carrier and LogicNat. It therefore completes the strict modular branch inside the UniversalForcing construction. The periodic carrier supplies one concrete model for the arithmetic orbit that later equivalences map back to the logic natural numbers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.