pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.ModularLogicRealization

show as:
view Lean formalization →

The module supplies definitions for equality cost on a finite carrier to support modular logic realizations in the Recognition Science foundation. Universal Forcing researchers cite it when extending discrete Boolean carriers to cyclic modular structures. It consists of definitions for the finite cost function, modulus properties, cyclic steps, and modular interpretations that preserve arithmetic invariants.

claimEquality cost on a finite carrier is given by a function $f(x,y)$ on a finite set equipped with modulus $m$, satisfying $f(x,y)=f(y,x)$ and $f(x,x)=0$, together with a modular interpretation map that is invariant under cyclic steps.

background

The upstream DiscreteLogicRealization supplies the discrete Boolean/propositional carrier, described as the second Law-of-Logic realization and the first non-continuous test case for Universal Forcing. This module extends that setting by defining the equality cost on a finite carrier, together with the modulus, cyclic step function, and modular interpretation map. These objects satisfy self-symmetry and positivity properties that prepare the ground for ordered realizations.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the modular arithmetic invariant that feeds OrderedLogicRealization, which delivers the ordered faithful realization for Universal Forcing, and UniversalForcingAudit, which provides the reproducible audit surface for the Universal Forcing program. It advances the foundation by realizing logic on finite modular carriers.

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)