pith. sign in
module module high

IndisputableMonolith.Foundation.UniversalForcing.ContinuousRealization

show as:
view Lean formalization →

The module supplies the continuous positive-ratio case for Law-of-Logic realizations. Recognition Science researchers cite it when extending the Universal Forcing theorem to continuous settings. It defines the main objects that later invariance kernels apply to show arithmetic equivalence across realization types.

claimContinuous positive-ratio realization $R_c$ of the Law-of-Logic, inducing forced arithmetic objects canonically equivalent to those of other realizations.

background

The upstream UniversalForcing module states the Universal Forcing theorem: 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 type. It operates inside the Foundation domain where J-cost and phi-ladder structures govern the forced objects.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the continuous case that feeds the TwoCases invariance kernel, which establishes canonical equivalence of forced arithmetic between continuous positive-ratio realizations and the discrete Boolean realization. It fills the continuous slot required by 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)