pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.UniversalForcing.DiscreteRealization

show as:
view Lean formalization →

This module supplies the discrete Boolean realization of the Law-of-Logic as a propositional carrier. It acts as the first non-continuous test case inside the Universal Forcing framework. Researchers verifying invariance kernels cite it to confirm that forced arithmetic remains canonically equivalent across carrier types. The module consists of targeted definitions establishing the carrier and its arithmetic equivalence.

claimA discrete propositional carrier realizing the Law-of-Logic, with forced arithmetic canonically isomorphic to that induced by continuous positive-ratio carriers.

background

Universal Forcing requires any two LogicRealizations to induce isomorphic forced arithmetic. The upstream DiscreteLogicRealization module introduces the second such realization as a discrete Boolean/propositional carrier and marks it as the first non-continuous test case. This module concretizes that carrier inside the foundation layer, providing the discrete counterpart to continuous positive-ratio realizations for direct comparison.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the discrete case required by the TwoCases invariance kernel, which shows that continuous positive-ratio realizations and the discrete Boolean realization have canonically equivalent forced arithmetic. It also feeds UniversalForcingSelfReference, where the meta-theorem is shown to fit the Law-of-Logic structural shape, closing the framework reflexively. It completes the non-continuous test case in 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 (2)