pith. sign in
module module high

IndisputableMonolith.Foundation.UniversalForcing.Strict.Modular

show as:
view Lean formalization →

The module supplies strict modular realizations for moduli n greater than 1, extending the ordered integer case with cost functions on Z/nZ. Researchers extending the UniversalForcing chain toward categorical structures would cite it as the intermediate modular layer. Content consists of definitions for the modular cost together with self-symmetry and arithmetic-logic equivalence lemmas.

claimFor each integer $n>1$, the modular cost function $zmodCost:ℤ/nℤ→ℝ$ satisfies $zmodCost(x)=zmodCost(-x)$ and induces an arithmetic equivalence to the logic-natural surface.

background

The module imports the strict ordered realization on ℤ, which equips the integers with equality cost and unit translation. It introduces the modular cost together with its self and symmetry properties, plus the strict modular realization map and the arithmetic-to-logic equivalence. The local setting is the strict fragment of the UniversalForcing hierarchy, positioned between ordered and categorical layers.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the modular component required by the downstream Categorical module, which uses it to attach the Lawvere-style realization hook on the canonical LogicNat NNO surface. It fills the modular slot in the strict realization sequence inside Foundation.UniversalForcing.Strict.

scope and limits

used by (1)

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 (5)