PrecedentStabilityCert
plain-language theorem explainer
Legal theorists modeling stare decisis as σ-conservation cite the PrecedentStabilityCert structure, which bundles additivity of total σ-charge over corpus concatenation, exact decrease upon overturning a weighted precedent, the fixed 45-year amendment cycle, and the US substantive amendment rate bound at 1/35 per year. It is constructed directly from the supporting lemmas on total sigma and overturn operations. The definition serves as the master certificate for precedent stability in the jurisprudence track.
Claim. The structure asserts: total σ-charge of the empty corpus satisfies $totalSigma([]) = 0$; additivity $totalSigma(C_1 ++ C_2) = totalSigma(C_1) + totalSigma(C_2)$ for any corpora $C_1, C_2$; if precedent $p$ with weight $σ(p) ≥ 1$ belongs to corpus $C$ then $totalSigma(overturn(C, p)) + σ(p) = totalSigma(C)$; the amendment cycle equals 45; the maximum amendment rate equals $1/45$ per year; and the US substantive σ-creating amendment rate satisfies $(US_substantive_sigma_creating : ℚ) / US_history_yr ≤ 1/35$.
background
The module models common-law precedent as a σ-conserving structure on the legal-decision graph. A Precedent carries a σ-weight (jurisdictional level: 1 for trial, 2 for appeal, 3 for supreme) and an age. Corpus is the list of active precedents. totalSigma sums the σ-weights across the list. Overturning removes a precedent without σ-equivalent replacement, strictly decreasing total σ. Upstream, sigma from AbileneParadox is defined as the gap between private and public report: +1 if the agent privately prefers stay but publicly votes go, -1 for the reverse, and 0 for truthful agents.
proof idea
This is a definition that packages the required properties by direct reference to the supporting lemmas: totalSigma_nil, totalSigma_append, overturn_decreases_sigma, amendmentCycle_eq, maxAmendmentRate_eq, and the US_substantive_rate theorem. No tactics are applied; the structure fields are populated from the already-proved siblings.
why it matters
This certificate is the master object used by precedentStabilityCert to assert stability of the legal system under σ-conservation. It fills Track I5 of Plan v5 by bounding amendment rates by the 45-year consciousness-gap cycle. It connects to the Recognition framework via σ as the decision defect from AbileneParadox and the RCL that enforces conservation across operations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.