Foundation Primitive Recognition Calculus Valid Comparison Bridge

The bridge

A bridge is a formal contract between three kinds of object: a native object, a display object, and an observable object. In plain terms, the native object is the real thing you care about, the display is a representation of it (a picture, a number, a diagram), and the observable is the feature you want to compare. The bridge supplies two functions: one turns a native object into a display, and another turns a display into an observable. The key requirement is a commuting law: observing the display gives exactly the same result as observing the native object directly. Think of a thermometer: the native object is the gas temperature, the display is the mercury height, and the observable is the number on the scale. The bridge says the scale reading you get from the mercury is the same as the temperature you would measure directly.

The bridge then defines what makes a comparison valid. Two native objects are considered to compare validly when their displays, after being observed, produce equal observable values. The central theorem, proved in the machine-checked library of formal theorems, states that this display-based comparison is equivalent to comparing the native observables directly: the displayed comparison holds exactly when the native observations are equal. This is not a heuristic or an approximation; it is a logical equivalence. The theorem also shows the property is stable under composition: if you chain a native-to-display bridge with a display-to-display bridge, the composite bridge remains valid, and the same equivalence holds for the composite.

In Recognition Science, the bridge is a primitive tool for comparing recognition events. The framework models reality as a ledger, a discrete record of events, and the bridge lets one compare events through a display carrier without losing the ground truth of the native observable protocol. The doctrine that emerges is precise: a comparison in a display carrier is legitimate exactly when it descends to equality of the native observable protocol, and this legitimacy survives composition of display bridges. That doctrine is what the declaration establishes.

What the bridge does not claim is equally important. It does not assert that any particular display is faithful; it merely defines the condition under which a display comparison is valid. It does not say that all native objects have displays, nor that all observables are comparable. It does not prove that any specific physical system satisfies the bridge; it provides the contract that such a system must meet. The bridge is a definitional scaffold, not a physical law. It gives the framework a clean way to say when a comparison is trustworthy, and it proves that trustworthiness is preserved when bridges are composed.

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 bridge does not assert that any particular display is faithful or that all native objects have displays. The bridge does not prove that any specific physical system satisfies the commuting law. The bridge does not derive any physical constant or empirical value.

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: