module module high

`IndisputableMonolith.Information.ComputationLimitsStructure`

This module defines the fundamental tick as the minimum time quantum in Recognition Science and assembles the associated computation limits structure. Researchers deriving the physical Church-Turing thesis or locating physics in the complexity zoo cite it. The module consists of definitions and supporting lemmas on the tick and phi properties built directly from the imported Constants and Cost modules.

claimThe fundamental tick satisfies $\tau_0 = 1$ tick (RS-native units). Maximum computation rate is the reciprocal of the tick. The golden ratio $\phi$ admits no exact finite computation and satisfies its minimal polynomial with no rational roots.

background

Recognition Science derives all physics from recognition costs and the forcing chain. This module sits in the Information domain and imports Constants, whose doc states "The fundamental RS time quantum (RS-native). $\tau_0 = 1$ tick.", together with Cost. It introduces the atomic time unit, position of ticks, maximum rate bounds, ledger-derived limits, and irrationality properties of $\phi$ that prevent exact computation.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the tick-based limits imported by ChurchTuringPhysicsStructure (IC-003: Physical Church-Turing Thesis) and PhysicsComplexityStructure (IC-005: Computational Complexity of Physics). It supplies the concrete time quantum and rate bounds required for those derivations of the RS answer to the physical Church-Turing question.

scope and limits

Does not derive the Physical Church-Turing Thesis itself.
Does not place physics in any specific complexity class.
Does not treat continuous-time or quantum computation models.
Does not prove rationality results for constants other than $\phi$.

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