Certificates, semantic minima and natural arithmetic
On this page · Permalink · Source line 251
WHAT THE FORMAL OBJECTS DO AND DO NOT COMPUTE DegreeLE d f is an inductive representation predicate. Its constructors build zero, a monomial represented by a variable-occurrence list of length at most \(d\), and XOR of certified functions. The polynomial evaluator XORs the monomial-list values. The source proves the equivalence between a degree certificate and such a finite representation.
Repeated indices are permitted. Boolean idempotence reduces their repetitions, so the representation gives the usual multilinear degree bound. The formal block supplies no separate canonical ANF normalization algorithm and no theorem that extracting homogeneous grades is computationally free. Zero has a degree-zero certificate. The Python degree helper's \(-1\) convention for zero is a mathematical convention outside the natural-valued formal bound.
CompleteSafeDegreeLE f d says that every positive point has some degree-\(d\) safe detector. It does not require one detector to cover all positives, and it places no efficiency bound on finding those detectors. Point indicators show that \(d=n\) suffices. A least-bound existence theorem then permits the noncomputable definition beta. Its specification supplies complete coverage; its minimality compares it with every sufficient natural bound.
AffineSafeDegreeLE f d universally quantifies every degree-one output function \(g\) and requires \(\beta(f+g)\le d\). The definition betaStar chooses its least common upper bound. There are finitely many Boolean functions on \(n\) inputs, so this least bound equals the main paper's maximum over affine output masks. It is a maximum over mask values, not a minimum over masks.
The source proves \(\beta(f)\le\beta^*(f)\le n\). The zero mask supplies the first inequality. The point-indicator bound supplies the second. Classical choice in the definitions is not a polynomial-time algorithm for computing these parameters.
All counters and degree bounds in this block are natural numbers. In 2 * betaStar f - 3, subtraction saturates at zero. Thus
in the formal natural-number statement is the integer inequality \(\max\{0,2\beta^*(f)-3\}\le T\). The nonsubtractive endpoint \(2\beta^*(f)\le T+3\) avoids ambiguity. Rounding at odd \(T\) is retained; the balanced cut is chosen by Toffoli count, not by half the gate-list length.