Foundation Primitive Recognition Calculus Delta Forced Delta Forced Iff Countabl

The countable certificate

In mathematics, a set is countable when its elements can be listed in a sequence: each element gets a distinct natural number label, 0, 1, 2, and so on. The integers are countable, the rational numbers are countable, and the real numbers are famously not. The declaration deltaForced_iff_countable in the Recognition Science library proves that its own notion, called δ-forced, is exactly this classical property. A type is δ-forced when it carries an explicit injection into the natural numbers, and the declaration states that δ-forced and countable are equivalent.

The proof runs in two directions. If a type is δ-forced, its injection into the naturals directly yields a countable set, since an injective map into a countable type is itself countable. Conversely, if a type is countable, the standard result that countable types embed into the naturals supplies the required injection. The library also shows the natural numbers, integers, and rationals are all δ-forced, while the reals are not, a result that follows from Cantor's diagonal argument. These facts combine into a single declaration, demarcation, which states the natural numbers, integers, and rationals are physically real while the reals are not, where physically real is defined as δ-forced.

In Recognition Science, the framework models recognition, a discrete record of events, as the primitive act. The claim is that anything physically real must be enumerable from the act of distinction itself, and the declaration deltaForced_iff_countable is what connects that philosophical thesis to a precise mathematical statement. The framework's library proves that δ-forced types are closed under products, sums, and subtypes, meaning that any construction built from countable pieces remains countable. This gives the framework a clean formal handle on which mathematical objects can appear in its ledger.

The declaration does not claim that the reals are physically impossible in some empirical sense, nor does it assert that the identification of physical reality with countability is itself a proved mathematical fact. The identification is a definitional choice, recorded in the declaration PhysicallyReal, and the declaration only establishes the equivalence between δ-forced and countable. The framework's own documentation states that the name δ-forced records the claim that this demarcation line is the physical one, but that demarcation remains a thesis, not a proved result.

/-- A type is **δ-forced** when it carries an explicit countable certificate: an
injection into ℕ. This is the formal content of "finitely generated, hence
enumerable, from the act of distinction." -/
def DeltaForced (X : Type u) : Prop := Nonempty (X ↪ ℕ)

/-- δ-forced ↔ countable. The forward direction is choice-free; the backward
direction extracts a certificate from countability and uses choice. -/
theorem deltaForced_iff_countable (X : Type u) : DeltaForced X ↔ Countable X := by
  constructor
  · exact countable_of_deltaForced
  · intro h
    obtain ⟨f, hf⟩ := h.exists_injective_nat'
    exact ⟨⟨f, hf⟩⟩

/-- **Demarcation.** The δ tower (ℕ, ℤ, ℚ) is physically real; the continuum ℝ is
not. The forced-tower conjuncts are choice-free (`forcedTower`); the ℝ conjunct uses
the classical uncountability of ℝ, which is a fact about the display-tier object, not
about the forced side. -/
theorem demarcation :
    PhysicallyReal ℕ ∧ PhysicallyReal ℤ ∧ PhysicallyReal ℚ ∧ ¬ PhysicallyReal ℝ :=
  ⟨deltaForced_nat, deltaForced_int, deltaForced_rat, not_deltaForced_real⟩

/-- The ontological reading: **physically real** is, by thesis, exactly δ-forced. The
mathematical content is carried entirely by `DeltaForced`; this name records the
claim that the demarcation line below is the physical one. -/
def PhysicallyReal (X : Type u) : Prop := DeltaForced X

What this page does not claim

The declaration does not prove that physical reality is countable; that is a definitional thesis, not a mathematical result. The declaration does not claim that the reals are physically impossible, only that they are not δ-forced under the framework's definition. The declaration does not provide an empirical argument for the countability of physical reality.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaForced.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: