strictModularRealization
The definition supplies a strict logic realization on the cyclic group Z/nZ for n greater than 1, using a binary cost that is zero exactly on equal elements and group addition for composition. Researchers constructing modular models of logic foundations cite it to obtain a concrete carrier that satisfies the strict realization axioms while keeping arithmetic as a free orbit. The construction is a direct structure instantiation that delegates identity and symmetry laws to the zmodCost lemmas and proves nontriviality by showing 1 is distinct from
claimFor each natural number $n>1$, there exists a strict logic realization whose carrier is the cyclic group $Z/nZ$, whose cost function returns 0 precisely when two elements coincide and 1 otherwise, whose composition is addition in the group, with identity element 0 and generator 1, satisfying the identity, symmetry, and nontriviality laws via the modular cost properties.
background
The module Strict/Modular.lean develops strict modular realizations on cyclic carriers. The auxiliary definition zmodCost assigns cost 0 to identical elements of ZMod n and cost 1 otherwise. Upstream lemmas establish reflexivity (zmodCost_self) and symmetry (zmodCost_symm) of this cost. The module states that the carrier interpretation is periodic while the forced arithmetic remains the derived free orbit. The compose definition from VirtueComposition appears in the dependency list but the realization itself uses direct addition on the carrier.
proof idea
The definition is a direct structure builder for StrictLogicRealization. It sets Carrier to ZMod n, Cost to Nat, compare to zmodCost, compose to addition, one to 0, and generator to 1. Identity and non-contradiction laws are supplied by zmodCost_self and zmodCost_symm. The nontrivial_law is discharged by a short tactic block that proves 1 ≠ 0 in ZMod n via valuation congruence and then simplifies the cost expression.
why it matters in Recognition Science
This definition supplies the modular instance of a strict logic realization. It is invoked by strictModular_arith_equiv_logicNat to produce an equivalence between the arithmetic carrier and LogicNat. Within the Recognition framework it provides the periodic carrier case for the universal forcing construction, preserving the free orbit arithmetic under finite moduli. No open questions are attached in the supplied material.
scope and limits
- Does not apply for n ≤ 1.
- Does not provide a continuous or infinite carrier.
- Does not modify the underlying arithmetic beyond modular reduction.
- Does not encode higher-order logical structure.
formal statement (Lean)
31def strictModularRealization (n : ℕ) [Fact (1 < n)] : StrictLogicRealization where
32 Carrier := ZMod n
proof body
Definition body.
33 Cost := Nat
34 zeroCost := inferInstance
35 compare := zmodCost
36 compose := fun a b => a + b
37 one := 0
38 generator := 1
39 identity_law := zmodCost_self
40 non_contradiction_law := zmodCost_symm
41 excluded_middle_law := True
42 composition_law := True
43 invariance_law := True
44 nontrivial_law := by
45 have hne : (1 : ZMod n) ≠ 0 := by
46 intro h
47 have hval := congrArg ZMod.val h
48 rw [ZMod.val_one n, ZMod.val_zero] at hval
49 norm_num at hval
50 simp [zmodCost, hne]
51