`Precedent`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Jurisprudence.PrecedentStabilityFromSigma on GitHub at line 45.

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

  42/-! ## §1. Precedents and the σ-charged corpus -/
  43
  44/-- A precedent with σ-weight (jurisdictional level) and age. -/
  45structure Precedent where
  46  label : String
  47  sigma : ℕ  -- 1=trial, 2=appeal, 3=supreme
  48  age : ℕ
  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 :=

papers checked against this theorem

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