isRecognitionConnected_subset
plain-language theorem explainer
If T is recognition-connected for recognizer r then every subset S of T is also recognition-connected for r. Workers on local regularity (RG5) cite this hereditary property when showing that resolution cells remain coherent under restriction. The proof is a direct one-line term that substitutes the subset relation into the universal quantifier of the connectivity definition.
Claim. Let $r$ be a recognizer. If $Ssubseteq T$ and every pair of elements in $T$ produces indistinguishable events under $r$, then every pair of elements in $S$ produces indistinguishable events under $r$.
background
A set $S$ is recognition-connected for recognizer $r$ precisely when every pair of its elements is indistinguishable, i.e., $forall c_1,c_2in S$, $r(c_1)=r(c_2)$ in the event space. The module develops this notion to support RG5: preimages of events must form connected clusters inside neighborhoods so that resolution cells do not fragment into Cantor-like sets. The local setting is therefore the emergence of smooth geometry from discrete recognition lattices, with upstream results on phi-forcing and ledger factorization supplying the ambient recognition structure.
proof idea
The proof is a one-line term: given $c_1,c_2in S$, apply the inclusion hypothesis to obtain $c_1,c_2in T$, then invoke the assumption that $T$ is recognition-connected.
why it matters
The result appears explicitly in the connectivity_status summary as one of the five basic properties that together establish RG5. It guarantees that connectivity is preserved under restriction, allowing resolution cells to serve as coherent atoms of recognition geometry without pathological fragmentation. In the Recognition Science chain this closes a small but necessary step toward the full local-regularity axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.