EffectiveManifoldHypotheses
plain-language theorem explainer
EffectiveManifoldHypotheses bundles a directed refinement system on type C with its convergence and non-collapse conditions into one structure. Researchers deriving effective manifolds from recognition quotients cite this when stating the U1 assumption from the paper. The declaration is a direct structure packaging of three fields with no proof obligations.
Claim. Let $C$ be a type. An effective manifold hypothesis on $C$ consists of a directed refinement system on $C$, the property that this system converges by eventually separating every pair of distinct points, and the non-collapse condition that separation remains monotone across stages.
background
The module formalizes structural conditions under which directed refinement of recognition quotients yields an effective manifold. It targets open problems U1-U4, with U1 as the complete hypothesis bundle packaging U2 and U4 (U3 follows when the limit exists). A directed refinement system is a sequence of recognizers indexed by natural numbers such that each later recognizer is finer than the previous. The convergence condition requires that any two distinct points in $C$ are separated by some recognizer in the sequence. The non-collapse condition requires the quotient to stay nontrivial at every stage and that separation is preserved under further refinement.
proof idea
This is a structure definition that directly assembles the directed refinement system with the convergence and non-collapse conditions. No lemmas are invoked and no tactics are executed; the declaration functions purely as a packaging of the three required properties.
why it matters
This supplies the U1 hypothesis bundle referenced as Assumption 2.11 in the paper. It feeds the theorem showing convergence implies the intersection of all equivalence relations is the identity, and the status summary tracking U1-U4 progress. In the Recognition framework it supplies the structural hypotheses needed to derive an effective manifold from the recognition composition law and the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.