OAI/NumberTheory/TwoPoint/Circuits/CircuitExceptionBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The recursive error certificate has polynomial size. Only this coarse bound, rather than the detailed shape of its gates, is used by the next stage.

  1. def OAI.TwoPointCorrelations.AC0Circuit.exceptionPolynomialBound line 13
  2. theorem OAI.TwoPointCorrelations.AC0Circuit.exceptionSizeBound_le line 16