pith. machine review for the scientific record. sign in
def definition def or abbrev high

totalSigma

show as:
view Lean formalization →

The total σ-charge of a legal corpus equals the sum of the jurisdictional σ-weights of its active precedents. Jurisprudence researchers tracking stare decisis under conservation would cite this when computing aggregate charge across precedent lists. The definition is a direct one-line sum after mapping the sigma field over the corpus list.

claimLet $C$ be a corpus, that is a list of precedents each carrying a natural-number σ-weight. The total σ-charge is $∑_{p ∈ C} σ(p)$, where σ(p) is the jurisdictional weight of precedent p.

background

In the Precedent Stability from σ-Conservation module a Precedent is a structure holding a label, a natural-number sigma field (1 for trial, 2 for appeal, 3 for supreme), and an age. Corpus is the list of such active precedents. The module treats common-law precedent as the σ-conserving structure on the legal-decision graph, with each precedent's σ-charge equal to its authoritative weight.

proof idea

This is a one-line definition that applies map to extract the sigma field from each precedent in the corpus and then sums the resulting list of natural numbers.

why it matters in Recognition Science

This definition supplies the total σ-charge used in overturn_decreases_sigma, which shows that overturning a positive-σ precedent decreases the total, and in the PrecedentStabilityCert structure that certifies stability bounds. It fills the σ-conservation step in Track I5 of Plan v5, where constitutional amendment rates are bounded by the gap-45 frustration period. The parent result is the one-statement precedent stability theorem that combines additivity, the 1/45 rate, and the US empirical bound.

scope and limits

formal statement (Lean)

  57def totalSigma (C : Corpus) : ℕ := (C.map Precedent.sigma).sum

proof body

Definition body.

  58
  59/-- σ is additive across corpus union (concatenation). -/

used by (10)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.