Foundation Primitive Recognition Calculus Delta Forced

The countable divide

In mathematics, a set is countable when its elements can be matched one-to-one with the natural numbers 0, 1, 2, and so on. The integers are countable, the rational numbers (all fractions) are countable, but the real numbers, which fill the number line, are not. This is a classical result proven by Georg Cantor in 1874, and it does not depend on any particular framework.

Recognition Science takes this classical divide and makes it the definition of physical existence. The framework's ledger, a discrete record of events, can only hold objects that can be assigned a natural number label. A type is called δ-forced when it carries such an explicit countable certificate: an injection into ℕ. The framework then states, as a thesis, that being physically real is exactly the same as being δ-forced. This is a definitional choice, not a derived theorem, and it draws the line between what the framework can describe and what it cannot.

The mathematical content is carried by the definition of DeltaForced. The framework's machine-checked library of formal theorems proves that the natural numbers, integers, and rationals all satisfy this property. It constructs explicit injections, such as pairing a fraction's numerator and denominator into a single natural number. The library also proves the other side: the real numbers are not δ-forced. Since the reals are uncountable, no such injection can exist. The central result, called demarcation, states all four facts together: the naturals, integers, and rationals are physically real, while the reals are not.

This demarcation has a direct consequence. The framework proves that δ-forced is equivalent to the standard mathematical notion of countability. It also proves that the property is preserved under common constructions: a subtype of a δ-forced type is δ-forced, as are its finite sums and products. This means the framework's universe of physically real objects is closed under the operations one expects, while remaining strictly smaller than the full continuum of real numbers.

What this changes is the boundary of what the framework can model. Any proposed physical quantity that requires the full real number line, such as a continuous field taking every real value, falls outside the ledger. The framework does not claim the real numbers do not exist mathematically; it claims they are not the right objects for its discrete, event-based account of reality. This is the foundational cut that shapes everything else built on top of it.

/-- 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 ↪ ℕ)

/-- 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

/-- The continuum is **not** δ-forced. A certificate would force `Countable ℝ`, but
ℝ has cardinality `𝔠 > ℵ₀`. -/
theorem not_deltaForced_real : ¬ DeltaForced ℝ := by
  intro h
  have hc : Countable ℝ := countable_of_deltaForced h
  have hle : Cardinal.mk ℝ ≤ Cardinal.aleph0 := Cardinal.mk_le_aleph0_iff.mpr hc
  rw [Cardinal.mk_real] at hle
  exact absurd hle (not_le.mpr Cardinal.aleph0_lt_continuum)

/-- **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⟩

/-- δ-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⟩⟩

What this page does not claim

The framework does not prove that the real numbers fail to exist mathematically, only that they are not δ-forced. The thesis that physical reality equals δ-forced is a definitional choice, not a derived theorem.

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: