Foundation Primitive Recognition Calculus Valid Comparison Valid Comparison Iff

What a valid comparison is

In many sciences you never observe a thing directly; you observe a display of it. A thermometer shows a column of mercury, a screen shows pixels, a ledger shows entries. The question is when two displays can be trusted to mean the same thing about the things behind them. The declaration valid comparison answers that: a comparison of two displayed values is legitimate exactly when the two native objects, observed through their own protocol, are equal. The display is a faithful messenger, and the test of faithfulness is that it never reports agreement where the native objects disagree, and never hides disagreement where they agree.

The formal statement, in the framework's machine-checked library of formal theorems, is a bridge structure. A bridge carries three maps: a display map from native object to display object, an observe-native map from native object to observable, and an observe-display map from display to observable. The bridge is valid when the two observation routes agree for every native object: observing the display gives the same result as observing the native directly. The theorem validComparison_iff_native then proves that a comparison of two displayed values is valid if and only if the two native observations are equal. The proof is a short rewrite using the bridge's commuting law; it is a theorem, not a definitional choice.

The same theorem composes. If a native-to-display bridge and a display-to-display bridge both commute with the observable protocol, then the composite bridge is valid, and the comparison doctrine holds: legitimacy descends to native equality and is stable under composition. In plain terms, you can chain displays, as from a sensor to a screen to a photograph, and the comparison remains trustworthy as long as every link in the chain is faithful. The framework calls this the valid comparison doctrine, and it is what lets the framework treat displayed observations as evidence about native objects.

What the theorem does not claim is just as important. It does not say that any particular display is accurate; it says only what validity means once a bridge is given. It does not claim that native equality is observable; the theorem is about the equivalence of two comparison criteria, not about whether observations can be made. And it does not claim that the display map is injective: two different native objects may display the same value, and the theorem is silent on that. The doctrine is a criterion, not a guarantee of discriminative power.

theorem validComparison_iff_native {N D O : Type*} (B : Bridge N D O) (x y : N) :
    IsValidComparison B x y ↔ B.observeNative x = B.observeNative y := by
  unfold IsValidComparison
  rw [B.commutes x, B.commutes y]

theorem validComparison_compose {N D E O : Type*}
    (B₁ : Bridge N D O) (B₂ : Bridge D E O) (x y : N) :
    IsValidComparison (compose B₁ B₂) x y ↔ B₂.observeNative (B₁.display x) = B₂.observeNative (B₁.display y) :=
  validComparison_iff_native (compose B₁ B₂) x y

/-- **Valid comparison doctrine.** A comparison in a display carrier is legitimate
exactly when it descends to equality of the native observable protocol, and this
legitimacy is stable under composition of display bridges. -/
theorem valid_comparison_doctrine {N D E O : Type*}
    (B₁ : Bridge N D O) (B₂ : Bridge D E O) :
    (∀ x y : N, IsValidComparison B₁ x y ↔ B₁.observeNative x = B₁.observeNative y)
      ∧ (∀ x y : N, IsValidComparison (compose B₁ B₂) x y
          ↔ B₂.observeNative (B₁.display x) = B₂.observeNative (B₁.display y)) :=
  ⟨validComparison_iff_native B₁, validComparison_compose B₁ B₂⟩

What this page does not claim

The theorem does not claim that any particular display is accurate. The theorem does not claim that native equality is observable. The theorem does not claim that the display map is injective.

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/ValidComparison.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: