module module high

`IndisputableMonolith.Information.ComputationLimitsStructure`

ComputationLimitsStructure defines the fundamental tick as the RS minimum time quantum and builds the structure of computation limits from the ledger. Researchers deriving the physical Church-Turing thesis or locating physics in the complexity zoo cite these bounds. The module consists of definitions and supporting lemmas on tick atomicity and phi irrationality.

claimThe fundamental tick satisfies $τ_0 = 1$ with position function $tick_pos$ and maximum computation rate derived from the ledger; $φ$ satisfies its minimal polynomial $x^2 - x - 1 = 0$ with no rational roots.

background

The module resides in the Information domain. It imports Constants, whose doc states 'The fundamental RS time quantum (RS-native). τ₀ = 1 tick.', and Cost. Sibling definitions introduce fundamental_tick, tick_pos, max_computation_rate, computation_limits_from_ledger, tick_is_atomic_time_unit, and lemmas establishing phi irrationality via its minimal polynomial and the rational root theorem.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the tick-based limits that feed IndisputableMonolith.Information.ChurchTuringPhysicsStructure (IC-003: Physical Church-Turing Thesis) and IndisputableMonolith.Information.PhysicsComplexityStructure (IC-005: Computational Complexity of Physics). These downstream modules use the atomic time unit and rate bounds to extend the Church-Turing thesis to physics and place physical processes in the complexity zoo.

scope and limits

Does not derive the physical Church-Turing thesis itself.
Does not classify specific classes such as BQP or QMA.
Does not treat continuous-time or non-discrete models.
Does not address quantum computation beyond the tick bound.

used by (2)

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

IndisputableMonolith.Information.ChurchTuringPhysicsStructure module_import
IndisputableMonolith.Information.PhysicsComplexityStructure module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

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