Foundation Primitive Recognition Calculus Frscarrier Carrier Values Proper

The finite carrier

The real numbers are uncountable: there are so many of them that no list, no matter how infinite, can contain them all. The framework Recognition Science works with a much smaller, explicitly describable collection. Its carrier, the set of values it actually computes on, is built from a finite list of starting constants (the golden ratio, pi, Euler's number e, and the inverse fine-structure constant) plus the rational numbers, combined by the ordinary field operations of addition, multiplication, negation, and reciprocal. This is a finite-description syntax: every term is a finite expression, so only countably many distinct terms exist.

The theorem carrierValues_proper states that this carrier value set is a proper subset of the real numbers: it is not equal to the whole of ℝ. The proof is a short argument by contradiction. If the carrier were all of ℝ, then since the carrier is countable (a separate theorem, carrierValues_countable), the reals would be countable. But a standard result of set theory, Cardinal.not_countable_real, says the reals are uncountable. Contradiction. The machine-checked library of formal theorems records both the countability result and the proper-subset conclusion, and the whole chain is verified by the Lean kernel with no framework-specific axioms.

The consequence is that the framework's computations never leave a countable field. Every carrier term evaluates inside a specific countable field called rsField, and the carrier sits inside it. This is a soundness guarantee: the finite-description syntax cannot escape into the uncountable continuum. The framework models its physical quantities as values in this countable carrier, not as arbitrary real numbers. That is a definitional choice about what the framework computes on; the theorems prove the carrier is countable and proper, but they do not prove that this carrier is the right or only way to model physical quantities.

What the theorem does not claim is just as important. It does not say that the carrier contains all numbers the framework will ever need, nor that every real number of physical interest is a carrier value. It does not assert that the inverse fine-structure constant is a derived constant; alphaInv is simply an inventory item, an identification, not a derivation. The theorem is silent on whether the carrier is closed under other operations, such as exponentiation or trigonometric functions. It proves a negative property (not all reals are in the carrier) and a size property (countable), nothing more.

The practical upshot is that the framework's ledger of computable values is a sparse, enumerable grid inside the continuum, not the continuum itself. Every value the framework actually uses has a finite description and a protocol display in the Delta-real interface. That is a strong finiteness guarantee for a framework that claims to derive physical constants, but it is a guarantee about the size of the value set, not about which specific numbers are included or whether the inventory is complete.

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

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

/-- **Soundness.** Every carrier term evaluates into the countable field `rsField`.
The finite-description syntax never escapes the carrier. -/
theorem eval_mem (ex : FRSExpr) : eval ex ∈ MinimalField.rsField := by
  induction ex with
  | rat q => exact SubfieldClass.ratCast_mem MinimalField.rsField q
  | phi => simpa [eval] using MinimalField.rsField_mem_phi
  | pi => simpa [eval] using MinimalField.rsField_mem_pi
  | e => simpa [eval] using MinimalField.rsField_mem_e
  | alphaInv => simpa [eval] using MinimalField.rsField_mem_alphaInv
  | neg a ih => simpa [eval] using neg_mem ih
  | add a b iha ihb => simpa [eval] using add_mem iha ihb
  | mul a b iha ihb => simpa [eval] using mul_mem iha ihb
  | inv a ih => simpa [eval] using inv_mem ih

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

/-- **Phase 3 headline.** The F_RS carrier is an explicit finite-description
syntax: every term evaluates into the countable field `rsField` (soundness), the
constant inventory (φ, π, e, α⁻¹) and the rationals are terms, the term values are
countable and a proper subset of ℝ, and every term value has a protocol display in
the `ℝδ` interface. The carrier the framework actually computes on is finite
generation over a fixed inventory, not the uncountable continuum. -/
theorem frs_carrier :
    (∀ ex : FRSExpr, eval ex ∈ MinimalField.rsField)
      ∧ eval FRSExpr.phi = Real.goldenRatio
      ∧ eval FRSExpr.pi = Real.pi
      ∧ eval FRSExpr.e = Real.exp 1
      ∧ eval FRSExpr.alphaInv = MinimalField.alphaInv
      ∧ carrierValues.Countable
      ∧ carrierValues ≠ Set.univ
      ∧ (∀ ex : FRSExpr, ∃ x : DeltaReal.Protocol, x.value = eval ex) :=
  ⟨eval_mem, phi_is_term, pi_is_term, e_is_term, alphaInv_is_term,
    carrierValues_countable, carrierValues_proper, has_protocol_display⟩

What this page does not claim

The carrier contains all real numbers of physical interest. The inverse fine-structure constant is derived rather than identified as an inventory item. The carrier is closed under operations beyond the field operations listed in the syntax.

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: