Foundation Primitive Recognition Calculus Valid Comparison Valid Comparison Comp

Composing comparisons

A ledger, a discrete record of events, often needs to present its entries in more than one form. A native object might be a raw internal state, a display object a formatted report, and an observable object the actual quantity a reader cares about. A bridge is the translation between two such forms, with one guarantee: observing the display gives the same answer as observing the native object directly. The declaration validComparison_compose proves that this guarantee survives chaining. If a first bridge translates native objects into a display, and a second bridge translates that display into yet another form, then the combined translation is again a valid bridge. A comparison made in the final display is legitimate exactly when the underlying native observables agree.

The proof is short because the setup is deliberately spare. Each bridge carries a commuting law: for every native object, observing the displayed version equals observing the original. Composing two bridges means applying one translation after the other, and the commuting laws line up so that the outer observation still matches the innermost native value. The theorem states this as an equivalence: a displayed comparison is valid if and only if the native observable values are equal. The same statement holds for the single-bridge case, and the composition theorem extends it to chains of arbitrary length. This is the property that makes comparisons trustworthy across multiple layers of representation.

In Recognition Science, this result anchors the valid comparison doctrine: a comparison in any 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. The doctrine is a theorem in the machine-checked library of formal theorems, proved from the structure definitions alone. It does not say which observable protocol is correct, what a native object is, or how bridges are constructed in practice. It only guarantees that once two bridges are valid, their composite is valid too. That is the load-bearing fact: translation errors do not accumulate when each step is faithful.

The practical consequence is that layered systems, where raw data passes through several formatting or transmission stages, preserve the integrity of comparisons if each stage individually preserves it. A reader can trust a final displayed comparison without re-checking every intermediate translation, provided the bridges were valid at each step. The theorem does not claim that any particular bridge is valid, nor that validity is automatic. It is a conditional guarantee, and its value lies in making that condition explicit and composable.

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

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

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

No particular bridge is asserted to be valid. The theorem does not define what counts as a native object or an observable protocol. It does not claim that validity is automatic or that any specific translation is faithful.

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: