pith. machine review for the scientific record. sign in
def definition def or abbrev

ic002_certificate

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

formal statement (Lean)

 191def ic002_certificate : String :=

proof body

Definition body.

 192  "═══════════════════════════════════════════════════════\n" ++
 193  "  IC-002: COMPUTATION LIMITS — STATUS: DERIVED\n" ++
 194  "═══════════════════════════════════════════════════════\n" ++
 195  "✓ tick_pos:                 τ₀ > 0\n" ++
 196  "✓ max_rate_pos:             1/τ₀ > 0\n" ++
 197  "✓ computation_limits:       Irrational φ (core constraint)\n" ++
 198  "✓ no_exact_phi_computation: ∀ q : ℚ, q ≠ φ\n" ++
 199  "✓ landauer_energy_pos:      k_B T ln(2) > 0\n" ++
 200  "✓ landauer_scales_with_temp: monotone in T\n" ++
 201  "✓ bremermann_limit_pos:     B = 2/ℏ > 0\n" ++
 202  "✓ phi_powers_unbounded:     φⁿ → ∞\n"
 203
 204end ComputationLimitsStructure
 205end Information
 206end IndisputableMonolith

depends on (14)

Lean names referenced from this declaration's body.