rich_iff_only_id_on_admissible_for_empty_G
plain-language theorem explainer
The theorem states that an inhabited admissible carrier with the empty generator action is rich precisely when every sigma-preserving map fixes all admissible points. Researchers closing the DREAM completeness residual cite it as the clean boundary case separating rich actions from those needing a fifteenth generator. The proof splits the equivalence into two directions, using case analysis on the generator list and unfolding of composition to reduce to the identity.
Claim. Let $adm : α → Prop$ be an admissible predicate on a type $α$ that is inhabited. For the empty generator action (where the generator type is $Empty$), the action is rich if and only if every sigma-preserving map $f : α → α$ satisfies $f(x) = x$ for all admissible $x$.
background
Admissible is the predicate $α → Prop$ selecting states that survive the cost filter. SigmaPreserving requires that $f$ maps admissible inputs to admissible outputs. RichGeneratorAction asserts that every such $f$ is reachable: there exists a list of generators whose composition (via foldl on the action) equals $f$ on admissible inputs. composeGenerators implements that left-fold composition. The module sits inside the abstract carrier-and-generator framework of FiniteLatticeEnumeration, whose goal is to decide whether the DREAM virtues generate all sigma-preserving maps on List MoralState.
proof idea
Forward direction: assume richness, fix a sigma-preserving $f$, obtain the witnessing generator list $gs$, then case on $gs$. The nil case reduces to the identity via unfolding composeGenerators and the id lemma; the cons case is impossible because the generator type is Empty. Reverse direction: assume every sigma-preserving map is the identity on admissible points, then for any such $f$ exhibit the empty list as witness and apply the assumption to obtain the required equality.
why it matters
This theorem supplies the degenerate empty-action case inside the SigmaPreservingIsReachable program. It directly supports the headline implication RichGeneratorAction → SigmaPreservingIsReachable (reachable_of_rich) and the contrapositive that failure of richness produces a fifteenth generator (fifteenth_generator_required_iff_not_rich). The module doc notes that the concrete question whether the 14 DREAM virtues form a rich action remains open and is bounded by the upstream MoralState rebuild; the present result isolates the boundary where no generators exist at all.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.