IndisputableMonolith.Foundation.UniversalForcing.Strict.Modular
The module defines strict modular realizations for moduli n > 1, extending the ordered integer case to Z/nZ carriers. It introduces zmodCost with self and symmetry lemmas plus the central strictModularRealization and its arithmetic equivalence to the LogicNat NNO surface. Recognition Science researchers cite it when moving from ordered to categorical strict forcings. The module is definitional with supporting arithmetic lemmas.
claimFor moduli $n > 1$, the strict modular realization equips $Z/nZ$ with the equality cost function zmodCost satisfying zmodCost(x,x)=0 and symmetry, together with the equivalence strictModular_arith_equiv_logicNat linking the arithmetic structure to the canonical LogicNat NNO surface.
background
The module builds directly on the upstream strict ordered realization on Z, which supplies equality cost and unit translation. It defines zmodCost as the modular cost on Z/nZ, with lemmas establishing zmodCost_self and zmodCost_symm. The main object strictModularRealization realizes the forcing instance for n > 1, while strictModular_arith_equiv_logicNat provides the bridge to the LogicNat surface.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the modular carrier required by the downstream Categorical submodule for its strict categorical/Lawvere-style realization hook on the LogicNat NNO surface. It fills the modular step in the strict forcing chain, enabling the transition from ordered integer realizations to categorical structures within UniversalForcing.Strict.
scope and limits
- Does not cover moduli n ≤ 1.
- Does not implement full Mathlib category-theory NNO API.
- Does not address non-strict or weighted cost functions.
- Does not prove properties beyond basic arithmetic equivalence.