module module

`IndisputableMonolith.Cosmology.RecognitionEventHorizon`

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 (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (25)

structure uses L50
lemma phi_pos L62
lemma one_lt_phi L63
lemma phi_sq_eq L64
lemma phi_inv_pos L68
lemma phi_inv_nonneg L70
lemma phi_inv_lt_one L72
def perEpochReach L79
def recognitionEventHorizon L82
def cumulativeReach L86
lemma perEpochReach_pos L89
lemma perEpochReach_summable L93
theorem tsum_phi_inv_pow L101
theorem tsum_perEpochReach L116
theorem recognitionEventHorizon_eq L123
theorem cumulativeReach_lt_horizon L132
theorem cumulativeReach_strictMono L151
theorem two_pow_four_lt_horizon L163
theorem horizon_lt_two_pow_five L171
theorem recognitionEventHorizon_between_dyadic_rungs L181
def dyadicFreezeRung L186
theorem dyadicFreezeRung_is_least L191
theorem recognition_event_horizon_one_statement L210
structure at L223
theorem reach_dichotomy L230