def
definition
circuitLedgerCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Complexity.CircuitLedger on GitHub at line 337.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
334 /-- The open gap is identified -/
335 open_gap : SpectralTuringBridgeHypothesis
336
337def circuitLedgerCert : CircuitLedgerCert where
338 capacity_bound := fun _n c => circuit_capacity_bound c
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