OAI/NumberTheory/TwoPoint/Circuits/CircuitCertifiedGate.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The sampled gate carries a Boolean certificate for all its errors: the new single-hit failure test together with the child certificates.

  1. def OAI.TwoPointCorrelations.AC0Circuit.combineGateException line 16
  2. lemma OAI.TwoPointCorrelations.AC0Circuit.combineGateException_eval line 22
  3. lemma OAI.TwoPointCorrelations.AC0Circuit.combineGateException_size line 29
  4. lemma OAI.TwoPointCorrelations.AC0Circuit.combineGateException_depth line 36
  5. theorem OAI.TwoPointCorrelations.exists_certified_and_sample line 49