NonCollapseCondition
plain-language theorem explainer
NonCollapseCondition encodes the requirement that a directed refinement of recognition quotients never loses distinctions between configurations. Researchers constructing effective manifolds in Recognition Science cite it to keep the quotient cardinality non-decreasing along the sequence. The declaration is a structure definition whose two fields directly package the nontriviality and monotonicity properties for U4.
Claim. Let $C$ be a configuration space and let $S$ be a directed refinement system of recognizers on $C$. The non-collapse condition on $S$ holds if, for every stage $i$, the recognizer at stage $i$ distinguishes at least one pair of configurations in $C$, and any pair distinguished at stage $i$ remains distinguished at stage $i+1$.
background
The Effective Manifold Theory module formalizes structural conditions U1–U4 under which a directed refinement of recognition quotients yields an effective manifold. DirectedRefinement packages a sequence of recognizers indexed by natural numbers together with the requirement that each later recognizer is finer than the earlier one. Indistinguishable is the equivalence relation on configurations induced by a recognizer: two configurations are equivalent precisely when they produce the same event.
proof idea
This is a structure definition that directly encodes the two required properties as fields of a Prop. The first field asserts existence of a distinguishable pair at every stage; the second field asserts that the distinguishable relation is monotone under the refinement step. No further proof is supplied because the declaration functions as a hypothesis bundle rather than a derived theorem.
why it matters
NonCollapseCondition supplies the U4 component inside EffectiveManifoldHypotheses, the complete hypothesis bundle for the effective-manifold assumption (paper Assumption 2.11). It prevents the quotient dimension from dropping, thereby supporting the claim that the limiting space has three spatial dimensions as required by the eight-tick octave. The status_summary records that monotone separation is automatic from refinement in some cases, yet the structure makes the condition explicit for downstream use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.