Foundation Primitive Recognition Calculus Delta Real Obs Eq Iff Value

When observations agree

A real number is often described by a nested sequence of shrinking rational intervals, each one a closer approximation. In the Recognition Science framework, such a sequence is called a protocol: a discrete record of events, here the successive rational bounds. Two protocols are observationally equal when, at every finite stage, their intervals overlap. The framework's machine-checked library of formal theorems establishes a clean equivalence: two protocols are observationally equal exactly when they have the same real value. This is the theorem obsEq_iff_value, and it is proved in full formal detail.

The theorem is a bridge between two ways of comparing real numbers. One way is operational: you look at the finite data, the intervals at each step, and ask whether they ever separate. The other is mathematical: you take the limit, the unique real number each protocol converges to, and compare those. The theorem says these two notions coincide. If two protocols agree observationally at every finite stage, they converge to the same real; conversely, if they converge to the same real, no finite stage can separate them. This is not an approximation or a heuristic; it is a proved equivalence, with no unproved assumptions beyond the standard foundations of the proof system.

The theorem also gives a precise sense in which the framework's protocols are not redundant. Every real number has at least one protocol that converges to it, and rational numbers have protocols that are exact at every stage. The equivalence then says that the observational data, the overlapping intervals, carries exactly the information of the real value. Two protocols that look different in the written record but agree observationally are, for the framework's purposes, the same object. This is what makes the theorem load-bearing: it justifies treating protocols as a working representation of real numbers, where equality of values and equality of observations are interchangeable.

What the theorem does not claim is just as important. It does not say that observational equality is decidable, that you can always tell in finite time whether two protocols agree. It does not say that every real number can be observed exactly, only that each real has a protocol converging to it. And it does not say that the framework's protocols are the only way to represent real numbers, or that they replace the standard construction. The theorem is a precise statement about one specific representation, and its power comes from that precision.

For a reader meeting the framework for the first time, the consequence is simple: within this calculus, what you can observe and what is true are the same thing. The theorem is a formal guarantee that the framework's observational language is faithful to the mathematics it describes. That faithfulness is what allows the framework to build further results on top of this foundation, from the cost function to the golden ratio, without worrying that the representation is leaking or distorting the underlying reality.

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

@[simp] theorem value_ofRat (q : ℚ) : (ofRat q).value = (q : ℝ) := by
  unfold value Protocol.lo ofRat
  simp

What this page does not claim

Observational equality is decidable in finite time. Every real number can be observed exactly, rather than approximated by a converging protocol. The protocol representation replaces the standard construction of real numbers.

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: