composeGenerators_preserves
plain-language theorem explainer
The theorem shows that if each generator preserves admissibility then any finite composition applied to an admissible state remains admissible. Researchers closing the DREAM completeness argument in Recognition Science cite it to justify that reachable transformations stay inside the admissible set. The proof is a direct induction on the generator list, applying the preservation hypothesis at each cons step and discharging the nil case by assumption.
Claim. If $Preserves(adm, act)$ holds, then for every finite list $gs$ of generators and every admissible state $x$, the left-fold composition of the generators in $gs$ applied to $x$ is admissible.
background
The module supplies constructive enumeration infrastructure for the residual hypothesis SigmaPreservingIsReachable inside the DREAM completeness program. It works on an abstract carrier type α equipped with a generator set G, deliberately avoiding the broken golden-ratio references in the parent Ethics.Virtues.CompletenessClosure module. The same finite-lattice argument therefore applies uniformly to any finite carrier and finite generator set; the 14 DREAM virtues appear only as parameters of the abstract framework.
proof idea
Induction on the list gs. The nil case returns the given admissibility assumption directly. The cons case first invokes the preservation hypothesis to obtain admissibility of act g x, then applies the inductive hypothesis to the tail list on that new state.
why it matters
The result is invoked by reachable_implies_sigma_preserving to conclude that every reachable transformation is sigma-preserving. It therefore supplies one concrete step toward discharging the SigmaPreservingIsReachable hypothesis in the DREAM program. Within Recognition Science it closes the finite-generator reachability argument on abstract carriers without importing the defective phi-ladder material.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.