Pith. sign in
module module high

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.QuotientSelection

show as:
view Lean formalization →

Defines observational equivalence of states under a family of observables and the induced physical quotient. Two states are identified exactly when every observable in the family agrees on them. Downstream gauge and signature modules import this setoid and projection. The development is mostly definitional: reflexivity, symmetry, and transitivity of the relation, then the quotient, projection, and descent lemmas.

claimFix a state space $X$ and a family $F$ of observables $f: X \to V_f$. Declare $x \sim_F y$ when $f(x)=f(y)$ for every $f\in F$. Then $\sim_F$ is an equivalence relation; the physical quotient is $X/\sim_F$ with projection $\pi$, and every $f\in F$ descends to a well-defined map on the quotient. If $F$ separates points, $\pi$ is injective.

background

In the Primitive Recognition Calculus, physical content is what a designated family of observables can distinguish. A single Boolean recognizer is an atomic floor (the T0 boundary), not a complete encoding of an arbitrary state space. Completeness requires a full family of recognizers and the signature they jointly determine.

This module packages that idea as a setoid. Observational equivalence under $F$ means every observable in $F$ returns the same value on the two states. The equivalence classes are the physically distinct states relative to $F$. The physical quotient and its projection are the formal carriers for later gauge and signature work.

The construction is pure Mathlib setoid/quotient infrastructure specialized to observable families. No Recognition-Science cost functional or forcing-chain step is assumed here; those enter in importers such as RecognitionSignatureGauge and RecognitionCore.

proof idea

Definition module with standard equivalence-relation lemmas. Observational equivalence is defined pointwise by agreement of all $f\in F$. Reflexivity, symmetry, and transitivity are immediate from equality in the value types, yielding a setoid. The physical quotient is the quotient type for that setoid; projection is the canonical map. Descent of observables is the universal property of the quotient. Injectivity of projection when $F$ separates points is the usual separating-family argument. Gauge-from-indistinguishability packages the identification of observationally equivalent states as a gauge quotient.

why it matters in Recognition Science

Supplies the indistinguishability quotient used at the T0/T4 recognizer layer. RecognitionCore aggregates this as part of "the recognizer, its indistinguishability quotient, the full recognition signature, and the completeness condition." RecognitionSignatureGauge records the related correction that a single Boolean distinction is atomic, not complete, and that the complete object is a family of observables and its signature.

Also imported by DeltaNativeAnalysis, DeltaNativeStrongClosure, ObjecthoodRegistry, and QuotientExamples, which need a canonical way to collapse states that no observable in the working family can tell apart. Without this quotient, later claims that a signature determines all physically relevant states would lack a precise carrier type.

scope and limits

used by (6)

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

declarations in this module (12)