SigmaPreservingProofCert
plain-language theorem explainer
SigmaPreservingProofCert packages the abstract claim that richness of a generator action on an admissible carrier implies every sigma-preserving map is reachable by generator compositions, together with the equivalence that non-richness is witnessed by a non-reachable sigma-preserving map. Researchers working on DREAM virtue completeness cite this structure to reduce concrete checks on List MoralState to verifying richness of the 14-generator action. The declaration is a structure definition that directly names the two components.
Claim. Let $adm : α → Prop$ be an admissibility predicate and $act : G → α → α$ a generator action. A certificate $SigmaPreservingProofCert$ $adm$ $act$ consists of a proof that if every admissibility-preserving map is reachable under $act$ then every sigma-preserving map is reachable, together with the equivalence that the action fails to be rich precisely when there exists a sigma-preserving map outside the reachable transitions.
background
In the abstract carrier-and-generator framework of Ethics.Virtues.FiniteLatticeEnumeration, an admissible state satisfies the predicate $adm$, and a generator action $act$ maps generators from $G$ to transformations on $α$. RichGeneratorAction $adm$ $act$ holds when every sigma-preserving function (one that maps admissible states to admissible states) can be obtained by composing a list of generators from $act$. SigmaPreservingIsReachable is the property that all such functions lie in the orbit of the identity under the generated monoid.
proof idea
The declaration is a structure definition with no computational content. It packages the abstract implication, which is supplied by the one-line wrapper reachable_of_rich that directly uses the definition of RichGeneratorAction, and the equivalence fifteenth_generator_required_iff_not_rich, which follows by unfolding the definition of RichGeneratorAction and applying push_neg.
why it matters
This structure closes the abstract part of the SigmaPreservingIsReachable residual in the DREAM completeness program. It is instantiated by sigmaPreservingProofCert_holds, which assembles the two components from reachable_of_rich and fifteenth_generator_required_iff_not_rich. The module doc notes that concrete richness for the 14-generator DREAM action on List MoralState remains open, bounded by the rebuild of Ethics.MoralState; if richness fails, the witnessing map becomes the fifteenth generator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.