Distinguishable
plain-language theorem explainer
Distinguishability holds for a recognizer r when two configurations map to distinct events under its recognition function. Workers on information monotonicity and composite recognizers cite this to prove that joining maps cannot decrease distinguishing power. The definition is a direct one-line unfolding of the output inequality with no further lemmas required.
Claim. Let $r$ be a recognizer from configuration space $C$ to event space $E$. Configurations $c_1,c_2$ in $C$ are distinguishable precisely when $r(c_1)neq r(c_2)$.
background
Recognition Geometry module RG3 introduces a recognizer as a map $R:Cto E$ that collapses configurations into events, thereby defining an equivalence $c_1sim c_2$ exactly when $R(c_1)=R(c_2)$. The resulting equivalence classes are the resolution cells, the smallest units separable by this particular map. The definition sits atop upstream results including the nontriviality predicate (existence of at least one pair of positive quantities whose comparison is non-vacuous) and the J-cost structure from PhiForcingDerived.
proof idea
One-line definition that directly equates the predicate to inequality of the recognition outputs on the given pair.
why it matters
The definition supplies the primitive for all downstream monotonicity statements, including composite_distinguishes (if either factor distinguishes a pair then the composite does) and pillar2_distinguish_monotone. It realizes the RG3 axiom that recognition is lossy and thereby supports the forcing chain steps that derive three spatial dimensions from distinguishability. It also appears in symmetry-preservation and existence theorems inside the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.