trivial_search_closed
plain-language theorem explainer
The empty list of reachability witnesses satisfies the search-closed property for any admissible-state predicate and generator action on abstract carriers. Researchers building constructive enumeration certificates for sigma-preserving reachability in the DREAM completeness program cite this as the vacuous base case. The proof is a one-line term that introduces a witness and membership hypothesis then eliminates the contradiction of membership in the empty list.
Claim. Let $α$ and $G$ be types, let $adm : α → Prop$ be an admissible-state predicate, and let $act : G → α → α$ be a generator action. Then $SearchClosed(α := α)(G := G)(adm := adm)(act := act) []$ holds.
background
This theorem sits inside the FiniteLatticeEnumeration module, which supplies constructive search infrastructure for the SigmaPreservingIsReachable residual hypothesis in the DREAM completeness program. The module works on abstract carriers and generator sets, treating the DREAM virtues as parameters rather than hard-coded data, and avoids prior bit-rot in golden-ratio foundations.
proof idea
The proof is a direct term-mode elimination. It introduces a witness w together with the hypothesis hw that w belongs to the empty list, then applies List.not_mem_nil to obtain a contradiction and eliminate.
why it matters
The result supplies the empty-list foundation for finiteLatticeEnumerationCert_holds, which assembles identity and singleton reachability witnesses into a full enumeration certificate. It advances the DREAM completeness program by closing the base case of the search-closed predicate used to verify that reachable transitions remain sigma-preserving.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.