totalSigma_nil
plain-language theorem explainer
The total σ-charge of an empty corpus of precedents equals zero. Jurisprudence models of stare decisis cite this nil case to anchor σ-conservation across legal corpora. The proof is a one-line wrapper that unfolds the sum definition and applies list simplification.
Claim. Let $C$ be a corpus, the list of active precedents each carrying an integer σ-weight. The total σ-charge of the empty corpus satisfies $0 = 0$.
background
A corpus is defined as a list of precedents. The total σ-charge of a corpus is the sum of the σ-weights of its precedents. This models common-law precedent as a σ-conserving structure on the legal-decision graph, where a precedent's σ-charge equals its authoritative weight.
proof idea
The proof is a one-line wrapper that unfolds the totalSigma definition and applies simp to reduce the empty-list sum.
why it matters
This base case populates the totalSigma_nil field of the PrecedentStabilityCert structure. That certificate certifies σ-conservation under append and overturn operations while bounding amendment rates by the 45-year frustration period. It completes the nil case in the σ-additivity chain for the jurisprudence track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.