Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparisonExamples

show as:
view Lean formalization →

Worked examples that instantiate the valid-comparison interface for three standard displays of Delta protocols: real value, probability, and Hilbert norm. Anyone closing native analysis or strong-closure arguments in the primitive recognition calculus cites these bridges. Each example is a small bridge definition plus an iff lemma equating display validity with the abstract ValidComparison predicate.

claimFor $\Delta$-real, probability, and Hilbert-norm protocols, the natural display map (to the real value, the probability, or the Hilbert norm) is a valid comparison: the protocol displays to that observable, and validity holds if and only if the abstract valid-comparison predicate is satisfied.

background

Primitive recognition calculus treats measurement as a comparison between a protocol and a displayed observable. The ValidComparison interface packages the abstract side of that relation: when a protocol is allowed to stand next to a concrete readout.

DeltaReal, DeltaProbability, and HilbertDisplayCompletion supply the three concrete display families used here. A $\Delta$-real protocol carries a real-valued readout; a probability protocol carries a probability; a Hilbert display completes to a norm-type observable. The module doc for the real case states the pattern: "a Delta-real protocol displays to its real value, and the observable is that same value." The probability and Hilbert cases follow the same template.

These examples sit downstream of the abstract ValidComparison layer and upstream of native analysis, so they fix notation and discharge the "is this display legitimate?" side conditions before stronger closure theorems run.

proof idea

Definition-and-bridge module, not a deep proof development. For each display family the pattern is the same: define a bridge object (realDisplayBridge, probabilityDisplayBridge, hilbertNormBridge) that pairs the Delta protocol with its canonical observable, then prove an iff lemma (real_display_valid_iff, probability_display_valid_iff, hilbert_display_valid_iff) equating that bridge's validity with the abstract ValidComparison predicate. A headline lemma packages the three examples. Arguments are direct unfoldings and applications of the imported ValidComparison, DeltaReal, DeltaProbability, and HilbertDisplayCompletion APIs.

why it matters in Recognition Science

Native analysis and strong closure of the Delta calculus need concrete, already-checked displays rather than the bare ValidComparison interface. This module supplies those instances. It is imported by DeltaNativeAnalysis and DeltaNativeStrongClosure, which use the bridges when they reason about real, probabilistic, or Hilbert-norm readouts without re-proving display legitimacy each time.

In the broader Recognition foundation, valid comparison is the gate between abstract recognition cost structure and laboratory observables. Pinning three standard displays here keeps later forcing-chain and native-unit arguments from carrying open display hypotheses. The headline lemma is the natural citation point when a parent theorem only needs "the usual displays are valid."

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (7)