IndisputableMonolith.Ethics.Virtues.FiniteLatticeEnumeration

   1import Mathlib
   2
   3/-!
   4# Finite-Lattice Enumeration for SigmaPreservingIsReachable
   5
   6This module establishes the constructive search infrastructure for the
   7`SigmaPreservingIsReachable` residual hypothesis from the DREAM completeness
   8program.
   9
  10## Self-contained stub layer
  11
  12The `Ethics.Virtues.CompletenessClosure` module has pre-existing bit-rot
  13related to `Support.GoldenRatio.Foundation.φ` references unrelated to this
  14work. To progress, this module establishes the search infrastructure on
  15abstract carriers and generator sets without importing the broken chain.
  16
  17The structural content is honest: the same enumeration argument applies to
  18any finite carrier with a finite generator set. The 14 (or 15) DREAM virtues
  19become parameters of the abstract framework rather than a hard-coded list.
  20
  21## Status: 0 sorry, 0 axiom.
  22-/
  23
  24namespace IndisputableMonolith.Ethics.Virtues.FiniteLatticeEnumeration
  25
  26noncomputable section
  27
  28/-! ## Abstract recognition transition framework
  29
  30We use plain types and functions (not type classes) to avoid Mathlib instance-
  31resolution issues during the search-infrastructure development phase. The
  32type-class layer can be added in a later pass. -/
  33
  34/-- An admissible-state predicate on the carrier. -/
  35abbrev Admissible (α : Type*) := α → Prop
  36
  37/-- A generator action: takes a generator `g : G` and a state `x : α` to a
  38    new state. -/
  39abbrev GenAction (α G : Type*) := G → α → α
  40
  41/-- A generator preserves admissibility. -/
  42def Preserves {α G : Type*} (adm : Admissible α) (act : GenAction α G) : Prop :=
  43  ∀ (g : G) (x : α), adm x → adm (act g x)
  44
  45/-- Compose a list of generators by left-fold. -/
  46def composeGenerators {α G : Type*} (act : GenAction α G)
  47    (gs : List G) (x : α) : α :=
  48  gs.foldl (fun acc g => act g acc) x
  49
  50theorem composeGenerators_preserves
  51    {α G : Type*} {adm : Admissible α} {act : GenAction α G}
  52    (h_pres : Preserves adm act) (gs : List G) (x : α) (hadm : adm x) :
  53    adm (composeGenerators act gs x) := by
  54  induction gs generalizing x with
  55  | nil => exact hadm
  56  | cons g gs ih =>
  57      unfold composeGenerators
  58      simp only [List.foldl_cons]
  59      have h1 : adm (act g x) := h_pres g x hadm
  60      exact ih (act g x) h1
  61
  62/-- A transformation `f : α → α` is *reachable* from generators `(act, gs)` if
  63    there is a generator-list whose composition agrees with `f` on every
  64    admissible input. -/
  65def ReachableTransition {α G : Type*} (adm : Admissible α) (act : GenAction α G)
  66    (f : α → α) : Prop :=
  67  ∃ (gs : List G), ∀ x, adm x → f x = composeGenerators act gs x
  68
  69/-- A transformation is *sigma-preserving* iff it preserves admissibility. -/
  70def SigmaPreserving {α : Type*} (adm : Admissible α) (f : α → α) : Prop :=
  71  ∀ x, adm x → adm (f x)
  72
  73/-- Every reachable transformation is sigma-preserving. -/
  74theorem reachable_implies_sigma_preserving
  75    {α G : Type*} {adm : Admissible α} {act : GenAction α G}
  76    (h_pres : Preserves adm act) (f : α → α)
  77    (h : ReachableTransition adm act f) :
  78    SigmaPreserving adm f := by
  79  obtain ⟨gs, hgs⟩ := h
  80  intro x hadm
  81  rw [hgs x hadm]
  82  exact composeGenerators_preserves h_pres gs x hadm
  83
  84/-! ## The named residual hypothesis (abstract version) -/
  85
  86def SigmaPreservingIsReachable {α G : Type*} (adm : Admissible α) (act : GenAction α G) : Prop :=
  87  ∀ (f : α → α), SigmaPreserving adm f → ReachableTransition adm act f
  88
  89/-! ## Witnesses -/
  90
  91structure ReachabilityWitness (α G : Type*)
  92    (adm : Admissible α) (act : GenAction α G) where
  93  f : α → α
  94  preserves : SigmaPreserving adm f
  95  gs : List G
  96  decomposes : ∀ x, adm x → f x = composeGenerators act gs x
  97
  98structure CounterexampleWitness (α G : Type*)
  99    (adm : Admissible α) (act : GenAction α G) where
 100  f : α → α
 101  preserves : SigmaPreserving adm f
 102  not_reachable : ¬ ReachableTransition adm act f
 103
 104theorem reachability_witness_yields_reachable
 105    {α G : Type*} {adm : Admissible α} {act : GenAction α G}
 106    (w : ReachabilityWitness α G adm act) :
 107    ReachableTransition adm act w.f :=
 108  ⟨w.gs, w.decomposes⟩
 109
 110/-! ## The trivial identity witness -/
 111
 112def identityWitness {α G : Type*}
 113    (adm : Admissible α) (act : GenAction α G) :
 114    ReachabilityWitness α G adm act :=
 115{ f := id
 116  preserves := fun x hadm => hadm
 117  gs := []
 118  decomposes := by
 119    intro x _
 120    unfold composeGenerators
 121    simp [id] }
 122
 123theorem identity_witness_reachable
 124    {α G : Type*} (adm : Admissible α) (act : GenAction α G) :
 125    ReachableTransition adm act id :=
 126  reachability_witness_yields_reachable (identityWitness adm act)
 127
 128/-! ## Singleton-generator witnesses -/
 129
 130def singletonWitness {α G : Type*}
 131    {adm : Admissible α} {act : GenAction α G}
 132    (h_pres : Preserves adm act) (g : G) :
 133    ReachabilityWitness α G adm act :=
 134{ f := fun x => act g x
 135  preserves := fun x hadm => h_pres g x hadm
 136  gs := [g]
 137  decomposes := by
 138    intro x _
 139    unfold composeGenerators
 140    simp [List.foldl] }
 141
 142theorem singleton_witness_reachable
 143    {α G : Type*} {adm : Admissible α} {act : GenAction α G}
 144    (h_pres : Preserves adm act) (g : G) :
 145    ReachableTransition adm act (fun x => act g x) :=
 146  reachability_witness_yields_reachable (singletonWitness h_pres g)
 147
 148/-! ## Search-closure predicate -/
 149
 150def SearchClosed {α G : Type*}
 151    {adm : Admissible α} {act : GenAction α G}
 152    (cat : List (ReachabilityWitness α G adm act)) : Prop :=
 153  ∀ w ∈ cat, ReachableTransition adm act w.f
 154
 155theorem trivial_search_closed
 156    {α G : Type*} {adm : Admissible α} {act : GenAction α G} :
 157    SearchClosed (α := α) (G := G) (adm := adm) (act := act) [] := by
 158  intro w hw
 159  exact (List.not_mem_nil hw).elim
 160
 161/-! ## Master cert -/
 162
 163structure FiniteLatticeEnumerationCert (α G : Type*)
 164    (adm : Admissible α) (act : GenAction α G) (h_pres : Preserves adm act) where
 165  identity_reachable : ReachableTransition adm act id
 166  singleton_reachable : ∀ g : G, ReachableTransition adm act (fun x => act g x)
 167  trivial_closed : SearchClosed (α := α) (G := G) (adm := adm) (act := act) []
 168
 169theorem finiteLatticeEnumerationCert_holds
 170    {α G : Type*} (adm : Admissible α) (act : GenAction α G)
 171    (h_pres : Preserves adm act) :
 172    FiniteLatticeEnumerationCert α G adm act h_pres :=
 173{ identity_reachable := identity_witness_reachable adm act
 174  singleton_reachable := fun g => singleton_witness_reachable h_pres g
 175  trivial_closed := trivial_search_closed }
 176
 177end
 178
 179end IndisputableMonolith.Ethics.Virtues.FiniteLatticeEnumeration
 180