IsFinerThan'
plain-language theorem explainer
Recognizer R1 is finer than R2 when every pair of configurations indistinguishable under R1 remains indistinguishable under R2. Effective manifold constructions cite this relation to enforce monotonicity in directed refinement sequences. The definition encodes the implication directly from the base indistinguishability predicate without additional lemmas.
Claim. For recognizers $R_1$ and $R_2$ over configuration space $C$, $R_1$ is at least as fine as $R_2$ when for all $c_1, c_2$ in $C$, indistinguishability of $c_1$ and $c_2$ under $R_1$ implies indistinguishability under $R_2$.
background
Effective Manifold Theory formalizes structural conditions U1-U4 under which directed refinements of recognition quotients produce an effective manifold. The upstream definition Indistinguishable declares that two configurations are equivalent under a recognizer precisely when they produce the same event, serving as the fundamental equivalence relation of recognition geometry. The module states these conditions as explicit hypothesis bundles rather than axioms, with a theorem showing that the conjunction of U2+U3+U4 is equivalent to the U1 bundle.
proof idea
This is a direct definition consisting of a universal quantifier over configurations that applies the implication between the two instances of the Indistinguishable predicate. No lemmas or tactics are invoked.
why it matters
It supplies the monotonicity predicate for the DirectedRefinement structure, which indexes a sequence of recognizers by natural numbers with each subsequent recognizer finer than the previous. This supports the U1 bundle for effective manifold data and enables the separate reflexivity and transitivity theorems. It operationalizes the refinement step toward the smooth limit manifold in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.