Foundation Primitive Recognition Calculus Delta Forced Delta Forced Int

The enumerable integers

The integers are the whole numbers, positive, negative, and zero. A familiar fact about them is that they can be arranged in a single endless list: 0, 1, -1, 2, -2, 3, -3, and so on. Mathematicians call a set that admits such a listing countable. The declaration deltaForced_int is a machine-checked proof of exactly this listing property for the integers, expressed in a precise formal language.

The proof works by building an explicit injection, a one-to-one map, from the integers into the natural numbers. The map sends a nonnegative integer k to 2k, and a negative integer -k-1 to 2k+1. This separates the list into evens for the nonnegative numbers and odds for the negative ones, guaranteeing that no two different integers land on the same natural number. The formal library of theorems checks each step of this argument and confirms the map is injective.

In Recognition Science, this countable listing is not just a curiosity. The framework defines a type as δ-forced when it carries such an explicit countable certificate, an injection into the natural numbers. Its thesis identifies being physically real with being δ-forced. The theorem deltaForced_int therefore establishes that the integers qualify as physically real under this definition. The same proof pattern applies to the natural numbers and the rational numbers, and the framework's library proves all three in a single statement called the forced tower.

The framework's library also proves a sharp boundary: the real numbers, which include irrationals like the square root of 2, are not δ-forced. There is no way to list all real numbers in a single endless sequence, a classical result of Georg Cantor from 1874. This gives a precise demarcation: the integers, rationals, and naturals are in, the reals are out. The integers thus serve as a basic example of what the framework counts as a physically real collection of objects.

What deltaForced_int does not claim is any statement about the physical universe itself. It proves a mathematical property of the integers, namely countability. The step from that property to physical reality is a definitional choice, a thesis the framework adopts, not a theorem about nature. The declaration does not assert that integers exist as physical objects, nor that the framework's notion of physical reality matches any experimental observation. It is a formal building block, not an empirical claim.

/-- ℤ is δ-forced via the explicit even/odd certificate. Choice-free. -/
theorem deltaForced_int : DeltaForced ℤ := ⟨⟨intToNat, intToNat_inj⟩⟩

/-- 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 forced tower is constructively (choice-free) physically real. Isolated from
the ℝ statement so the positive content carries no `Classical.choice`: this is the
exact formal residue of "the δ tower ℕδ → ℤδ → ℚδ is built, not posited." -/
theorem forcedTower :
    PhysicallyReal ℕ ∧ PhysicallyReal ℤ ∧ PhysicallyReal ℚ :=
  ⟨deltaForced_nat, deltaForced_int, deltaForced_rat⟩

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

What this page does not claim

The declaration does not assert that integers exist as physical objects in the universe. The framework's identification of physical reality with δ-forced is a definitional thesis, not an empirically tested claim. The theorem does not prove anything about the real numbers beyond their uncountability.

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: