Pith. sign in
module module high

IndisputableMonolith.Foundation.UniversalForcing

show as:
view Lean formalization →

UniversalForcing extracts the forced arithmetic object from any Law-of-Logic realization by initiality. Researchers deriving arithmetic from logic or testing categorical initial algebras cite it. The module imports ArithmeticOf and supplies the common interface used by all concrete realization submodules.

claimFor a realization $R$ supplying identity and step data, the forced arithmetic object is the initial Peano algebra generated by that data.

background

The module imports ArithmeticOf, whose doc states: "Arithmetic extracted from an abstract Law-of-Logic realization. The key point is 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."

It organizes this construction as the central object for the Universal Forcing program. Sibling definitions in the module (arithmeticOf, arithmetic_invariant, arith_universal_initial, universal_forcing, peano_surface) supply supporting invariants and the initial algebra surface.

Downstream modules instantiate the same object on different carriers: discrete Boolean, continuous positive-ratio, modular ZMod, order on Z, and the Lawvere natural-number object triple (N, z, s).

proof idea

This is a definition module, no proofs. It imports ArithmeticOf and re-exports the initial Peano algebra construction under the UniversalForcing namespace for use by realization modules.

why it matters in Recognition Science

This module feeds DiscreteLogicRealization, ContinuousRealization, ModularRealization, OrderRealization, NaturalNumberObject, UniversalForcingAudit, UniversalForcingSelfReference, and StrictRealization. It supplies the initiality mechanism that forces the natural numbers from the Law of Logic, serving as the common foundation for all test realizations in 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)