IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaForced
A type is δ-forced when it admits an explicit injection into the naturals: a countable certificate that it is finitely generated from acts of distinction. The module defines that predicate, equates it with physical reality in the RS sense, and builds the concrete injections for ℕ, ℤ, and ℚ. Anyone citing the δ-only tower or the PublicSpine dual forcing surface depends on these certificates. The content is mostly definitional plus elementary injectivity lemmas.
claimA type $X$ is $\delta$-forced when there exists an injection $X \hookrightarrow \mathbb{N}$. The module equates $\delta$-forced with physically real, and exhibits explicit injections for $\mathbb{N}$, $\mathbb{Z}$, and $\mathbb{Q}$ (via pairing and sign/numerator/denominator encodings).
background
In the Primitive Recognition Calculus, physical content is required to arise from finite acts of distinction. The operational stand-in is countability with an explicit certificate: an injection into $\mathbb{N}$. That is the meaning of $\delta$-forced.
The module sits under Foundation and imports Omniscience. It introduces the predicate $\mathrm{DeltaForced},X$, the companion notion $\mathrm{PhysicallyReal}$, and the equivalence linking them. Concrete encodings follow: identity on $\mathbb{N}$; a sign-and-magnitude map $\mathbb{Z}\to\mathbb{N}$; and a rational encoding built from an injective pairing on $\mathbb{N}\times\mathbb{N}$ together with a normal-form equality lemma for rationals.
These certificates are the discrete half of the dual forcing surface later exposed in PublicSpine: the $\delta$-only tower $\mathbb{N}/\mathbb{Z}/\mathbb{Q}$, with the continuum cut handled separately.
proof idea
Definition module with short injectivity proofs. DeltaForced is the existence of an injection into $\mathbb{N}$; PhysicallyReal is tied to it by an iff. intToNat and ratToNat are explicit encodings; their injectivity lemmas are elementary case splits (sign/magnitude; pairing plus rational normal form via rat_eq_of). dpair supplies the underlying $\mathbb{N}\times\mathbb{N}$ pairing. deltaForced_nat and deltaForced_int package the certificates for the first two rungs of the tower. No deep tactics: constructors, cases, and arithmetic.
why it matters in Recognition Science
PublicSpine imports this module as the honest $\delta$-stratified dual of UnifiedForcingChain. The downstream doc states the $\delta$-only tower is $\mathbb{N}/\mathbb{Z}/\mathbb{Q}$ (forced_tower_holds), with the continuum cut as classicalExtension and a panel note not to place $\neg\mathbb{R}$ under deltaOnly. Without the injections and the physicallyReal equivalence here, that tower has no certificate layer. In the broader RS forcing chain this is the discrete enumeration side of recognition: what can be finitely generated from distinction before continuum structure is adjoined. It does not touch T5–T8 (J-uniqueness, $\varphi$, eight-tick, $D=3$) directly; it supplies the countable substrate those later steps presuppose when they speak of discrete modes and ladders.
scope and limits
- Does not prove uncountable types fail physical reality; continuum is deferred to classicalExtension.
- Does not construct an injection for $\mathbb{R}$ or claim $\neg\mathrm{DeltaForced}\,\mathbb{R}$.
- Does not derive mass, $\alpha$, or forcing steps T5–T8.
- Does not assert uniqueness of the chosen encodings, only that some injection exists.
- Does not replace UnifiedForcingChain; PublicSpine keeps both surfaces.
used by (1)
depends on (1)
declarations in this module (21)
-
def
DeltaForced -
def
PhysicallyReal -
theorem
physicallyReal_iff_deltaForced -
def
intToNat -
theorem
intToNat_inj -
def
dpair -
theorem
dpair_inj2 -
theorem
rat_eq_of -
def
ratToNat -
theorem
ratToNat_inj -
theorem
deltaForced_nat -
theorem
deltaForced_int -
theorem
deltaForced_rat -
theorem
countable_of_deltaForced -
theorem
not_deltaForced_real -
theorem
forcedTower -
theorem
demarcation -
theorem
deltaForced_iff_countable -
theorem
deltaForced_prod -
theorem
deltaForced_subtype -
theorem
deltaForced_sum