Pith. sign in
module module high

IndisputableMonolith.Foundation.ModularLogicRealization

show as:
view Lean formalization →

Finite modular carrier for Universal Forcing: equality cost on a cyclic residue ring, with a step map and an interpretation that preserves the discrete logic laws. Anyone checking that forcing is not continuum-specific cites this realization. The module defines the cost, modulus bounds, cyclic step, and the modular realization bundle, then records the arithmetic invariant.

claimOn a finite carrier $\mathbb{Z}/m\mathbb{Z}$ with $m>1$, an equality cost $c(x,y)$ is symmetric and vanishes on the diagonal; a cyclic step and modular interpretation realize the discrete logic laws, and modular arithmetic is invariant under that interpretation.

background

Universal Forcing asks whether the Recognition composition law and the J-cost uniqueness chain force the same structure on every faithful logic carrier, not only on continuous ones. The upstream discrete Boolean realization is the first non-continuous test case.

This module supplies the next discrete test: a finite cyclic carrier. Equality cost on that carrier is the finite analogue of defect distance: it is zero exactly when the two residues agree, and it is symmetric. A positive modulus $m>1$ fixes the ring; the cyclic step advances the residue; modular interpretation maps logical structure into that arithmetic.

The local setting is therefore a Law-of-Logic realization on $\mathbb{Z}/m\mathbb{Z}$, sitting between the pure discrete Boolean carrier and the ordered faithful realization used later in the audit surface.

proof idea

Definition-and-lemma module, not a single theorem. It introduces finCost with reflexivity and symmetry, fixes a modulus with positivity and $1<m$, defines the cyclic step and the modular interpretation (including zero and step cases), packages modularRealization, and states the modular arithmetic invariant. Arguments are direct finite-arithmetic checks and one-line rewrites from the discrete realization import; no deep forcing step is proved here.

why it matters in Recognition Science

Closes the finite-carrier slot in the Universal Forcing program: after continuous and discrete Boolean carriers, modular arithmetic shows the same logic laws survive on a cyclic residue ring. Downstream, OrderedLogicRealization imports this module for the ordered faithful realization, and UniversalForcingAudit imports it as part of the reproducible audit surface. Together they support the claim that forcing is carrier-independent rather than an artifact of $\mathbb{R}_+$. Landmark contact is indirect: the module is infrastructure for the forcing chain (T5 J-uniqueness and RCL) rather than a statement of those theorems.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (13)