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

IndisputableMonolith.Foundation.UniversalForcing.ContinuousRealization

show as:
view Lean formalization →

This module defines the continuous positive-ratio realization of the Law-of-Logic. It supplies the continuous model whose forced arithmetic objects are canonically equivalent to those from any other realization, since all such objects are initial Peano algebras. Researchers comparing continuous and discrete models in the Universal Forcing setting cite this definition when establishing invariance kernels. The module contains only definitions and no internal proofs.

claimA continuous positive-ratio Law-of-Logic realization is a structure in which arithmetic objects are forced by a continuous map preserving positive ratios, yielding objects canonically equivalent to those forced by any other Law-of-Logic realization.

background

The parent UniversalForcing module states that any two Law-of-Logic realizations have canonically equivalent forced arithmetic objects because those objects are initial Peano algebras. This module introduces the continuous positive-ratio variant as one concrete realization within that framework. It sits inside the Foundation domain and supplies the continuous case needed for later invariance arguments.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the TwoCases invariance kernel, which proves that continuous positive-ratio realizations and the discrete Boolean realization have canonically equivalent forced arithmetic. It completes the continuous half of the first non-trivial invariance result that follows from the Universal Forcing theorem.

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