US_substantive_rate
plain-language theorem explainer
The theorem verifies that the US substantive σ-creating amendment rate, given by 6 amendments over 235 years, satisfies ≤ 1/35 per year. Constitutional scholars modeling precedent stability via σ-conservation would cite this numerical check when applying the framework to real legal corpora. The proof is a one-line wrapper that unfolds the two constant definitions and normalizes the rational inequality.
Claim. The rate of substantive σ-creating amendments in US constitutional history satisfies $6/235 ≤ 1/35$ per year.
background
The module treats common-law precedent as a σ-conserving structure on the legal-decision graph: each precedent carries a σ-weight equal to its jurisdictional level, and total σ of a corpus must remain invariant under overturning events. Constitutional amendment rates are bounded by the 45-year consciousness-gap cycle. US_substantive_sigma_creating counts the σ-creating amendments (emancipation, citizenship, suffrage and similar) as 6; US_history_yr fixes the historical span at 235 years. These constants instantiate the general maxAmendmentRate = 1/45 bound for the concrete US corpus.
proof idea
The proof is a one-line wrapper. It unfolds the definitions of US_substantive_sigma_creating and US_history_yr, then applies norm_num to confirm the numerical inequality 6/235 ≤ 1/35 by direct rational arithmetic.
why it matters
This result supplies the US-specific numerical verification that feeds into precedentStabilityCert and the consolidated theorem precedent_stability_one_statement. The latter collects additivity of totalSigma, the general maxAmendmentRate = 1/45, and the observed bound ≤ 1/35. It instantiates σ-conservation for the US constitutional corpus, confirming consistency with the frustration-period bound derived from the Recognition framework. The module falsifier is any documented substantive amendment rate exceeding 1/45 in a democracy with more than 100 years of constitutional history.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.