Binary bit cost of the first-success counting parameter #
For each fixed width k, the existing countingThresholdBase k has an ordinary polynomial-time
native machine from binary inverse budget B to binary threshold base. The same machine works
for every B, including zero. The width is fixed before the input, and is not a runtime unary
parameter.
The proof refines the selector to a bounded first-match scan through its proven logarithmic exponent bound. Only the exponent indices and logarithms are unary; the retained budget, powers of two, coefficient sums and integer-test operands remain binary. Existing plain providers charge the entire candidate-index list, captured input, arithmetic intermediates and final output. The scan may materialize the candidate list; no sharper polynomial degree or workspace claim is made.
Main results #
Cslib.Logic.PL.ClauseSet.Sparsification.computableInPolyTime_countingThresholdBase: a uniform binary-input/output certificate for each fixed width.Cslib.Logic.PL.ClauseSet.Sparsification.exists_length_countingThresholdBase_le: the full binary output length is linear in the binary input length, for width-dependent constants.
References #
This is an implementation of the parameter-search bit-cost claim for σ = 1/B; it does not
certify tree construction, a counting algorithm, general rational encodings or runtime width.
For each fixed width, one native polynomial-time machine computes the unchanged first-success threshold from a binary inverse budget, returning the complete binary output. Widths zero and one and inverse budget zero use the existing total default.
The complete binary output has a linear bit-length bound in the complete binary input. The additive constant depends only on the fixed width; all inverse budgets, including zero, are covered.