module module high

`IndisputableMonolith.Information.ComputationLimitsStructure`

ComputationLimitsStructure defines the fundamental tick as the minimum time quantum in Recognition Science and derives bounds on physical computation rates from the cost ledger. Researchers working on the physical Church-Turing thesis and complexity classifications cite it when grounding simulation limits in RS-native units. The module organizes atomicity results for the tick together with irrationality properties of phi to support downstream information structures.

claimLet $τ_0$ be the fundamental tick, the minimum time quantum with $τ_0 = 1$ in RS-native units. The maximum computation rate satisfies $1/τ_0$ and no exact computation of $φ$ is possible.

background

Recognition Science takes the fundamental tick $τ_0 = 1$ as the RS time quantum from the Constants module. This module imports the Cost module to express computation limits directly from the ledger. Key objects include the tick as atomic time unit and results establishing that $φ$ has no rational roots via its minimal polynomial.

proof idea

This is a definition module, no proofs. It collects the fundamental tick definition, tick positivity and atomicity statements, and phi irrationality lemmas to prepare the ground for information-theoretic bounds.

why it matters in Recognition Science

This module supplies the time quantum and rate bounds required by ChurchTuringPhysicsStructure (IC-003) for extending the Church-Turing thesis to physics and by PhysicsComplexityStructure (IC-005) for locating physics in the complexity zoo. It closes the step from the RS ledger to explicit computation limits.

scope and limits

Does not derive explicit numerical rates beyond the tick bound.
Does not treat non-RS physical models.
Does not incorporate quantum-mechanical details.

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