`Corpus`

definition

show as: view math explainer →

module: IndisputableMonolith.Jurisprudence.PrecedentStabilityFromSigma
domain: Jurisprudence
line: 52 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Jurisprudence.PrecedentStabilityFromSigma on GitHub at line 52.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  49  deriving DecidableEq, Repr
  50
  51/-- The legal corpus = list of active precedents. -/
  52abbrev Corpus := List Precedent
  53
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.