IndisputableMonolith.Foundation.UniversalForcing.Strict.Modular
Module constructing a strict modular realization on residue rings for every modulus n > 1. It supplies a modular equality cost, verifies the strict-forcing interface on that carrier, and records an arithmetic equivalence with the LogicNat surface. Downstream categorical hooks import it as the modular step after the ordered realization on Z. Content is mostly definitions and short structural lemmas.
claimFor each integer modulus $n > 1$, the module equips $\mathbb{Z}/n\mathbb{Z}$ with a modular cost $d([a],[b])$ (vanishing iff $[a]=[b]$), packages a strict modular realization of the universal-forcing interface on that carrier, and exhibits an arithmetic equivalence between this realization and the LogicNat carrier.
background
Universal Forcing builds a chain of strict realizations of the Recognition interface on successively more structured carriers. The immediate upstream module, Strict.Ordered, gives the ordered case: a strict realization on $\mathbb{Z}$ with equality cost and unit translation.
This module steps from $\mathbb{Z}$ to residue classes. The sibling definitions introduce zmodCost (the equality cost on $\mathbb{Z}/n\mathbb{Z}$), its reflexivity and symmetry facts, the packaged strictModularRealization for $n > 1$, and strictModular_arith_equiv_logicNat linking the modular arithmetic carrier to the LogicNat NNO surface used later in the categorical layer.
The setting is foundation-level: no physical constants yet, only the algebraic carriers that the forcing chain will later specialize.
proof idea
Definition-and-packaging module rather than a deep proof development. Cost on residue classes is defined by lifting equality (or a discrete distance) from $\mathbb{Z}/n\mathbb{Z}$; self and symmetry lemmas are immediate from that definition. The strict modular realization is assembled by feeding the modular carrier and cost into the strict-forcing interface already shaped by Strict.Ordered. The arithmetic equivalence to LogicNat is a structure-preserving map between the modular carrier and the canonical NNO surface, recorded so later categorical code can treat them interchangeably.
why it matters in Recognition Science
Sits between the ordered realization on $\mathbb{Z}$ and the categorical/Lawvere-style hook. Strict.Categorical imports this module and uses the LogicNat surface (with the modular equivalence available) as its carrier: "the carrier is the canonical LogicNat NNO surface from CategoricalLogicRealization." Without a modular step, the forcing chain would jump from ordered integers to category-theoretic NNOs with no finite-cyclic intermediate. In the broader Recognition foundation this is scaffolding for the universal-forcing spine that eventually constrains J-cost uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), and $D=3$ (T8), though those landmarks are not proved here.
scope and limits
- Does not prove J-uniqueness, phi-forcing, eight-tick structure, or D = 3.
- Does not treat the modulus n = 1 or the zero ring.
- Does not construct a full Mathlib category-theory NNO; only an arithmetic equivalence hook.
- Does not derive physical constants or mass-ladder formulae.
- Does not claim uniqueness of the modular cost among all possible costs on Z/nZ.