strictModularRealization
plain-language theorem explainer
This definition assembles a StrictLogicRealization whose carrier is the cyclic group Z/nZ for each n>1, using the binary cost that vanishes on equality, addition for composition, zero as identity, and one as generator. Workers constructing arithmetic models of logic or proving orbit equivalences to LogicNat cite the construction. It is assembled directly by field assignment, invoking zmodCost together with its self and symmetry lemmas for the required laws.
Claim. For each natural number $n>1$, there exists a strict logic realization with carrier the cyclic group $Z/nZ$, cost function $c(a,b)=0$ if $a=b$ and $1$ otherwise, composition given by addition in the group, identity element $0$, generator $1$, and the identity, non-contradiction, excluded-middle, composition, invariance, and nontriviality laws satisfied by direct assignment or the cited cost properties.
background
The module supplies strict modular realizations on cyclic carriers. StrictLogicRealization is the structure type that packages a carrier set, a cost function to natural numbers, a comparison operation, a composition law, distinguished elements one and generator, and proofs of the six named laws. The local setting states that the carrier interpretation is periodic while the forced arithmetic remains the derived free orbit. zmodCost is the equality cost on a cyclic carrier, returning 0 on equality and 1 otherwise; its self and symmetry theorems establish that the cost vanishes on the diagonal and is symmetric.
proof idea
The definition populates each field of the StrictLogicRealization structure. Carrier, Cost, compare, compose, one and generator receive the obvious assignments ZMod n, Nat, zmodCost, addition, 0 and 1. identity_law is discharged by zmodCost_self, non_contradiction_law by zmodCost_symm, and the remaining four laws are set to True. nontrivial_law proceeds by a short tactic block that first proves 1 ≠ 0 in ZMod n via valuation and then simplifies the cost expression.
why it matters
The definition supplies the modular carrier instance required by the downstream strictModular_arith_equiv_logicNat, which converts the arithmetic orbit into an equivalence with LogicNat. It therefore realizes the periodic case inside the universal forcing construction, where the carrier remains periodic yet the arithmetic orbit stays free. The construction sits inside the chain that derives arithmetic models from the Recognition Composition Law and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.