Encyclopedia Foundation Foundation Primitive Recognition Calculus Delta Real Value Surjective
ARTICLE 4 claims 4 theorems
Foundation Primitive Recognition Calculus Delta Real Value Surjective
A machine-checked theorem shows that the framework's discrete approximation process can name every real number, not just a convenient subset.
Every real number is reachable
The real numbers are the continuum we use for lengths, times, and probabilities. A standard way to build them is through nested intervals: take a shrinking sequence of rational brackets, each one inside the last, whose widths tend to zero, and declare the real number to be the unique point they all contain. The Recognition Science framework builds its own version of this construction, called a protocol (a discrete record of shrinking rational intervals), and then asks which real numbers such protocols can represent.
The answer, proved in the framework's machine-checked library of formal theorems, is that every real number is representable. The theorem named value_surjective states that the function which reads off a protocol's limiting value hits every real number. The proof is constructive: for any real number r, there is a canonical protocol whose intervals close in on r, and the theorem verifies that this protocol's value is exactly r. This is not a claim that the framework has discovered a new kind of number; it is a guarantee that the framework's own bookkeeping language is as expressive as the classical real line.
This surjectivity result is a completeness property. It says the protocol representation does not silently omit any real value. Alongside it, the library also proves that the representation is faithful: two protocols are observationally equivalent exactly when they have the same value, and the arithmetic operations (addition, negation, subtraction) defined on protocols agree with the usual operations on the real numbers they represent. Taken together, these theorems show that the protocol calculus is a working model of the real numbers, not a fragment.
The value_surjective theorem does not claim that the canonical protocol is the only way to represent a real number, nor that it is the most efficient. It does not claim that every protocol converges to a distinct real, since many different protocols can share a value. It also does not claim anything about the physical meaning of the real numbers themselves; the theorem is about the internal consistency and coverage of the framework's formal language. What it establishes is a bridge: the discrete, finitely-specified protocols can span the whole continuous real line, so any real-valued quantity can in principle be expressed within the framework's ledger.
THEOREM value_surjective · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean
/-- `value` is surjective onto ℝ. -/
theorem value_surjective : Function.Surjective Protocol.value :=
fun r => ⟨canonical r, value_canonical r⟩
THEOREM value_canonical · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean
theorem value_canonical (r : ℝ) : (canonical r).value = r := by
symm
apply value_unique
intro n
have h2 : (0 : ℝ) < 2 ^ n := by positivity
have hflo : (⌊r * 2 ^ n⌋ : ℝ) ≤ r * 2 ^ n := Int.floor_le _
have hflo1 : r * 2 ^ n < (⌊r * 2 ^ n⌋ : ℝ) + 1 := Int.lt_floor_add_one _
constructor
· show (canonical r).lo n ≤ r
simp only [canonical, Protocol.lo]
push_cast
rw [div_le_iff₀ h2]
linarith
· show r ≤ (canonical r).hi n
simp only [canonical, Protocol.hi]
push_cast
rw [le_div_iff₀ h2]
linarith
THEOREM obsEq_iff_value · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean
/-- Observational equality is exactly equality of value. This is the central
faithfulness statement: the protocol distinguishes two reals iff their values
differ. -/
theorem obsEq_iff_value (x y : Protocol) : ObsEq x y ↔ x.value = y.value := by
constructor
· intro h
have hbound : ∀ n : ℕ, |x.value - y.value| ≤ 2 * (1 / ((n : ℝ) + 1)) := by
intro n
obtain ⟨hxy, hyx⟩ := h n
obtain ⟨hxl, hxr⟩ := x.value_mem n
obtain ⟨hyl, hyr⟩ := y.value_mem n
have hxw := x.width_real_bound n
have hyw := y.width_real_bound n
have ov1 : x.lo n ≤ y.hi n := by unfold Protocol.lo Protocol.hi; exact_mod_cast hxy
have ov2 : y.lo n ≤ x.hi n := by unfold Protocol.lo Protocol.hi; exact_mod_cast hyx
rw [abs_le]
constructor <;> linarith
have : |x.value - y.value| = 0 := by
apply tiny_le_zero (abs_nonneg _)
intro n
have hb := hbound (2 * n + 1)
have heq : 2 * (1 / ((↑(2 * n + 1) : ℝ) + 1)) = 1 / ((n : ℝ) + 1) := by
have hne : (n : ℝ) + 1 ≠ 0 := by positivity
push_cast
field_simp
ring
rw [heq] at hb
exact hb
have := abs_eq_zero.mp this
linarith
· intro h n
have hx := x.value_mem n
have hy := y.value_mem n
rw [h] at hx
refine ⟨?_, ?_⟩
· -- (x.approx n).lo ≤ (y.approx n).hi
have : x.lo n ≤ y.hi n := le_trans hx.1 (y.value_le_hi n)
unfold Protocol.lo Protocol.hi at this; exact_mod_cast this
· -- (y.approx n).lo ≤ (x.approx n).hi
have h1 := hy.1 -- y.lo n ≤ y.value
have h2 := hx.2 -- y.value ≤ x.hi n
have : y.lo n ≤ x.hi n := by linarith
unfold Protocol.lo Protocol.hi at this; exact_mod_cast this
THEOREM value_add · value_neg · value_sub · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean
theorem value_add (x y : Protocol) : (add x y).value = x.value + y.value := by
symm
apply value_unique
intro n
refine ⟨?_, ?_⟩
· show (add x y).lo n ≤ x.value + y.value
unfold Protocol.lo add
simp only
have hx := x.lo_le_value (2 * n + 1)
have hy := y.lo_le_value (2 * n + 1)
unfold Protocol.lo at hx hy
push_cast
linarith
· show x.value + y.value ≤ (add x y).hi n
unfold Protocol.hi add
simp only
have hx := x.value_le_hi (2 * n + 1)
have hy := y.value_le_hi (2 * n + 1)
unfold Protocol.hi at hx hy
push_cast
linarith
theorem value_neg (x : Protocol) : (neg x).value = -x.value := by
symm
apply value_unique
intro n
refine ⟨?_, ?_⟩
· show (neg x).lo n ≤ -x.value
unfold Protocol.lo neg
simp only
have := x.value_le_hi n
unfold Protocol.hi at this
push_cast; linarith
· show -x.value ≤ (neg x).hi n
unfold Protocol.hi neg
simp only
have := x.lo_le_value n
unfold Protocol.lo at this
push_cast; linarith
theorem value_sub (x y : Protocol) : (sub x y).value = x.value - y.value := by
unfold sub
rw [value_add, value_neg]
ring
What this page does not claim
The theorem does not claim that every real number has a unique protocol representation. The theorem does not claim that the protocol construction is computationally efficient or practical for numerical work. The theorem does not assign any physical or metaphysical significance to the real numbers themselves.
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/DeltaReal.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:
- How does the protocol construction relate to the classical Dedekind cut or Cauchy sequence definitions of the reals?
- What role does the surjectivity result play in the framework's derivation of physical constants?
- Does the protocol representation offer any computational advantage over standard real-number representations?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM value_surjective · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean
/-- `value` is surjective onto ℝ. -/ theorem value_surjective : Function.Surjective Protocol.value := fun r => ⟨canonical r, value_canonical r⟩The theorem named value_surjective states that the function which reads off a protocol's limiting value hits every real number. value_surjective · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.leanTHEOREM value_canonical · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean
theorem value_canonical (r : ℝ) : (canonical r).value = r := by symm apply value_unique intro n have h2 : (0 : ℝ) < 2 ^ n := by positivity have hflo : (⌊r * 2 ^ n⌋ : ℝ) ≤ r * 2 ^ n := Int.floor_le _ have hflo1 : r * 2 ^ n < (⌊r * 2 ^ n⌋ : ℝ) + 1 := Int.lt_floor_add_one _ constructor · show (canonical r).lo n ≤ r simp only [canonical, Protocol.lo] push_cast rw [div_le_iff₀ h2] linarith · show r ≤ (canonical r).hi n simp only [canonical, Protocol.hi] push_cast rw [le_div_iff₀ h2] linarithfor any real number r, there is a canonical protocol whose intervals close in on r, and the theorem verifies that this protocol's value is exactly r. value_canonical · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.leanTHEOREM obsEq_iff_value · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean
/-- Observational equality is exactly equality of value. This is the central faithfulness statement: the protocol distinguishes two reals iff their values differ. -/ theorem obsEq_iff_value (x y : Protocol) : ObsEq x y ↔ x.value = y.value := by constructor · intro h have hbound : ∀ n : ℕ, |x.value - y.value| ≤ 2 * (1 / ((n : ℝ) + 1)) := by intro n obtain ⟨hxy, hyx⟩ := h n obtain ⟨hxl, hxr⟩ := x.value_mem n obtain ⟨hyl, hyr⟩ := y.value_mem n have hxw := x.width_real_bound n have hyw := y.width_real_bound n have ov1 : x.lo n ≤ y.hi n := by unfold Protocol.lo Protocol.hi; exact_mod_cast hxy have ov2 : y.lo n ≤ x.hi n := by unfold Protocol.lo Protocol.hi; exact_mod_cast hyx rw [abs_le] constructor <;> linarith have : |x.value - y.value| = 0 := by apply tiny_le_zero (abs_nonneg _) intro n have hb := hbound (2 * n + 1) have heq : 2 * (1 / ((↑(2 * n + 1) : ℝ) + 1)) = 1 / ((n : ℝ) + 1) := by have hne : (n : ℝ) + 1 ≠ 0 := by positivity push_cast field_simp ring rw [heq] at hb exact hb have := abs_eq_zero.mp this linarith · intro h n have hx := x.value_mem n have hy := y.value_mem n rw [h] at hx refine ⟨?_, ?_⟩ · -- (x.approx n).lo ≤ (y.approx n).hi have : x.lo n ≤ y.hi n := le_trans hx.1 (y.value_le_hi n) unfold Protocol.lo Protocol.hi at this; exact_mod_cast this · -- (y.approx n).lo ≤ (x.approx n).hi have h1 := hy.1 -- y.lo n ≤ y.value have h2 := hx.2 -- y.value ≤ x.hi n have : y.lo n ≤ x.hi n := by linarith unfold Protocol.lo Protocol.hi at this; exact_mod_cast thistwo protocols are observationally equivalent exactly when they have the same value obsEq_iff_value · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.leanTHEOREM value_add · value_neg · value_sub · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean
theorem value_add (x y : Protocol) : (add x y).value = x.value + y.value := by symm apply value_unique intro n refine ⟨?_, ?_⟩ · show (add x y).lo n ≤ x.value + y.value unfold Protocol.lo add simp only have hx := x.lo_le_value (2 * n + 1) have hy := y.lo_le_value (2 * n + 1) unfold Protocol.lo at hx hy push_cast linarith · show x.value + y.value ≤ (add x y).hi n unfold Protocol.hi add simp only have hx := x.value_le_hi (2 * n + 1) have hy := y.value_le_hi (2 * n + 1) unfold Protocol.hi at hx hy push_cast linariththeorem value_neg (x : Protocol) : (neg x).value = -x.value := by symm apply value_unique intro n refine ⟨?_, ?_⟩ · show (neg x).lo n ≤ -x.value unfold Protocol.lo neg simp only have := x.value_le_hi n unfold Protocol.hi at this push_cast; linarith · show -x.value ≤ (neg x).hi n unfold Protocol.hi neg simp only have := x.lo_le_value n unfold Protocol.lo at this push_cast; linariththeorem value_sub (x y : Protocol) : (sub x y).value = x.value - y.value := by unfold sub rw [value_add, value_neg] ringthe arithmetic operations (addition, negation, subtraction) defined on protocols agree with the usual operations on the real numbers they represent. value_add · value_neg · value_sub · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean