IndisputableMonolith.Ethics.Virtues.Independence

   1import Mathlib
   2
   3/-!
   4# Virtue Independence and Minimality
   5
   6This module proves that the 14 virtue effect signatures are distinct,
   7non-redundant (removing any breaks the 14-element completeness condition),
   8and mutually independent (each is absent from the list after its removal).
   9These are structural/combinatorial properties of the signature catalogue,
  10not semantic independence of the virtue transforms themselves.
  11
  12All proofs are explicit - no `native_decide` (which uses compiler-trust axioms).
  13Only standard foundational axioms (propext, Quot.sound) are used.
  14-/
  15
  16namespace IndisputableMonolith.Ethics.Virtues.Independence
  17
  18/-! ## Effect Categories -/
  19
  20/-- The four categories of ethical transformation -/
  21inductive VirtueCategory where
  22  | Relational    -- Love, Compassion, Sacrifice
  23  | Systemic      -- Justice, Temperance, Humility
  24  | Temporal      -- Wisdom, Patience, Prudence
  25  | Facilitative  -- Forgiveness, Gratitude, Courage, Hope, Creativity
  26  deriving DecidableEq, Repr
  27
  28/-- Effect signature: category plus within-category index -/
  29structure EffectSignature where
  30  category : VirtueCategory
  31  index : ℕ
  32  deriving DecidableEq, Repr
  33
  34/-! ## The 14 Virtue Signatures -/
  35
  36def loveSignature : EffectSignature := ⟨.Relational, 0⟩
  37def compassionSignature : EffectSignature := ⟨.Relational, 1⟩
  38def sacrificeSignature : EffectSignature := ⟨.Relational, 2⟩
  39def justiceSignature : EffectSignature := ⟨.Systemic, 0⟩
  40def temperanceSignature : EffectSignature := ⟨.Systemic, 1⟩
  41def humilitySignature : EffectSignature := ⟨.Systemic, 2⟩
  42def wisdomSignature : EffectSignature := ⟨.Temporal, 0⟩
  43def patienceSignature : EffectSignature := ⟨.Temporal, 1⟩
  44def prudenceSignature : EffectSignature := ⟨.Temporal, 2⟩
  45def forgivenessSignature : EffectSignature := ⟨.Facilitative, 0⟩
  46def gratitudeSignature : EffectSignature := ⟨.Facilitative, 1⟩
  47def courageSignature : EffectSignature := ⟨.Facilitative, 2⟩
  48def hopeSignature : EffectSignature := ⟨.Facilitative, 3⟩
  49def creativitySignature : EffectSignature := ⟨.Facilitative, 4⟩
  50
  51def allSignatures : List EffectSignature := [
  52  loveSignature, compassionSignature, sacrificeSignature,
  53  justiceSignature, temperanceSignature, humilitySignature,
  54  wisdomSignature, patienceSignature, prudenceSignature,
  55  forgivenessSignature, gratitudeSignature, courageSignature,
  56  hopeSignature, creativitySignature
  57]
  58
  59theorem allSignatures_length : allSignatures.length = 14 := rfl
  60
  61/-! ## Category Orthogonality -/
  62
  63theorem Relational_ne_Systemic : VirtueCategory.Relational ≠ VirtueCategory.Systemic := by
  64  intro h; cases h
  65
  66theorem Relational_ne_Temporal : VirtueCategory.Relational ≠ VirtueCategory.Temporal := by
  67  intro h; cases h
  68
  69theorem Relational_ne_Facilitative : VirtueCategory.Relational ≠ VirtueCategory.Facilitative := by
  70  intro h; cases h
  71
  72theorem Systemic_ne_Temporal : VirtueCategory.Systemic ≠ VirtueCategory.Temporal := by
  73  intro h; cases h
  74
  75theorem Systemic_ne_Facilitative : VirtueCategory.Systemic ≠ VirtueCategory.Facilitative := by
  76  intro h; cases h
  77
  78theorem Temporal_ne_Facilitative : VirtueCategory.Temporal ≠ VirtueCategory.Facilitative := by
  79  intro h; cases h
  80
  81/-! ## Signature Distinctness -/
  82
  83theorem sig_ne_of_cat_ne {s₁ s₂ : EffectSignature} (h : s₁.category ≠ s₂.category) : s₁ ≠ s₂ := by
  84  intro heq; apply h; cases heq; rfl
  85
  86theorem sig_ne_of_idx_ne {s₁ s₂ : EffectSignature}
  87    (hi : s₁.index ≠ s₂.index) : s₁ ≠ s₂ := by
  88  intro heq; apply hi; cases heq; rfl
  89
  90/-! ## All 14 Signatures Are Distinct -/
  91
  92-- The key insight: we can prove nodup by showing all pairs are distinct,
  93-- which follows from either different categories or different indices
  94
  95theorem all_signatures_distinct : allSignatures.Nodup := by
  96  unfold allSignatures
  97  -- Use Mathlib's decidability for List.Nodup with DecidableEq
  98  decide
  99
 100/-! ## Independence Definitions -/
 101
 102def SignatureIndependent (sig : EffectSignature) (sigs : List EffectSignature) : Prop :=
 103  sig ∉ sigs
 104
 105def SignatureSetMinimal (sigs : List EffectSignature) : Prop :=
 106  sigs.Nodup
 107
 108def SignatureSetComplete (sigs : List EffectSignature) : Prop :=
 109  sigs.length = 14 ∧ sigs.Nodup
 110
 111/-! ## Core Theorems -/
 112
 113theorem all_signatures_minimal : SignatureSetMinimal allSignatures :=
 114  all_signatures_distinct
 115
 116theorem signatures_complete : SignatureSetComplete allSignatures :=
 117  ⟨allSignatures_length, all_signatures_distinct⟩
 118
 119theorem signatures_non_redundant (i : Fin 14) :
 120    ¬SignatureSetComplete (allSignatures.eraseIdx i) := by
 121  unfold SignatureSetComplete
 122  intro ⟨h_len, _⟩
 123  have h_erased : (allSignatures.eraseIdx i).length = 13 := by
 124    simp only [List.length_eraseIdx]
 125    have h1 : allSignatures.length = 14 := rfl
 126    have h2 : i.val < 14 := i.isLt
 127    simp only [h1, h2, ↓reduceIte]
 128  omega
 129
 130/-! ## Individual Virtue Independence -/
 131
 132theorem all_virtues_independent (i : Fin 14) :
 133    SignatureIndependent allSignatures[i] (allSignatures.eraseIdx i) := by
 134  unfold SignatureIndependent
 135  have h_nodup := all_signatures_distinct
 136  have h_len : allSignatures.length = 14 := rfl
 137  -- Use nodup property: if a appears at position i, it doesn't appear elsewhere
 138  intro h_mem
 139  -- h_mem : allSignatures[i] ∈ allSignatures.eraseIdx i
 140  -- This means there exists j < length - 1 such that (eraseIdx i)[j] = allSignatures[i]
 141  -- But (eraseIdx i)[j] = allSignatures[k] where k = j if j < i else j + 1
 142  -- And k ≠ i, so by nodup, allSignatures[k] ≠ allSignatures[i]
 143  rw [List.mem_iff_getElem] at h_mem
 144  obtain ⟨j, hj, heq⟩ := h_mem
 145  have h_erase_len : (allSignatures.eraseIdx i).length = 13 := by
 146    simp only [List.length_eraseIdx, h_len, i.isLt, ↓reduceIte]
 147  rw [h_erase_len] at hj
 148  -- Now heq : (allSignatures.eraseIdx i)[j] = allSignatures[i]
 149  -- (eraseIdx i)[j] = allSignatures[if j < i then j else j + 1]
 150  have h_inj := List.nodup_iff_injective_getElem.mp h_nodup
 151  by_cases h_lt : j < i.val
 152  · -- k = j < i, so k ≠ i
 153    have h_ne : j ≠ i.val := Nat.ne_of_lt h_lt
 154    have h_j_lt : j < allSignatures.length := by omega
 155    have heq' : allSignatures[j] = allSignatures[i.val] := by
 156      rw [List.getElem_eraseIdx] at heq
 157      simp only [h_lt] at heq
 158      exact heq
 159    have := @h_inj ⟨j, h_j_lt⟩ ⟨i.val, i.isLt⟩ heq'
 160    simp only [Fin.mk.injEq] at this
 161    exact h_ne this
 162  · -- k = j + 1, and k ≠ i because j ≥ i implies j + 1 > i
 163    have h_ge : i.val ≤ j := Nat.ge_of_not_lt h_lt
 164    have h_ne : j + 1 ≠ i.val := by omega
 165    have h_j1_lt : j + 1 < allSignatures.length := by omega
 166    have heq' : allSignatures[j + 1] = allSignatures[i.val] := by
 167      rw [List.getElem_eraseIdx] at heq
 168      have h_not_lt : ¬(j < i.val) := h_lt
 169      simp only [h_not_lt] at heq
 170      exact heq
 171    have := @h_inj ⟨j + 1, h_j1_lt⟩ ⟨i.val, i.isLt⟩ heq'
 172    simp only [Fin.mk.injEq] at this
 173    exact h_ne this
 174
 175/-! ## Master Theorem -/
 176
 177theorem virtue_signatures_minimality_complete :
 178    SignatureSetMinimal allSignatures ∧
 179    SignatureSetComplete allSignatures ∧
 180    (∀ i : Fin 14, ¬SignatureSetComplete (allSignatures.eraseIdx i)) :=
 181  ⟨all_signatures_minimal, signatures_complete, signatures_non_redundant⟩
 182
 183/-! ## Summary
 184
 185All proofs use only:
 186- Standard foundational axioms (propext, Quot.sound)
 187- Decidability instances (no compiler-trust axioms)
 188- Explicit structural reasoning
 189
 190NO `native_decide`, NO HOLES, NO custom axioms.
 191-/
 192
 193end IndisputableMonolith.Ethics.Virtues.Independence
 194