Foundation Primitive Recognition Calculus Delta Real Of Rat Obs Eq Iff

The rational identity test

The real numbers are often built by approximation: a real number is a rule that, for each desired precision, produces a rational interval containing the number. The framework's ledger, a discrete record of events, uses this same idea. A protocol is such a rule: for each step n, it gives a rational interval, with intervals shrinking as n grows, and the width of the interval at step n is at most 1/(n+1). The real value of a protocol is the unique real number that lies inside every interval it produces.

Two protocols are observationally equal when, at every step n, their intervals overlap. This is a natural way to say that two approximation rules describe the same real number. The framework proves that this observational equality matches exact equality of values: two protocols are observationally equal if and only if their real values are equal. For rational numbers, this becomes a clean identity test. A rational number q, when fed into the construction, becomes a protocol whose intervals are all the single point q. The theorem ofRat_obsEq_iff states that two such rational protocols are observationally equal exactly when the rational numbers themselves are equal.

This is not a deep fact about the real numbers; it is a sanity check on the construction. The framework's library of machine-checked formal theorems verifies that its approximation-based reals behave correctly on the rationals. The theorem confirms that the observational notion of equality, which is what the framework actually uses, does not collapse distinct rational numbers into one. It is the first step in showing that the construction is faithful: distinct rationals stay distinct, and the map from rationals into the protocols is injective.

The result matters because the framework builds its real numbers from these protocols, and later results about addition, negation, and subtraction all rely on the value function. The identity test for rationals is a base case that keeps the whole tower honest. It is not a claim about irrational numbers, about the cost function, or about the structure of physical space. It is a small, precise guarantee about the foundation.

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

/-- The rational embedding is faithful: two rational protocols are observationally
equal iff the rationals are equal. -/
theorem ofRat_obsEq_iff (q r : ℚ) : ObsEq (ofRat q) (ofRat r) ↔ q = r := by
  rw [obsEq_iff_value, value_ofRat, value_ofRat]
  exact_mod_cast Iff.rfl

What this page does not claim

This theorem does not establish any property of irrational numbers. This theorem does not derive the cost function or any physical constant. This theorem does not claim that the framework's real numbers are the only possible construction.

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: