isFinerThan'_refl
plain-language theorem explainer
Reflexivity of the finer-than relation asserts that every recognizer is at least as fine as itself under the indistinguishability criterion. Researchers constructing directed refinement sequences for effective manifolds cite this to confirm the relation forms a preorder. The proof is a term-mode one-liner that returns the input indistinguishability witness unchanged.
Claim. For every recognizer $r$, if $r$ identifies two configurations $c_1$ and $c_2$ as indistinguishable then $r$ identifies them as indistinguishable.
background
The Effective Manifold module formalizes structural conditions under which directed refinements of recognition quotients produce an effective manifold, addressing open problems U1-U4. IsFinerThan' is the predicate stating that recognizer r1 is at least as fine as r2 precisely when indistinguishability under r1 implies indistinguishability under r2. The upstream E definition from SpectralEmergence counts the edges of the D-cube as D times 2 to the power of D minus 1, supplying the geometric background for the recognizer event spaces though not invoked here.
proof idea
The proof is a term-mode one-liner that applies the identity function to the two configurations and the indistinguishability hypothesis from the first recognizer.
why it matters
This reflexivity result supplies the base case for the DirectedRefinement structure, whose refines field requires IsFinerThan' between consecutive recognizers in the sequence. It contributes to the U1 hypothesis bundle by ensuring the refinement ordering is reflexive, enabling the monotone chains that address convergence under U2. In the Recognition Science setting this supports the passage from discrete recognizers to the smooth effective manifold limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.