CounterexampleWitness
plain-language theorem explainer
CounterexampleWitness packages a map on an admissible carrier that preserves the admissible predicate yet cannot be realized as any finite composition of generator actions. Researchers auditing the DREAM completeness program cite it when constructing search procedures over finite lattices to test the residual SigmaPreservingIsReachable hypothesis. The declaration is a plain structure definition that bundles the map, its preservation property, and the explicit negation of reachability.
Claim. A structure consisting of a function $f : X → X$, a proof that $f$ preserves the admissible predicate on $X$, and a proof that $f$ is not equal to the action of any finite list of generators on admissible inputs.
background
The module supplies abstract search infrastructure for the residual hypothesis that every sigma-preserving map is reachable from a finite generator set. Admissible is the predicate $α → Prop$ selecting admissible states. GenAction is the type of maps $G → α → α$ that apply a generator to a state. SigmaPreserving requires that $f$ sends admissible states to admissible states. ReachableTransition asserts that $f$ agrees with the iterated action of some list of generators on every admissible input, using the composeGenerators helper from the same module.
proof idea
This is a structure definition that directly bundles the three components of the witness: the map, the preservation proof, and the unreachability proof. No tactics or lemmas are applied; the declaration simply records the data of a potential counterexample.
why it matters
It supplies the constructive search infrastructure for the SigmaPreservingIsReachable residual hypothesis in the DREAM completeness program. The module isolates the enumeration argument on abstract finite carriers so that the 14–15 DREAM virtues can later be instantiated as parameters rather than hard-coded. The structure therefore sits at the interface between the ethics cost model and the broader Recognition Science forcing chain, though it remains disconnected from the phi-ladder and T5–T8 landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.