singletonWitness
plain-language theorem explainer
This definition constructs an explicit ReachabilityWitness showing that the map induced by a single generator action is reachable from the generator list. Researchers enumerating sigma-preserving transitions on finite lattices for the DREAM completeness program cite it when assembling base cases for reachability. The construction directly populates the witness record with the generator action, applies the preservation hypothesis, and verifies decomposition on the singleton list via unfolding and simplification.
Claim. Let Adm be a predicate selecting admissible states on a carrier set, Act a generator action mapping each generator and state to a new state, Pres the assertion that every generator preserves admissibility, and g a generator. Then singletonWitness(Adm, Act, Pres, g) is the reachability witness whose transformation sends each admissible x to Act(g, x), whose preservation property is inherited from Pres, whose generator list is the singleton containing g, and whose decomposition property states that the transformation equals the left-fold composition of Act over that list.
background
The module supplies constructive enumeration tools for the residual hypothesis that every sigma-preserving map is reachable from generators, placed in the DREAM completeness program for ethical virtues. It works on abstract carriers and finite generator sets, avoiding prior import issues with golden-ratio references. Admissible is the predicate selecting valid states. GenAction is the map from a generator and state to the successor state. Preserves asserts that each generator sends admissible states to admissible states. ReachabilityWitness packages a transformation f together with its sigma-preservation property, a list of generators, and the equality showing f arises from composing those generators via left-fold. composeGenerators performs that left-fold.
proof idea
The definition is a direct record construction. It sets the transformation field to the action of the supplied generator g. The preserves field applies the input preservation hypothesis pointwise on admissible inputs. The generator list is instantiated as the singleton containing g. The decomposes field is discharged by unfolding composeGenerators and simplifying the fold over a one-element list.
why it matters
The definition is invoked by the downstream theorem singleton_witness_reachable to conclude that the single-generator map satisfies ReachableTransition. It supplies the base case for the finite-lattice enumeration infrastructure addressing the SigmaPreservingIsReachable hypothesis in the DREAM program. The surrounding module works abstractly on any finite carrier with finite generators and leaves open whether the full hypothesis holds for the fourteen-virtue lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.