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

circuitLedgerCert

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)

 337def circuitLedgerCert : CircuitLedgerCert where
 338  capacity_bound := fun _n c => circuit_capacity_bound c

proof body

Definition body.

 339  moat_width := fun _n f h => moat_width_unsat f h
 340  blind_decoder := fun _n M _hM g => adversarial_failure M g
 341  separation := circuitSeparation
 342  open_gap :=
 343    { spectral_gap_positive := fun _n => ⟨1/2, by norm_num, by norm_num⟩
 344      rhat_convergence := fun n => ⟨n, Nat.le_succ n⟩
 345      simulation_cost_per_step := fun n => ⟨n / 2, le_refl _⟩
 346      tm_time_lower_bound := fun n => ⟨n * (n / 2), le_refl _⟩ }
 347
 348end -- noncomputable section
 349
 350end CircuitLedger
 351end Complexity
 352end IndisputableMonolith

depends on (8)

Lean names referenced from this declaration's body.