totalSigma_append
The total σ-charge of a concatenated legal corpus equals the sum of the charges of its parts. Legal theorists modeling stare decisis would cite this additivity to establish σ-conservation under precedent union. The proof is a direct algebraic reduction that unfolds the sum definition and rewrites via list append lemmas.
claimFor any two corpora $C_1, C_2$ (lists of precedents), the total σ-charge satisfies $σ(C_1 ++ C_2) = σ(C_1) + σ(C_2)$, where $σ(C)$ denotes the sum of the σ-weights of precedents in $C$.
background
Corpus is defined as the list of active precedents, each carrying an integer σ-weight equal to its jurisdictional level. totalSigma is the function that maps a corpus to the sum of those weights. The module models common-law precedent as a σ-conserving structure on the legal-decision graph, with overturning events required to preserve total charge. This additivity lemma is the direct analogue of the totalSigma definition imported from SubstrateIndependentMonotheism, where the same summation appears for substrate charges.
proof idea
One-line term proof that unfolds totalSigma to expose the list sum, then rewrites with the standard Mathlib lemmas List.map_append and List.sum_append.
why it matters in Recognition Science
This lemma supplies the append case required by the PrecedentStabilityCert structure and the precedent_stability_one_statement theorem. It closes the conservation property needed to bound amendment rates at 1/45 yr (the consciousness-gap cycle) and to prove that overturning a positive-σ precedent strictly decreases total charge. The result sits inside Track I5 of the Recognition framework, where σ-additivity mirrors the RCL functional equation used for physical constants.
scope and limits
- Does not assign numerical values to individual precedent weights.
- Does not address operations other than list concatenation.
- Does not derive the 1/45 yr bound; that follows from later lemmas.
- Does not model non-list representations of legal corpora.
Lean usage
precedentStabilityCert : PrecedentStabilityCert where totalSigma_append := Corpus.totalSigma_appendformal statement (Lean)
60theorem totalSigma_append (C₁ C₂ : Corpus) :
61 totalSigma (C₁ ++ C₂) = totalSigma C₁ + totalSigma C₂ := by
proof body
Term-mode proof.
62 unfold totalSigma
63 rw [List.map_append, List.sum_append]
64
65/-- Empty corpus has zero σ. -/