module module

`IndisputableMonolith.Jurisprudence.PrecedentStabilityFromSigma`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (18)

structure Precedent L45
abbrev Corpus L52
def totalSigma L57
theorem totalSigma_append L60
theorem totalSigma_nil L66
def overturn L75
theorem overturn_decreases_sigma L80
def amendmentCycle L95
theorem amendmentCycle_eq L97
def maxAmendmentRate L100
theorem maxAmendmentRate_pos L102
theorem maxAmendmentRate_eq L106
def US_substantive_sigma_creating L116
def US_history_yr L118
theorem US_substantive_rate L121
structure PrecedentStabilityCert L128
def precedentStabilityCert L139
theorem precedent_stability_one_statement L152