RichGeneratorAction
plain-language theorem explainer
RichGeneratorAction defines a generator action as rich when every sigma-preserving map on admissible states is reachable by composing generators from the action. Researchers investigating DREAM virtue completeness cite this predicate to reduce the question of whether the 14 virtues suffice to a single richness check on List MoralState. The definition consists of a direct universal quantification over sigma-preserving functions implying reachability under the generator monoid.
Claim. Let $adm$ be an admissibility predicate on type $α$ and $act$ a generator action on $α$ generated by $G$. The action $act$ is rich if for every function $f:α→α$, if $f$ preserves sigma-charge and admissibility then $f$ lies in the monoid generated by $act$ when restricted to admissible inputs.
background
In the abstract carrier-and-generator framework of FiniteLatticeEnumeration, an admissibility predicate selects valid states in $α$, a generator action supplies transformations generated by a set $G$, SigmaPreserving requires $f$ to map admissible states to admissible states while preserving sigma-charge (the gap between private and public reports), and ReachableTransition asserts that $f$ belongs to the monoid generated by the action on admissible elements. The module addresses the SigmaPreservingIsReachable residual from the DREAM completeness program. From the module documentation: 'The abstract framework admits a positive answer when the generator action is rich enough: specifically, when every sigma-preserving function is in the orbit of the identity under the generator monoid.'
proof idea
This is a definition whose body is the direct universal statement of the richness condition. No lemmas or tactics are invoked; the content is the naming of the predicate. Downstream results such as reachable_of_rich then apply the hypothesis directly to obtain SigmaPreservingIsReachable.
why it matters
This predicate supplies the central naming convention for the module's headline implication: RichGeneratorAction implies SigmaPreservingIsReachable, proved in reachable_of_rich by direct use of the hypothesis. It feeds fifteenth_generator_required_iff_not_rich and SigmaPreservingProofCert. In the Recognition Science framework it closes the abstract step of the DREAM completeness program by reducing sufficiency of the 14 virtues to richness verification, leaving the concrete status on MoralState as the open empirical question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.