Foundation Primitive Recognition Calculus Delta Real Value Canonical

The canonical representation

A real number such as π or √2 is usually thought of as a point on a continuous line. The framework's ledger, a discrete record of events, instead represents a real number by an infinite sequence of nested rational intervals, each one a pair of fractions bracketing the number. The intervals shrink as the sequence advances, and their width is guaranteed to fall below 1/(n+1) after n steps.

The declaration value_canonical proves a completeness property: for any real number r, there is a protocol whose value is exactly r. The construction, called canonical, builds the sequence by taking the dyadic rationals ⌊r·2^n⌋/2^n as lower bounds and (⌊r·2^n⌋+1)/2^n as upper bounds. This is the standard binary expansion of r, written as nested intervals. The theorem value_canonical states that the value of this protocol equals r, and the companion theorem value_unique shows that any protocol whose intervals all contain y must have value y. Together they imply that every real number has a canonical representation in the ledger, and that the representation is unique.

This is not a numerical approximation scheme. The protocol is an infinite object, and its value is defined as the limit of the lower bounds. The theorem is a statement about the real numbers themselves, not about computing them to finite precision. The construction is noncomputable in the sense that it requires choosing floors of arbitrary real numbers, but the existence and uniqueness are fully proved.

In Recognition Science, this result grounds the claim that the ledger can represent every real number. The recognition events, the individual observations, are the rational intervals; the real number is what they converge to. The theorem value_canonical is the bridge from the discrete ledger to the continuous real line, showing that nothing is lost in the representation.

The practical consequence is that the framework's arithmetic on protocols, with addition, negation, and subtraction, is faithful to real arithmetic. The theorem value_add states that the value of the sum of two protocols equals the sum of their values, and similarly for negation and subtraction. This means the ledger's operations mirror the real numbers exactly, not approximately.

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

/-- Squeeze: any real in every interval equals the value. -/
theorem value_unique (x : Protocol) (y : ℝ)
    (hy : ∀ n, x.lo n ≤ y ∧ y ≤ x.hi n) : y = x.value := by
  have hbound : ∀ n : ℕ, |y - x.value| ≤ 1 / (n + 1) := by
    intro n
    obtain ⟨h1l, h1r⟩ := hy n
    obtain ⟨h2l, h2r⟩ := x.value_mem n
    have hw := x.width_real_bound n
    rw [abs_le]
    constructor <;> linarith
  have : |y - x.value| = 0 := tiny_le_zero (abs_nonneg _) hbound
  have := abs_eq_zero.mp this
  linarith

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

What this page does not claim

The theorem does not claim that the canonical protocol is computable in finite time. It does not claim that the ledger's representation of real numbers is physically realized in nature. It does not claim that every real number is a recognition event; the protocol is a mathematical object, not a physical one.

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: