module module moderate

`IndisputableMonolith.Ethics.Virtues.FiniteLatticeEnumeration`

This module establishes the abstract carrier-and-generator framework for finite lattice enumeration in the virtues domain. It introduces the Admissible predicate on a carrier, generator actions, preservation properties, and reachability constructs to support ethical state modeling. Researchers addressing the DREAM completeness program cite it as the setup for later equivalence proofs. The module is definitional, supplying the basic objects and relations used downstream without a central theorem.

claimLet $C$ be a carrier set. The central object is the admissible-state predicate $A : C → Prop$, equipped with generator actions $G$, preservation maps $P$, reachable transitions, and reachability witnesses $W$ such that reachable states imply sigma-preserving properties.

background

The module operates inside the abstract carrier-and-generator framework of Recognition Science applied to ethics and virtues. It defines Admissible as an admissible-state predicate on the carrier, together with GenAction for generator actions on states, Preserves for maps that preserve admissible structure, and ReachableTransition together with ReachabilityWitness for tracking transitions under finite generator sequences. The setting supplies the lattice-enumeration primitives needed for completeness arguments in the DREAM program.

proof idea

This is a definition module, no proofs. It enumerates the core predicates (Admissible, GenAction, Preserves, SigmaPreserving) and the basic lemmas (reachable_implies_sigma_preserving, reachability_witness_yields_reachable, SigmaPreservingIsReachable) that relate reachability to preservation properties on the finite lattice.

why it matters in Recognition Science

The module supplies the abstract carrier-and-generator framework that SigmaPreservingProof uses to close the SigmaPreservingIsReachable residual in the DREAM completeness program. It therefore supplies the foundational definitions and relations that allow later proofs to equate sigma-preserving maps with reachable transitions inside the virtues lattice.

scope and limits

Does not supply concrete models for named virtues.
Does not enumerate explicit finite lattices beyond the abstract carrier.
Does not connect to the T0-T8 forcing chain or physical constants.
Does not prove full DREAM completeness on its own.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Ethics.Virtues.SigmaPreservingProof module_import

declarations in this module (20)

abbrev Admissible L35
abbrev GenAction L39
def Preserves L42
def composeGenerators L46
theorem composeGenerators_preserves L50
def ReachableTransition L65
def SigmaPreserving L70
theorem reachable_implies_sigma_preserving L74
def SigmaPreservingIsReachable L86
structure ReachabilityWitness L91
structure CounterexampleWitness L98
theorem reachability_witness_yields_reachable L104
def identityWitness L112
theorem identity_witness_reachable L123
def singletonWitness L130
theorem singleton_witness_reachable L142
def SearchClosed L150
theorem trivial_search_closed L155
structure FiniteLatticeEnumerationCert L163
theorem finiteLatticeEnumerationCert_holds L169