Pith. sign in
module module high

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaForced

show as:
view Lean formalization →

Defines δ-forced types: those carrying an explicit injection into the naturals, the formal stand-in for "finitely generated from distinction." Introduces the PhysicallyReal predicate as equivalent to δ-forced, and builds the countable certificates for ℕ, ℤ, and ℚ. Cited by anyone working the δ-stratified public spine. The module is mostly definitions plus injectivity lemmas for the encoding maps.

claimA type $T$ is $\delta$-forced when there exists an injection $T \hookrightarrow \mathbb{N}$. Physical reality is identified with $\delta$-forcedness. The module supplies explicit injections $\mathbb{N}\hookrightarrow\mathbb{N}$, $\mathbb{Z}\hookrightarrow\mathbb{N}$, and $\mathbb{Q}\hookrightarrow\mathbb{N}$ (via pairing and fraction encodings), so the discrete tower $\mathbb{N}/\mathbb{Z}/\mathbb{Q}$ is $\delta$-forced.

background

In the Primitive Recognition Calculus, distinction is the generative act. Anything that can be built by finitely many distinctions should be enumerable: it must admit a countable certificate. The module packages that demand as the structure DeltaForced, an explicit injection into $\mathbb{N}$.

PhysicallyReal is the same demand under a physics-facing name; the module proves the two predicates coincide. Encodings are concrete: identity on $\mathbb{N}$, a sign-and-magnitude map intToNat on $\mathbb{Z}$, and a pairing-plus-fraction map ratToNat on $\mathbb{Q}$, each with a proved injectivity lemma.

The surrounding setting is the dual public surface of the Unified Forcing Chain. Upstream sits the Omniscience layer of the same calculus; downstream the PublicSpine imports this module to anchor the $\delta$-only tower.

proof idea

Definition module with supporting injectivity lemmas, not a single theorem. DeltaForced is a structure packing an injection into $\mathbb{N}$. PhysicallyReal is defined equivalently, and physicallyReal_iff_deltaForced is the obvious biconditional.

For $\mathbb{Z}$, intToNat folds sign into a natural; intToNat_inj is a case split on signs. For $\mathbb{Q}$, dpair is a pairing function, rat_eq_of normalizes fractions, and ratToNat_inj composes those facts. Instances deltaForced_nat and deltaForced_int (and the rational analogue) are then one-line structure constructors from those injections.

why it matters in Recognition Science

PublicSpine imports this module as the certificate layer of the dual forcing surface. That spine is the public dual of UnifiedForcingChain: it keeps a Boolean/certificate path for pedagogy while stating the honest $\delta$-stratified map. Downstream doc-comment: the $\delta$-only tower is $\mathbb{N}/\mathbb{Z}/\mathbb{Q}$ via forced_tower_holds; the continuum cut is classicalExtension, and one must not place $\neg\mathbb{R}$ under deltaOnly.

Without an explicit countable certificate, "finitely generated from distinction" is slogan rather than Lean content. This module closes that gap for the discrete tower and feeds every later claim that physical types in the RS foundation are $\delta$-forced. It does not itself force dimension, $\phi$, or the eight-tick octave; those remain T6–T8 in the UFC chain.

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