forced_quotient_iff
plain-language theorem explainer
The full recognition signature determines physical states only up to the indistinguishability quotient of the admitted observable family, with no extra hypotheses. Two states land in the same physical class exactly when no admissible observable separates them. Cite this when arguing that gauge is forced by the recognizer family rather than imposed by hand. The declaration is a public re-export of the core quotient-selection equivalence.
Claim. For an admissible family $F$ of observables $X \to C$ and states $x,y \in X$, the forced physical projections agree if and only if $x$ and $y$ are observationally equivalent under $F$: $\mathrm{proj}_F(x) = \mathrm{proj}_F(y) \iff x \sim_F y$. The forced quotient adds no identifications beyond indistinguishability and omits none.
background
Recognition Core aggregates the T0/T4 layer of the forcing chain: the recognizer, its indistinguishability quotient, the full recognition signature, and the completeness condition under which that signature determines all physically relevant states. The local slogan is that a single Boolean observable is atomic, not complete; physical content is carried by the admitted recognizer family.
The upstream result being re-exported states that the quotient is exactly the indistinguishability collapse: two states map to the same physical class iff no admissible observable separates them. Observational equivalence under a family $F$ means every map in $F$ takes the same value on both states. The projection $\mathrm{proj}_F$ is the canonical map onto classes of that relation.
Related structure in the same layer includes the identity event at the J-cost minimum ($x=1$) and the cost projector forced by the golden-ratio fixed point, but those enter only as ambient recognition geometry, not as hypotheses of this equivalence.
proof idea
One-line public abbrev that aliases the upstream theorem QuotientSelection.forced_iff. That theorem is itself a direct application of the standard quotient equality lemma: equality of projected classes is definitionally the generating equivalence relation (observational equivalence under $F$). No extra algebraic work is done at this aggregator site.
why it matters
This is the first public citation target listed in Recognition Core: the unconditional statement that the full signature determines the state up to the indistinguishability quotient. It sits at the T0/T4 recognizer/signature layer of the forcing chain and underwrites the gauge reading used by sibling declarations (gauge as absence of a distinguishing recognition act; completeness iff the family separates points; one Boolean coordinate atomic but not complete).
Downstream consumers in this module treat the forced quotient as the physical state space on which recognizer refinement, observer forcing, induced logic, and the recognition lattice are built. Without the exact match between projection equality and observational equivalence, gauge would be an extra stipulation rather than a forced collapse. No open sorry remains on this path; the module claims zero project-local axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.