OAI/NumberTheory/TwoPoint/Circuits/CircuitBravermanApproximation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The combinatorial approximation stage of Braverman's proof, with a fully explicit error circuit and coarse quantitative bounds. The depth estimate is sufficient for the fixed-depth comparison.

  1. theorem OAI.TwoPointCorrelations.AC0Circuit.polynomial_error_approximation line 12