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
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.