ReachabilityWitness
plain-language theorem explainer
ReachabilityWitness packages a sigma-preserving map f on an admissible carrier together with a generator list whose composition recovers f exactly on admissible inputs. Researchers on the DREAM completeness program cite the structure when constructing explicit witnesses for reachable transformations inside finite-lattice enumerations of virtues. The declaration is a pure structure definition that records the four fields with no additional proof obligations.
Claim. A reachability witness for an admissible predicate adm on carrier α and generator action act on set G consists of a map f : α → α, a proof that f preserves admissibility, a list gs of generators, and a proof that f(x) equals the left-fold composition of act along gs for every admissible x.
background
The module supplies abstract search infrastructure for the residual hypothesis SigmaPreservingIsReachable inside the DREAM completeness program, deliberately avoiding the bit-rotted golden-ratio references in the completeness-closure module. Admissible is the predicate α → Prop selecting valid states. GenAction is the map G → α → α describing generator effects. SigmaPreserving requires that f sends admissible states to admissible states. ReachableTransition asserts existence of a generator list whose iterated action matches f on admissible inputs. ComposeGenerators performs the left-fold of the action over the list.
proof idea
The declaration is a structure definition. It directly bundles the data of a reachable transition that additionally satisfies the sigma-preserving property, with no lemmas or tactics invoked.
why it matters
ReachabilityWitness supplies the concrete data type consumed by identityWitness, singletonWitness, and SearchClosed to populate the search catalog. It advances the finite-lattice enumeration argument that every sigma-preserving map on a finite admissible set is reachable from the generators, thereby supporting the residual hypothesis SigmaPreservingIsReachable in the DREAM completeness program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.