pith. sign in
module module high

IndisputableMonolith.Foundation.UniversalForcing

show as:
view Lean formalization →

The UniversalForcing module defines the forced arithmetic object of a realization as the initial Peano algebra generated by supplied identity and step data. Categorical logicians cite it when establishing uniqueness up to isomorphism across realizations. The module imports ArithmeticOf and exposes the initiality mechanism as a shared interface for downstream realizations.

claimFor a realization supplying identity and step data, the forced arithmetic object is the initial Peano algebra \((N, z, s)\) generated by that data.

background

This module sits in the Foundation domain and imports ArithmeticOf. The upstream doc-comment states that arithmetic is extracted from an abstract Law-of-Logic realization, with the key point being initiality: once a realization supplies identity/step data, the forced arithmetic object is the initial Peano algebra generated by that data. Initial objects are unique up to unique isomorphism; this is the mechanism behind Universal Forcing.

The module supplies the common namespace and interface used by concrete realizations (continuous positive-ratio, discrete Boolean, modular, order-theoretic) that each certify their own forced arithmetic via the shared initial object.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module is imported by DiscreteLogicRealization (first non-continuous test case), UniversalForcingAudit, ContinuousRealization, ModularRealization, NaturalNumberObject (which makes precise the categorical sense in which the Law of Logic forces the natural numbers via the Lawvere characterization), OrderRealization, and others. It fills the foundation step that forces arithmetic from the Law of Logic and enables the initiality mechanism used throughout the program.

scope and limits

used by (9)

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)