module module

`IndisputableMonolith.NumberTheory.ZeroCompositionLaw`

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.NumberTheory.CompositionDivergence module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.DiscretenessForcing module_import
IndisputableMonolith.NumberTheory.XiJBridge module_import
IndisputableMonolith.NumberTheory.ZeroLocationCost module_import

declarations in this module (15)

def defectIterate L54
theorem defectIterate_zero_param L57
theorem defectIterate_zero_eq_J_log L61
theorem defectIterate_nonneg L66
theorem defectIterate_zero_pos L71
theorem defectIterate_succ L89
theorem defectIterate_succ' L103
theorem defectIterate_four_mul_le L111
theorem defectIterate_exponential_lower L121
theorem one_le_four_pow L132
theorem defectIterate_mono L140
theorem nat_succ_le_pow_four L149
theorem defectIterate_unbounded L164
theorem defectIterate_zero_eq_zeroDefect L184
theorem zero_composition_diverges L192