CircuitLedgerCert

formal source

 317/-! ## Certificate -/
 318
 319/-- **CircuitLedgerCert**: bundles all proved results in this module. -/
 320structure CircuitLedgerCert where
 321  /-- A poly-size circuit has poly-bounded Z-capacity -/
 322  capacity_bound : ∀ n : ℕ, ∀ c : BooleanCircuit n,
 323    CircuitZCapacity c ≤ 2 * c.gate_count
 324  /-- UNSAT formulas have a defect moat of width ≥ 1 -/
 325  moat_width : ∀ n : ℕ, ∀ f : CNFFormula n, f.isUNSAT →
 326    ∀ a : Assignment n, satJCost f a ≥ 1
 327  /-- No fixed-view decoder over <n variables is universal -/
 328  blind_decoder : ∀ n : ℕ, ∀ M : Finset (Fin n), M.card < n →
 329    ∀ g : ({i // i ∈ M} → Bool) → Bool,
 330      ∃ (b : Bool) (R : Fin n → Bool),
 331        g (restrict (enc b R) M) ≠ b
 332  /-- The full separation structure holds -/
 333  separation : CircuitSeparation
 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