Pith. sign in
module module moderate

IndisputableMonolith.Foundation.UniversalForcing.ModularRealization

show as:
view Lean formalization →

Defines equality cost and orbit interpretation on a cyclic (Z/nZ) carrier, giving a modular model of forced arithmetic. Used by anyone checking that Law-of-Logic realizations yield equivalent arithmetic on finite cyclic groups. The module packages cost symmetry, self-cost zero, and an invariance statement that modular arithmetic is realization-independent.

claimOn the cyclic carrier $\mathbb{Z}/n\mathbb{Z}$, an equality cost $d(a,b)$ is defined so that $d(a,a)=0$ and $d(a,b)=d(b,a)$. Orbit interpretation maps modular residues to forced arithmetic data. Modular realization asserts that this cyclic model is a Law-of-Logic realization whose arithmetic is invariant under change of realization.

background

Universal Forcing says that any two Law-of-Logic realizations have canonically equivalent forced arithmetic, because those objects are initial Peano algebras. This module supplies one concrete carrier: modular (cyclic) arithmetic.

The equality cost on $\mathbb{Z}/n\mathbb{Z}$ measures disagreement of residues; sibling facts record that self-cost vanishes and the cost is symmetric. Orbit interpretation reads residues as arithmetic data forced by the Law of Logic. Modular realization packages these into a realization object that can be compared across models.

The parent UniversalForcing development frames the uniqueness claim; this file is the cyclic special case before the general invariance theorem.

proof idea

Definition-heavy module with short supporting lemmas. Cost on the cyclic carrier is introduced first; self-cost and symmetry are immediate from the definition. Orbit interpretation is a structure map from residues into forced arithmetic. The modular realization object is assembled from those pieces; modular arithmetic invariance is the statement that the forced arithmetic extracted this way does not depend on the ambient realization, feeding the general Universal Forcing argument.

why it matters in Recognition Science

Feeds Invariance.Universal, the general Universal Forcing theorem: every Law-of-Logic realization carries canonically equivalent forced arithmetic. The cyclic carrier is the simplest nontrivial model where equality cost, orbits, and realization invariance can be checked by hand before the abstract initial-algebra argument. In the Recognition foundation stack this sits under Universal Forcing (forced Peano arithmetic unique up to canonical equivalence), upstream of later physics forcing (T5–T8). It does not itself force $\varphi$, eight-tick structure, or $D=3$; it only stabilizes the arithmetic layer those steps presuppose.

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