Encyclopedia Foundation Foundation Primitive Recognition Calculus Delta Real Display Real Forgetful

ARTICLE 6 claims 6 theorems

Foundation Primitive Recognition Calculus Delta Real Display Real Forgetful

A single machine-checked theorem collects the basic facts about how the framework's real numbers behave, and it proves nothing about the physical world.

Verify this page

The display theorem

The declaration display_real_forgetful is a theorem in the framework's machine-checked library of formal theorems. It assembles six already-proved facts about a structure called Protocol, which is the framework's discrete record of nested rational intervals that shrink toward a real number. The theorem states these facts together, as a single package, rather than proving anything new on its own.

The six facts are the basic algebraic and observational properties of this construction. First, every real number is the value of some Protocol: the map from protocols to real numbers is surjective. Second, a protocol built from a rational number has that rational as its value. Third, two protocols are observationally equivalent, meaning their intervals overlap at every stage, exactly when they have the same real value. Fourth, addition of protocols corresponds to addition of their real values. Fifth, negation of a protocol corresponds to negation of its value. Sixth, subtraction of protocols corresponds to subtraction of their values.

These facts are proved in the Lean 4 proof assistant, and the theorem display_real_forgetful is itself a proved statement in that system, with no unproved axioms beyond the standard ones the ambient type theory supplies. The name "forgetful" signals that the theorem records what the framework's real-number construction does, without claiming anything about what it is for. It is a display of internal consistency, not a bridge to physics.

What the theorem does not claim is just as important as what it proves. It does not say that the real numbers are the only way to model physical quantities. It does not say that the Protocol construction is the only way to build real numbers, nor that the framework's real numbers are the same as the classical real numbers in every respect. It only states the six algebraic and observational facts above, nothing more.

THEOREM display_real_forgetful · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean
display_real_forgetful · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean:457 
/-- **Phase 1 headline.** The classical real line is the forgetful value of a
Delta-real protocol. Concretely:

1. every real is the value of a protocol (`value_surjective`);
2. the rational embedding `ofRat` has `value (ofRat q) = q`, so ℚ sits inside;
3. observational equality of protocols is exactly equality of value
   (`obsEq_iff_value`), so the presentation is faithful;
4. the protocol operations are native interval rules whose value is a ring
   homomorphism (`value_add`, `value_neg`, `value_sub`).

So ℝ is not a primitive completed object here; it is recovered as the value
display of refinement protocols, and nothing in analysis needs more than the
protocol that produces rational data to any requested precision. -/
theorem display_real_forgetful :
    Function.Surjective Protocol.value
      ∧ (∀ q : ℚ, (ofRat q).value = (q : ℝ))
      ∧ (∀ x y : Protocol, ObsEq x y ↔ x.value = y.value)
      ∧ (∀ x y : Protocol, (add x y).value = x.value + y.value)
      ∧ (∀ x : Protocol, (neg x).value = -x.value)
      ∧ (∀ x y : Protocol, (sub x y).value = x.value - y.value) :=
  ⟨value_surjective, value_ofRat, obsEq_iff_value, value_add, value_neg, value_sub⟩
THEOREM display_real_forgetful · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean
display_real_forgetful · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean:457 
/-- **Phase 1 headline.** The classical real line is the forgetful value of a
Delta-real protocol. Concretely:

1. every real is the value of a protocol (`value_surjective`);
2. the rational embedding `ofRat` has `value (ofRat q) = q`, so ℚ sits inside;
3. observational equality of protocols is exactly equality of value
   (`obsEq_iff_value`), so the presentation is faithful;
4. the protocol operations are native interval rules whose value is a ring
   homomorphism (`value_add`, `value_neg`, `value_sub`).

So ℝ is not a primitive completed object here; it is recovered as the value
display of refinement protocols, and nothing in analysis needs more than the
protocol that produces rational data to any requested precision. -/
theorem display_real_forgetful :
    Function.Surjective Protocol.value
      ∧ (∀ q : ℚ, (ofRat q).value = (q : ℝ))
      ∧ (∀ x y : Protocol, ObsEq x y ↔ x.value = y.value)
      ∧ (∀ x y : Protocol, (add x y).value = x.value + y.value)
      ∧ (∀ x : Protocol, (neg x).value = -x.value)
      ∧ (∀ x y : Protocol, (sub x y).value = x.value - y.value) :=
  ⟨value_surjective, value_ofRat, obsEq_iff_value, value_add, value_neg, value_sub⟩
THEOREM value_surjective · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean
value_surjective · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean:451 
/-- `value` is surjective onto ℝ. -/
theorem value_surjective : Function.Surjective Protocol.value :=
  fun r => ⟨canonical r, value_canonical r⟩
THEOREM value_ofRat · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean
value_ofRat · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean:235 
@[simp] theorem value_ofRat (q : ℚ) : (ofRat q).value = (q : ℝ) := by
  unfold value Protocol.lo ofRat
  simp
THEOREM obsEq_iff_value · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean
obsEq_iff_value · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean:167 
/-- 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 display_real_forgetful · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean
display_real_forgetful · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean:457 
/-- **Phase 1 headline.** The classical real line is the forgetful value of a
Delta-real protocol. Concretely:

1. every real is the value of a protocol (`value_surjective`);
2. the rational embedding `ofRat` has `value (ofRat q) = q`, so ℚ sits inside;
3. observational equality of protocols is exactly equality of value
   (`obsEq_iff_value`), so the presentation is faithful;
4. the protocol operations are native interval rules whose value is a ring
   homomorphism (`value_add`, `value_neg`, `value_sub`).

So ℝ is not a primitive completed object here; it is recovered as the value
display of refinement protocols, and nothing in analysis needs more than the
protocol that produces rational data to any requested precision. -/
theorem display_real_forgetful :
    Function.Surjective Protocol.value
      ∧ (∀ q : ℚ, (ofRat q).value = (q : ℝ))
      ∧ (∀ x y : Protocol, ObsEq x y ↔ x.value = y.value)
      ∧ (∀ x y : Protocol, (add x y).value = x.value + y.value)
      ∧ (∀ x : Protocol, (neg x).value = -x.value)
      ∧ (∀ x y : Protocol, (sub x y).value = x.value - y.value) :=
  ⟨value_surjective, value_ofRat, obsEq_iff_value, value_add, value_neg, value_sub⟩

What this page does not claim

The theorem does not prove that the Protocol construction is unique or canonical. The theorem does not establish any physical law or empirical fact. The theorem does not define what a real number is; it assumes the classical real numbers as given.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND