pith. machine review for the scientific record. sign in
theorem proved term proof high

maxAmendmentRate_pos

show as:
view Lean formalization →

The theorem establishes positivity of the maximum constitutional amendment rate in the σ-conservation model of legal precedent. Constitutional theorists modeling stare decisis as a conserved σ-quantity would cite the bound when analyzing amendment frequency limits in long-lived systems. The proof is a one-line term wrapper that unfolds the rate as the reciprocal of the 45-year amendment cycle then applies norm_num to confirm the inequality holds.

claim$0 < 1/45$, where the denominator is the consciousness-gap amendment cycle of 45 years.

background

The module models common-law precedent as the σ-conserving structure on the legal-decision graph, with each Precedent carrying a σ-weight equal to its jurisdictional level (trial/appeal/supreme). Total σ of a corpus must remain conserved across overturning events, and constitutional amendment rates are bounded by the gap-45 frustration period. Upstream, amendmentCycle is defined as the 45-year consciousness-gap cycle, while maxAmendmentRate is the predicted maximum amendment rate per year given by its reciprocal.

proof idea

The proof is a one-line term-mode wrapper. It unfolds maxAmendmentRate and amendmentCycle to reduce the goal to 0 < 1/45, then applies norm_num to discharge the inequality by direct numeric computation.

why it matters in Recognition Science

This result completes the derivation that amendment rates cannot exceed one σ-conserving change per consciousness-gap cycle, supporting the module claim that constitutional amendment rates are bounded by the gap-45 frustration period. It sits inside the Precedent Stability from σ-Conservation track and supplies the positivity step required for the rate bound. The broader falsifier remains a documented amendment rate above 1/45 yr in any democracy with more than 100 years of constitutional history.

scope and limits

formal statement (Lean)

 102theorem maxAmendmentRate_pos : 0 < maxAmendmentRate := by

proof body

Term-mode proof.

 103  unfold maxAmendmentRate amendmentCycle
 104  norm_num
 105

depends on (2)

Lean names referenced from this declaration's body.