IndisputableMonolith.Information.ComputationLimitsStructure

declarations in this module (26)

• def fundamental_tick L44
• theorem tick_pos L47
• def max_computation_rate L52
• theorem max_rate_pos L55
• theorem tick_is_atomic_time_unit L62
• def computation_limits_from_ledger L74
• theorem computation_limits_structure L76
• theorem phi_not_rational L79
• theorem phi_minimal_polynomial L87
• theorem phi_minimal_polynomial_no_rational_roots L91
• theorem rational_root_theorem_for_phi L96
• theorem no_exact_phi_computation L102
• def k_B L110
• theorem landauer_energy_pos L114
• theorem landauer_scales_with_temp L124
• theorem computation_has_nonzero_energy_cost L133
• def hbar L140
• def bremermann_limit L144
• theorem bremermann_limit_pos L147
• def max_ops_per_sec L153
• theorem max_ops_scales_with_energy L156
• theorem finite_energy_implies_finite_computation L161
• theorem phi_gt_one L168
• theorem phi_powers_unbounded L172
• def computation_limits_summary L179
• def ic002_certificate L191