pith. sign in
module module high

IndisputableMonolith.Ethics.Virtues.SigmaPreservingProof

show as:
view Lean formalization →

Module SigmaPreservingProof introduces rich generator actions, where every admissibility-preserving function arises from composing a list of generators on admissible inputs. It models the claim that the 14 DREAM virtues generate all sigma-preserving transformations on List MoralState. The structure depends on finite lattice enumeration to support constructive reachability checks in the DREAM program.

claimA generator action $G$ is rich if for every admissibility-preserving function $f$ there exists a generator list whose composition equals $f$ on admissible inputs. This models the generation of all sigma-preserving maps by the DREAM virtues on lists of moral states.

background

The theoretical setting is the DREAM completeness program in Recognition Science ethics, which seeks to derive all sigma-preserving transformations from a finite virtue set. The module defines a rich generator action as one where every admissibility-preserving function can be expressed as the composition of some generator list on admissible inputs. It imports FiniteLatticeEnumeration, which establishes the constructive search infrastructure for the SigmaPreservingIsReachable residual hypothesis from the DREAM completeness program.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the abstract model for how the 14 DREAM virtues generate sigma-preserving transformations, feeding the DREAM completeness program. It addresses the residual hypothesis SigmaPreservingIsReachable by providing the rich action framework. The development links ethics formalization to the broader Recognition Science forcing chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)