pith. sign in
module module high

IndisputableMonolith.Foundation.UniversalForcing.DiscreteRealization

show as:
view Lean formalization →

DiscreteRealization supplies the discrete Boolean/propositional carrier as the second Law-of-Logic realization and the first non-continuous test case. Researchers working on invariance kernels or the reflexive closure of Universal Forcing cite it to confirm that the forcing conditions hold for propositional logic. The module consists of definitions establishing the required arithmetic equivalence. It contains no theorems or proofs.

claimThe discrete Boolean realization $R$ of the Law-of-Logic, a propositional carrier satisfying the conditions for canonically equivalent forced arithmetic with continuous positive-ratio realizations.

background

The module imports DiscreteLogicRealization, whose doc-comment states: 'The second Law-of-Logic realization: a discrete Boolean/propositional carrier. This is the first non-continuous test case for Universal Forcing.' In the Recognition Science setting, Universal Forcing asserts that any two LogicRealizations induce canonically isomorphic forced arithmetic. The module introduces the discrete carrier via sibling definitions discreteRealization and discrete_arith_equiv_logicNat.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the TwoCases invariance kernel, whose doc-comment states it is the 'First non-trivial invariance kernel: continuous positive-ratio realizations and the discrete Boolean realization have canonically equivalent forced arithmetic.' It also feeds UniversalForcingSelfReference, which formalizes that the meta-theorem itself fits the Law-of-Logic structural shape and renders the framework reflexively closed. It supplies the discrete test case required by 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)