reachable_implies_sigma_preserving
plain-language theorem explainer
Reachable transformations on admissible carriers are necessarily sigma-preserving. Workers on the DREAM completeness closure cite this lemma to confirm that generator compositions automatically respect the admissibility predicate. The short term proof extracts the witnessing generator list from the reachability assumption and applies the inductive composition-preservation result.
Claim. Let $adm : α → Prop$ be an admissibility predicate on a carrier $α$ and let $act : G → α → α$ be a generator action. Assume every generator preserves admissibility. If a map $f : α → α$ agrees with the composition of some finite list of generators on every admissible input, then $f$ itself maps admissible inputs to admissible outputs.
background
The FiniteLatticeEnumeration module abstracts the DREAM virtues into an arbitrary carrier equipped with an admissibility predicate and a generator action. Admissibility is simply a predicate on states. The generator action applies an element of $G$ to a state. Preservation requires that each generator sends admissible states to admissible states. A map is reachable when it equals the left-fold composition of some generator list on admissible inputs. Sigma-preserving means the map itself sends admissible states to admissible states.
proof idea
The term proof obtains the generator list from the reachability hypothesis. It introduces an arbitrary admissible state, rewrites the image under the map using the equality supplied by reachability, and discharges the goal by the composition-preservation theorem applied to the same list.
why it matters
This result supplies the reachable-to-preserving direction required by the SigmaPreservingIsReachable residual hypothesis in the DREAM completeness program. It closes a structural step in the ethics virtues layer by showing that any map constructed from the generators inherits the preservation property. The argument stays within the abstract finite-lattice setting and does not invoke the core forcing chain or recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.