Foundation Primitive Recognition Calculus Delta Real

The delta real protocol

The real numbers are usually introduced as a complete ordered field, but recognition, the discrete record of events that Recognition Science starts from, needs a more constructive picture. Delta real provides that picture: it defines a real number as a protocol, a sequence of closed rational intervals that shrink toward a single point. Each protocol carries three guarantees: the intervals are nested, each one contains the next; their widths shrink to zero at a controlled rate, at most 1/(n+1) for the n-th interval; and every interval is a closed rational interval, with rational endpoints and a lower bound no greater than its upper bound. The value of a protocol is the unique real number that lies in every interval, and the construction proves that this value exists and is unique.

The construction is not just a definition; it is a working arithmetic. The construction defines addition, negation, and subtraction on protocols, and proves that these operations respect the underlying real values. Adding two protocols yields a protocol whose value is the sum of the two values, and similarly for negation and subtraction. It also proves that every rational number embeds as a constant protocol, and that every real number can be represented by some protocol, so the map from protocols to reals is surjective. The key theorem, value_unique, states that if any real number lies in all intervals of a protocol, then that number is exactly the protocol's value, which is what makes the representation well-defined.

The construction also introduces an equivalence relation, ObsEq, which holds between two protocols when their intervals overlap at every stage. This is a finer notion than having the same value, and the construction proves that the two notions coincide: two protocols are observationally equivalent if and only if they have the same real value. This equivalence is then used to build a setoid, a structure that allows protocols to be treated as equal when they are observationally indistinguishable. This is the sense in which the construction is a real number system: it identifies all protocols that pin down the same point on the line.

In Recognition Science, this construction establishes the ground layer of the framework's calculus. It provides a rigorous, machine-checked foundation for the real numbers that does not rely on an abstract axiom of completeness, but instead builds the reals from a discrete, finitary process of interval refinement. This is the substrate on which the framework's cost function, the golden ratio, and the forcing chain are later developed. The construction's theorems are all proved in the framework's machine-checked library of formal theorems, with no unproved assumptions beyond the standard axioms of the underlying type theory.

The practical consequence is that every real number used in the framework, from the cost function's values to the constants that emerge from the forcing chain, can be traced back to a concrete protocol of rational intervals. This means that every claim about real numbers in the framework is ultimately a claim about rational arithmetic, which is finitary and checkable. The delta real construction is thus not a mere convenience; it is the bridge that lets the framework's discrete starting point support the continuous mathematics it needs.

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

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

/-- `value` is surjective onto ℝ. -/
theorem value_surjective : Function.Surjective Protocol.value :=
  fun r => ⟨canonical r, value_canonical r⟩

What this page does not claim

This construction does not prove the existence of the real numbers as a complete ordered field; it constructs a representation from rational intervals. This construction does not define the cost function or any other framework-specific structure; it only provides the real number substrate. The ObsEq equivalence is not claimed to be the same as equality of protocols; it is a coarser relation that identifies protocols with the same value.

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: