Foundation Primitive Recognition Calculus Frscarrier Carrier Values Subset

The finite carrier

The real numbers are vast, but a framework that computes must start with a smaller, explicit set of values. In Recognition Science, that set is called the carrier: the collection of all numbers the framework's expressions can produce. The declaration carrierValues_subset is a machine-checked theorem stating that every value in this carrier belongs to rsField, a countable field built from the rationals together with the constants φ, π, e, and α⁻¹, closed under addition, multiplication, and inversion.

The theorem's proof is direct. Each expression in the carrier is built from a finite set of constants and operations. The theorem checks, case by case, that each constant lies in rsField and that each operation preserves membership. Since the field is countable, the theorem also implies the carrier itself is countable: only countably many finite expressions exist, so they can produce only countably many values. A companion theorem confirms the carrier is a proper subset of the real numbers, not the entire continuum.

The point of this result is scope. The framework does not claim to compute over every real number. It works with a countable, finitely generated set of values, which is enough for its calculations and proofs. This is a definitional choice about what the framework computes with, not a claim about the nature of the real numbers themselves.

The theorem does not say that rsField contains all numbers of interest, nor that the carrier equals the field. It establishes only one inclusion: carrier values sit inside rsField. It does not assert that every element of rsField is reachable by a carrier expression, nor that the constants φ, π, e, and α⁻¹ are algebraically independent. Those are separate questions, and the theorem leaves them open.

/-- The carrier value set sits inside `rsField`. -/
theorem carrierValues_subset : carrierValues ⊆ (MinimalField.rsField : Set ℝ) := by
  rintro x ⟨ex, rfl⟩
  exact eval_mem ex

/-- The carrier value set is countable: only countably many finite terms exist. -/
theorem carrierValues_countable : carrierValues.Countable :=
  (MinimalField.rsField_countable).mono carrierValues_subset

/-- The carrier values are a proper subset of ℝ. -/
theorem carrierValues_proper : carrierValues ≠ Set.univ := by
  intro h
  exact Cardinal.not_countable_real (h ▸ carrierValues_countable)

What this page does not claim

The carrier equals rsField, only that it is a subset of it. The constants φ, π, e, and α⁻¹ are algebraically independent or otherwise special beyond being in the inventory. The real numbers themselves are countable or otherwise different from their standard mathematical definition.

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/FRSCarrier.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: