module module

`IndisputableMonolith.Unification.ConsciousnessBandwidth`

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.Unification.CriticalRecognitionLoading module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.BoltzmannConstant module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Unification.RecognitionBandwidth module_import

declarations in this module (19)

def barrierTicks L60
theorem barrier_eq L63
theorem barrier_is_lcm L66
def barrierPeriod L70
theorem barrierPeriod_pos L72
theorem barrierPeriod_eq L76
def boundaryArea L84
theorem boundaryArea_pos L86
theorem boundaryArea_monotone L90
def maintenanceBudget L103
theorem maintenanceBudget_pos L106
def maintenanceDemand L123
theorem maintenanceDemand_nonneg L127
theorem maintenanceDemand_zero_iff L133
def IsViable L150
theorem identity_viable L154
def complexDemand L167
theorem complexDemand_ge L171
theorem higher_Z_more_demand L184