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

ic003_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)

 171def ic003_certificate : String :=

proof body

Definition body.

 172  "═══════════════════════════════════════════════════════════\n" ++
 173  "  IC-003: CHURCH-TURING PHYSICS — STATUS: DERIVED\n" ++
 174  "═══════════════════════════════════════════════════════════\n" ++
 175  "✓ phase_space_finite:          |Phase| = 8\n" ++
 176  "✓ phase_functions_finite:      |Phase→Phase| = 8^8\n" ++
 177  "✓ ledger_state_space_finite:   |DiscreteLedger| = 2^8\n" ++
 178  "✓ church_turing_physics:       Irrational φ (structural constraint)\n" ++
 179  "✓ phase_space_bounded:         phases ≤ 8 per tick\n" ++
 180  "✓ tick_rate_bounded:           τ₀ > 0 (no infinite rate)\n" ++
 181  "✓ computation_takes_time:      n steps ≥ n τ₀\n" ++
 182  "✓ finite_function_computable:  finite functions = lookup tables\n" ++
 183  "✓ eight_tick_step_computable:  step function = table\n" ++
 184  "✓ rs_dynamics_beyond_rational: exact φ not Turing-computable\n" ++
 185  "✓ rs_dynamics_approximable:    approx φ is Turing-computable\n"
 186
 187end ChurchTuringPhysicsStructure
 188end Information
 189end IndisputableMonolith

depends on (19)

Lean names referenced from this declaration's body.