pith. sign in
module module high

IndisputableMonolith.Foundation.ModularLogicRealization

show as:
view Lean formalization →

ModularLogicRealization defines equality costs and modular interpretations on finite carriers as an extension of discrete logic. Researchers building ordered realizations or audit surfaces for Universal Forcing cite it for the finite modular test case. The module consists entirely of definitions and basic invariants with no proof obligations.

claimEquality cost function $finCost$ on a finite carrier equipped with modulus $m>1$, together with the modular interpretation $modularInterpret$ that realizes propositional logic via cyclic steps $cycStep$ and the invariant $modular_arithmetic_invariant$.

background

The module sits in the Foundation domain and imports DiscreteLogicRealization, whose doc-comment states it supplies the discrete Boolean/propositional carrier as the first non-continuous test case for Universal Forcing. It introduces finCost and its symmetry and self-properties, the modulus with positivity and lower bound, cycStep, modularInterpret with zero and step cases, modularRealization, and the modular_arithmetic_invariant. These objects realize equality cost on finite carriers while preserving the discrete logic structure.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the modular finite realization that feeds OrderedLogicRealization (ordered faithful realization for Universal Forcing) and UniversalForcingAudit (reproducible audit surface for the Universal Forcing program). It advances the second Law-of-Logic realization from the discrete Boolean carrier toward ordered and audited stages of the forcing chain.

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)