IndisputableMonolith.Foundation.UniversalForcing.Strict.Modular
This module defines strict modular realizations for moduli n greater than 1, extending the ordered integer structure with a cost function on Z/nZ. Researchers formalizing the Recognition Science forcing chain cite it when bridging ordered and modular layers before categorical hooks. The module supplies definitions for zmodCost together with self-symmetry and symmetry lemmas plus an arithmetic equivalence to logic naturals.
claimFor moduli $n>1$, the strict modular realization equips $\mathbb{Z}/n\mathbb{Z}$ with the cost function zmodCost satisfying zmodCost_self and zmodCost_symm, together with the realization strictModularRealization and the equivalence strictModular_arith_equiv_logicNat.
background
The module belongs to the Strict subhierarchy of UniversalForcing in the Foundation layer. It imports the Ordered module, whose doc-comment describes the strict ordered realization on $\mathbb{Z}$ with equality cost and unit translation. Sibling definitions introduce zmodCost as the modular cost, its self and symmetry properties, the main realization object, and the arithmetic equivalence to logic naturals. The setting is the strict forcing chain prior to categorical extensions.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module feeds the downstream Categorical module, whose doc-comment describes the strict categorical/Lawvere-style realization hook whose carrier is the canonical LogicNat NNO surface. It supplies the modular step in the strict ordered realization sequence within the UniversalForcing chain.
scope and limits
- Does not treat moduli equal to 1.
- Does not supply the full Mathlib category-theory NNO API.
- Does not address non-strict realizations.
- Does not extend to higher-dimensional or non-modular cases.