`amendmentCycle`

definition

show as: view math explainer →

module: IndisputableMonolith.Jurisprudence.PrecedentStabilityFromSigma
domain: Jurisprudence
line: 95 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Jurisprudence.PrecedentStabilityFromSigma on GitHub at line 95.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  92/-! ## §3. Amendment-rate bound -/
  93
  94/-- The consciousness-gap amendment cycle = 45 yr. -/
  95def amendmentCycle : ℕ := 45
  96
  97theorem amendmentCycle_eq : amendmentCycle = 45 := rfl
  98
  99/-- Predicted maximum amendment rate (per yr). -/
 100def maxAmendmentRate : ℚ := 1 / (amendmentCycle : ℚ)
 101
 102theorem maxAmendmentRate_pos : 0 < maxAmendmentRate := by
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.