IndisputableMonolith.Ethics.Virtues.SigmaPreservingProof

   1import Mathlib
   2import IndisputableMonolith.Ethics.Virtues.FiniteLatticeEnumeration
   3
   4/-!
   5# SigmaPreservingIsReachable: Proof in the Abstract Framework
   6
   7This module addresses the SigmaPreservingIsReachable residual from the
   8DREAM completeness program in the abstract carrier-and-generator framework
   9established by `Ethics.Virtues.FiniteLatticeEnumeration`.
  10
  11## Outcome of the search
  12
  13The abstract framework admits a *positive* answer when the generator action
  14is *rich enough*: specifically, when every sigma-preserving function is in
  15the orbit of the identity under the generator monoid. We make this precise
  16via the `RichGeneratorAction` predicate.
  17
  18In the concrete DREAM virtue setting, the question of whether the 14
  19generators yield a rich action on `List MoralState` reduces to the bond-window
  20restriction. If yes, no 15th virtue is needed; if no, the smallest
  21counterexample becomes the 15th generator.
  22
  23## Honest status
  24
  25This module proves the *abstract* implication:
  26  RichGeneratorAction adm act -> SigmaPreservingIsReachable adm act.
  27
  28The empirical question of whether `RichGeneratorAction` holds for the
  29concrete DREAM virtue action on `List MoralState` is open and bounded by
  30the upstream rebuild of `Ethics.MoralState`.
  31
  32If concrete RichGeneratorAction is later shown to FAIL on a specific
  33sigma-preserving `f`, the failing `f` is the 15th DREAM virtue generator
  34and the inductive `DreamVirtue` would need an extra constructor.
  35
  36## Status: 0 sorry, 0 axiom.
  37-/
  38
  39namespace IndisputableMonolith.Ethics.Virtues.SigmaPreservingProof
  40
  41open IndisputableMonolith.Ethics.Virtues.FiniteLatticeEnumeration
  42
  43noncomputable section
  44
  45/-! ## Rich generator action -/
  46
  47/-- A generator action is *rich* when every admissibility-preserving function
  48    can be expressed as the composition of some generator list (on admissible
  49    inputs). This is the abstract analogue of "the 14 DREAM virtues generate
  50    every sigma-preserving transformation on List MoralState". -/
  51def RichGeneratorAction {α G : Type*}
  52    (adm : Admissible α) (act : GenAction α G) : Prop :=
  53  ∀ (f : α → α), SigmaPreserving adm f → ReachableTransition adm act f
  54
  55/-! ## The headline (conditional) theorem -/
  56
  57/-- Under `RichGeneratorAction`, every sigma-preserving function is reachable.
  58    This is a near-tautology at the abstract level (RichGeneratorAction *is*
  59    SigmaPreservingIsReachable in the framework's vocabulary), so the content
  60    is the *naming*: future investigations of the concrete DREAM action need
  61    only verify Richness to close the residual. -/
  62theorem reachable_of_rich
  63    {α G : Type*} (adm : Admissible α) (act : GenAction α G)
  64    (h_rich : RichGeneratorAction adm act) :
  65    SigmaPreservingIsReachable adm act :=
  66  h_rich
  67
  68/-! ## Inverse direction: if RichGeneratorAction fails, a 15th virtue exists
  69
  70The contrapositive: if the abstract framework's `RichGeneratorAction` fails
  71on `(adm, act)`, there is a sigma-preserving `f` with no generator-list
  72witness, and this `f` is the canonical "15th generator" needed to extend
  73the action to a rich one. -/
  74
  75theorem fifteenth_generator_required_iff_not_rich
  76    {α G : Type*} (adm : Admissible α) (act : GenAction α G) :
  77    ¬ RichGeneratorAction adm act ↔
  78    ∃ (f : α → α), SigmaPreserving adm f ∧ ¬ ReachableTransition adm act f := by
  79  unfold RichGeneratorAction
  80  push_neg
  81  rfl
  82
  83/-! ## Trivial degenerate case: empty generator action
  84
  85When the generator type `G` is empty, `RichGeneratorAction` holds iff every
  86sigma-preserving function equals the identity on admissible inputs. This is
  87trivially false in general but is a clean boundary case. -/
  88
  89theorem rich_iff_only_id_on_admissible_for_empty_G
  90    {α : Type*} (adm : Admissible α)
  91    (h_inhabited : ∃ x, adm x) :
  92    RichGeneratorAction adm (act := (fun (g : Empty) => g.elim))
  93    ↔ ∀ (f : α → α), SigmaPreserving adm f → ∀ x, adm x → f x = x := by
  94  constructor
  95  · intro h_rich f h_pres x hadm
  96    obtain ⟨gs, hgs⟩ := h_rich f h_pres
  97    cases gs with
  98    | nil =>
  99        rw [hgs x hadm]
 100        unfold composeGenerators
 101        simp [id]
 102    | cons g _ =>
 103        exact g.elim
 104  · intro h_only_id f h_pres
 105    refine ⟨[], ?_⟩
 106    intro x hadm
 107    have h := h_only_id f h_pres x hadm
 108    rw [h]
 109    unfold composeGenerators
 110    simp [id]
 111
 112/-! ## Master cert -/
 113
 114structure SigmaPreservingProofCert
 115    {α G : Type*} (adm : Admissible α) (act : GenAction α G) where
 116  abstract_implication : RichGeneratorAction adm act → SigmaPreservingIsReachable adm act
 117  fifteenth_iff : ¬ RichGeneratorAction adm act ↔
 118      ∃ (f : α → α), SigmaPreserving adm f ∧ ¬ ReachableTransition adm act f
 119
 120theorem sigmaPreservingProofCert_holds
 121    {α G : Type*} (adm : Admissible α) (act : GenAction α G) :
 122    SigmaPreservingProofCert adm act :=
 123{ abstract_implication := reachable_of_rich adm act
 124  fifteenth_iff := fifteenth_generator_required_iff_not_rich adm act }
 125
 126end
 127
 128end IndisputableMonolith.Ethics.Virtues.SigmaPreservingProof
 129