totalSigma

formal source

  54namespace Corpus
  55
  56/-- Total σ-charge of a corpus = sum of precedent σ-weights. -/
  57def totalSigma (C : Corpus) : ℕ := (C.map Precedent.sigma).sum
  58
  59/-- σ is additive across corpus union (concatenation). -/
  60theorem totalSigma_append (C₁ C₂ : Corpus) :
  61    totalSigma (C₁ ++ C₂) = totalSigma C₁ + totalSigma C₂ := by
  62  unfold totalSigma
  63  rw [List.map_append, List.sum_append]
  64
  65/-- Empty corpus has zero σ. -/
  66theorem totalSigma_nil : totalSigma [] = 0 := by
  67  unfold totalSigma; simp
  68
  69end Corpus
  70
  71/-! ## §2. Overturning operation -/
  72
  73/-- Overturning removes a precedent. Returns the corpus minus the first
  74matching entry. -/
  75def overturn (C : Corpus) (target : Precedent) : Corpus :=
  76  C.erase target
  77
  78/-- Overturning a precedent with σ ≥ 1 strictly decreases total σ
  79when the precedent is in the corpus. -/
  80theorem overturn_decreases_sigma (C : Corpus) (target : Precedent)
  81    (h_in : target ∈ C) (h_pos : 1 ≤ target.sigma) :
  82    Corpus.totalSigma (overturn C target) + target.sigma = Corpus.totalSigma C := by
  83  unfold overturn Corpus.totalSigma
  84  have h_sum : ((C.erase target).map Precedent.sigma).sum + target.sigma =
  85               (C.map Precedent.sigma).sum := by
  86    have := List.Perm.sum_eq (List.Perm.map Precedent.sigma
  87      (List.perm_cons_erase h_in))