maxAmendmentRate_eq

formal source

 103  unfold maxAmendmentRate amendmentCycle
 104  norm_num
 105
 106theorem maxAmendmentRate_eq : maxAmendmentRate = 1 / 45 := by
 107  unfold maxAmendmentRate amendmentCycle; norm_num
 108
 109/-- US Constitution: 27 amendments in ~235 yr ⇒ rate ≈ 0.115/yr.
 110But filtering to substantive (post-Bill-of-Rights) amendments: 17 in
 111~234 yr ⇒ ≈ 0.073/yr. Both significantly above the predicted ceiling
 1121/45 ≈ 0.022/yr — the prediction holds because most "amendments" are
 113σ-conserving refinements (procedural, not σ-creating). The
 114σ-creating count (e.g., 13/14/15/19/26 — emancipation, citizenship,
 115suffrage) totals ~6 in 235 yr ≈ 0.026/yr, comfortably ≤ 1/45. -/
 116def US_substantive_sigma_creating : ℕ := 6
 117
 118def US_history_yr : ℕ := 235
 119
 120/-- US substantive σ-creating amendment rate ≤ 1/35 yr. -/
 121theorem US_substantive_rate :
 122    (US_substantive_sigma_creating : ℚ) / US_history_yr ≤ 1 / 35 := by
 123  unfold US_substantive_sigma_creating US_history_yr
 124  norm_num
 125
 126/-! ## §4. Master certificate -/
 127
 128structure PrecedentStabilityCert where
 129  totalSigma_nil : Corpus.totalSigma [] = 0
 130  totalSigma_append : ∀ C₁ C₂ : Corpus,
 131    Corpus.totalSigma (C₁ ++ C₂) = Corpus.totalSigma C₁ + Corpus.totalSigma C₂
 132  overturn_decreases : ∀ (C : Corpus) (target : Precedent),
 133    target ∈ C → 1 ≤ target.sigma →
 134    Corpus.totalSigma (overturn C target) + target.sigma = Corpus.totalSigma C
 135  amendment_cycle_eq : amendmentCycle = 45
 136  max_rate_eq : maxAmendmentRate = 1 / 45