Foundation Primitive Recognition Calculus Delta Forced Countable Of Delta Forced

The countable certificate

The theorem countable_of_deltaForced states that any type which carries a δ-forced certificate is countable. A δ-forced certificate is an explicit injection into the natural numbers: a rule that assigns to each element a unique natural number label, with no two elements sharing a label. This is the formal content of the idea that a collection which is finitely generated, hence enumerable, from the act of distinction is countable. The declaration proves that having such a certificate implies the standard mathematical property of countability.

The proof is short and constructive. Given an injection e from a type X into the natural numbers, the theorem uses the fact that an injective function into a countable type yields a countable type. The library then applies this to show that the natural numbers, the integers, and the rational numbers are all δ-forced, and therefore countable. The real numbers are not: the theorem not_deltaForced_real proves that no injection from the reals into the natural numbers exists, because the reals have cardinality strictly greater than the natural numbers.

In Recognition Science, the declaration carries an ontological reading. The framework defines PhysicallyReal as exactly δ-forced: a type is physically real, by thesis, precisely when it carries this countable certificate. The declaration countable_of_deltaForced is the bridge that connects this framework-specific notion to the classical mathematical concept of countability. It does not, however, claim that countability itself is a physical property, nor that the natural numbers are physically real in any empirical sense. Those are separate claims, and the framework's demarcation theorem states that the natural numbers, integers, and rationals are physically real while the reals are not, a statement about the framework's own definition, not a discovery about the physical universe.

The practical consequence is a clean boundary. Any collection that can be generated by a finite process of distinction, such as the rational numbers, can be listed in an infinite queue. The real numbers, which include the continuum of points on a line, cannot be so listed. This gives a precise, machine-checked sense in which the framework's notion of physical reality is countable, and it sets the stage for the framework's further claims about what structures can and cannot be built from recognition events.

/-- A δ-forced type is countable (the certificate is an injection into ℕ).
Choice-free. -/
theorem countable_of_deltaForced {X : Type u} (h : DeltaForced X) : Countable X := by
  obtain ⟨e⟩ := h
  exact e.injective.countable

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

/-- 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 claim that countability is itself a physical property. The declaration does not claim that the natural numbers are physically real in an empirical sense. The declaration does not claim that the framework's notion of physical reality matches any experimental observation.

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: