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, the induced setoid, and the physical quotient that collapses indistinguishable states. Anyone working at the T0 recognizer or gauge-signature layer cites this when states must be identified by what can be measured. The module is definitional scaffolding plus elementary equivalence and descent lemmas.

claimFix a state space $X$ and a family $F$ of observables $X \to V$. Two states $x,y \in X$ are observationally equivalent, written $x \sim_F y$, when $f(x)=f(y)$ for every $f \in F$. The relation $\sim_F$ is an equivalence; the physical quotient is $X/\sim_F$, with canonical projection $\pi$. Observables in $F$ descend to the quotient, and $\pi$ is injective precisely when $F$ separates points.

background

In Recognition Science the atomic floor is a single Boolean distinction (the T0 boundary), but a complete physical object is a family of recognizers, not one bit. This module sits in the Primitive Recognition Calculus and formalizes that distinction: states are identified exactly when no observable in the family can tell them apart.

Observational equivalence $\mathrm{ObsEquiv}$ is the pointwise agreement relation for a family $F$. The module packages it as a Lean setoid $\mathrm{obsSetoid}$, builds the quotient type $\mathrm{PhysicalQuotient}$, and supplies the projection $\mathrm{proj}$. Downstream gauge and signature work treats this quotient as the space of physically distinct configurations.

The surrounding Recognition Core aggregator exposes the same layer: recognizer, indistinguishability quotient, full recognition signature, and the completeness condition under which the signature determines all physically relevant states.

proof idea

This is primarily a definition module. Equivalence properties (reflexivity, symmetry, transitivity) are immediate from equality of observable values. The setoid and quotient are standard Lean constructions. Remaining lemmas are short: observables descend along the projection; states related by observational equivalence map to the same class; the projection is injective when the family separates points; gauge identification is read off indistinguishability.

why it matters in Recognition Science

The physical quotient is the formal carrier for "what recognition can actually distinguish." It is imported by RecognitionSignatureGauge, which records the T-1/T0 Boolean-shadow correction: a single Boolean is an atomic floor, not a complete encoding; the complete object is a family of observables and its full signature. RecognitionCore re-exports the same quotient as part of the public T0/T4 recognition-geometry core.

Sibling consumers (DeltaNativeAnalysis, DeltaNativeStrongClosure, ObjecthoodRegistry, QuotientExamples) build native $\Delta$-analysis, objecthood bookkeeping, and worked examples on top of this identification. Without collapsing observationally equivalent states, later gauge and signature theorems would count unphysical duplicates. The module therefore anchors the forcing-chain language at the recognizer layer before J-cost uniqueness (T5) and the phi fixed point (T6) enter.

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)