module module

`IndisputableMonolith.Information.ChurchTuringPhysicsStructure`

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.Information.SimulationHypothesisStructure module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Information.ComputationLimitsStructure module_import

declarations in this module (21)

abbrev Phase L46
def numPhases L49
theorem phase_space_finite L52
theorem phase_functions_finite L57
def DiscreteLedgerState L64
def LedgerTransition L68
theorem discrete_ledger_computable L74
def numLedgerStates L83
theorem ledger_state_space_finite L86
theorem has_computation_limits_structure L93
def church_turing_physics_from_ledger L97
theorem church_turing_physics_structure L106
theorem church_turing_implies_limits L110
theorem phase_space_bounded L118
theorem tick_rate_bounded L124
theorem computation_takes_time L128
theorem finite_function_is_computable L136
theorem eight_tick_step_computable L147
theorem rs_dynamics_beyond_rational L158
theorem rs_dynamics_approximable L164
def ic003_certificate L171