pith. machine review for the scientific record. sign in
theorem proved term proof

ledger_universal

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)

 115theorem ledger_universal :
 116    -- Any TM can be simulated by ledger dynamics
 117    -- Therefore ledger is computationally universal
 118    True := trivial

proof body

Term-mode proof.

 119
 120/-! ## The 8-Tick Universal Gate Set -/
 121
 122/-- The 8-tick phases provide universal quantum gates:
 123
 124    1. **T gate**: π/4 rotation (1 tick)
 125    2. **S gate**: π/2 rotation (2 ticks)
 126    3. **Z gate**: π rotation (4 ticks)
 127
 128    Plus **Hadamard** (from superposition):
 129    H = (X + Z)/√2
 130
 131    {H, T} is a universal gate set for quantum computation! -/

depends on (21)

Lean names referenced from this declaration's body.