Foundation Primitive Recognition Calculus Valid Comparison Compose

The comparison bridge

A comparison bridge is a formal way to say that one object can stand in for another. The setup has three kinds of objects: native objects, which are the originals; display objects, which are the stand-ins; and observable objects, which are the results of a measurement. A bridge pairs each native object with a display object, and it also pairs each native object with an observable result. The bridge is valid when observing the display gives the same result as observing the native object directly. In symbols, for every native object n, observeDisplay (display n) = observeNative n.

The key theorem about bridges is that a comparison made through a display is legitimate exactly when it agrees with a comparison made directly on the native objects. If two native objects produce the same observable result through the bridge, then they also produce the same observable result when measured natively, and the reverse holds as well. This is not a matter of approximation or convention. It is a proved equivalence: a display comparison is valid if and only if it descends to equality of the native observable protocol.

The declaration compose extends this idea from one bridge to a chain of bridges. Suppose a native object is first displayed in one format, and that display is then displayed again in a second format. The composite bridge sends the native object straight to the second display. The composition law says that if each bridge in the chain commutes with the observable protocol, then the composite bridge is also valid. The proof is short: the second bridge's commuting law applies to the first bridge's display output. The resulting theorem states that a valid comparison through the composite bridge is equivalent to comparing the intermediate displays through the second bridge's native observation.

What this establishes in plain terms is a stability property. If a comparison is legitimate in one display format, it remains legitimate when that format is itself displayed in another format. The validity of a comparison does not depend on which display layer you look through, as long as every layer obeys the same observable protocol. The framework's library of formal theorems records this as the valid comparison doctrine: legitimacy descends to native equality, and that legitimacy is stable under composition of display bridges.

What compose does not claim is just as important. It does not say that any two displays of the same native object are interchangeable in every context. It says only that they agree on the observable protocol that the bridge specifies. If a different observable is chosen, the bridge must be rebuilt. The declaration also does not claim that every native object has a display, or that displays are unique. It defines a structure and proves a property about that structure. It does not assert that the structure exists for any particular pair of types.

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]

/-- Bridge composition: if a native-to-display bridge and a display-to-display
bridge both commute with the observable protocol, the composite bridge is valid. -/
def compose {N D E O : Type*} (B₁ : Bridge N D O) (B₂ : Bridge D E O) : Bridge N E O where
  display := B₂.display ∘ B₁.display
  observeNative := B₂.observeNative ∘ B₁.display
  observeDisplay := B₂.observeDisplay
  commutes := by
    intro n
    exact B₂.commutes (B₁.display n)

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 declaration does not prove that any particular pair of types has a bridge. It does not claim that displays are unique or that all observables agree. It does not establish that a bridge exists for physical recognition events.

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: