Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparisonExamples

show as:
view Lean formalization →

Catalogue of concrete display bridges showing that Delta-real, Delta-probability, and Hilbert-norm protocols are valid comparisons in the primitive recognition calculus. Each bridge pairs a protocol with its displayed observable and proves the valid-comparison predicate. Downstream native-analysis and strong-closure modules import these examples as canonical instances. Arguments are short iff-style reductions to the corresponding display definitions.

claimFor the real, probability, and Hilbert-norm displays, each $\Delta$-protocol $P$ displays to an observable $O$ equal to the protocol's native value (real number, probability, or Hilbert norm), and the pair $(P,O)$ satisfies the valid-comparison predicate.

background

Primitive recognition calculus separates a protocol (how a quantity is recognized) from its display (the classical number or structure an observer reads). A valid comparison is a protocol-display pair in which the displayed observable is exactly what the protocol computes, with no extra identification hypothesis.

This module sits on three display layers already defined upstream: Delta-real (protocols whose native output is a real), Delta-probability (protocols valued in $[0,1]$ probabilities), and Hilbert display completion (protocols whose display is a Hilbert-space norm). The shared ValidComparison interface supplies the predicate that each bridge must discharge.

The local goal is not new physics, but a short roster of canonical instances: real display bridge, probability display bridge, and Hilbert-norm bridge, each with an iff lemma linking the bridge construction to validity.

proof idea

Definition-and-bridge module rather than a deep proof development. For each display kind one constructs an explicit bridge record (protocol, displayed value, equality witness) and proves an iff: the pair is a valid comparison exactly when the display equals the protocol's native output. Proofs are short algebraic or definitional reductions to the upstream display and ValidComparison APIs; no substantial tactic search.

why it matters in Recognition Science

Supplies the standard worked examples that DeltaNativeAnalysis and DeltaNativeStrongClosure import when they treat native $\Delta$-calculus as already equipped with valid real, probability, and Hilbert displays. Without these bridges, later closure and analysis results would have to re-prove instancehood inline. In the Recognition foundation stack this is scaffolding for the comparison layer that sits under forcing and cost arguments, not a T0-T8 step itself.

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)