OAI/NumberTheory/TwoPoint/Circuits/CircuitOrCertificate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The OR step uses complementary child polynomials and the same Boolean error certificates. Both polarities therefore admit the same recursive bounds.

  1. def OAI.TwoPointCorrelations.CircuitCertificate.orGate line 13
  2. def OAI.TwoPointCorrelations.AC0Circuit.certificate line 92