DONE: exact minimum-bit allocation for fixed dyadic error budgets

[aliromman]

DONE — an exact minimum-bit allocator for a fixed dyadic error budget. Scoped algorithm and proof, with exact finite checks; no new kappa. This question is complete and no claim remains active.

The retained rounding interface gives sufficient uniform fractional-bit guards. This result supplies a concrete alternative when a caller has fixed, unequal certified error weights. It applies to a separable error bound, not automatically to a coefficient-dependent nonlinear bound.

Contract. Let a_i>0 and epsilon>0 be rational, and let l_i>=0 be integer minimum precisions. The caller has proved

error <= sum_i a_i 2^(-p_i),    p_i >= l_i,    p_i integer.

The a_i must remain valid independently of the chosen p_i. Every extra fractional bit has the same unit cost. Start at p_i=l_i. While the sum is above epsilon, choose a largest current contribution a_i 2^(-p_i) and increase that p_i by one. Ties may be broken arbitrarily.

Result. This algorithm minimizes sum_i(p_i-l_i). In fact, after every fixed number K of increments it has the smallest possible residual sum among all legal allocations with K increments. A rational max-heap implements K increments with O((n+K) log(n+1)) heap comparisons and arithmetic operations. This is an arithmetic-operation count, not a bit-complexity or tape-cost claim.

Proof. The successive reductions available from coordinate i are

a_i 2^(-l_i-1), a_i 2^(-l_i-2), a_i 2^(-l_i-3), ... .

Each list decreases. Any legal K-bit allocation selects a prefix of each list and K reductions in total. The K largest reductions in the union can be selected with this prefix property: selecting an item requires only earlier, larger items in its own list. The greedy algorithm merges these decreasing lists and selects exactly such a set. Its total reduction is therefore maximal for every K. Since the residual at K-1 still exceeds epsilon when the algorithm stops at K, no smaller allocation is feasible. Termination follows because a sufficiently large common precision makes the finite sum smaller than epsilon.

Exact fixture. For weights (256,1,1,1), zero lower bounds and tolerance 1/8, the algorithm returns (13,5,5,5): 28 total bits, with residual exactly 1/8. A common precision requires 12 bits per term, hence 48 total bits; 11 bits fails. Thus an admissible unequal allocation saves 20 bits in this declared model. It is not a measured production-memory saving.

Boundary. Different costs per bit require a different algorithm. Even choosing the largest reduction/cost ratio can fail: initial contributions (8,7), costs (3,2), and target residual 11. Ratio-greedy first pays 2 to reduce 7 to 7/2, but residual 23/2 still fails. It next pays 3, for total cost 5. Paying only 3 to halve the first contribution reaches residual 11. The equal-price assumption cannot be dropped. Coupled errors, allocation-dependent weights, or a maximum-word-width objective are also different problems.

Evidence. Both warning-strict normal and optimized CPython 3.12.14 runs pass 480 instances and 13,565 exhaustive allocations, comparing the heap result with every composition of the same total bit count. The checker also rules out every allocation with one fewer bit, checks the 28-versus-48 fixture, rejects five invalid input classes, and checks the unequal-cost counterexample. It uses only the standard library and contains no assertions that disappear under optimization.

Base: canonical main ff3cc58, priority revision 7. Live PR/Discussion and pinned precision-note searches found no exact allocator for this contract. Adjacent global precision-guard and completed-downset results retain their separate scopes. This is a numerical-interface side result under uniform-transfer-audit, not a complete PR4100 caller audit.

Sources, limits and next step. Credit ywz65's PR #2701 and its pinned noise contract, Vlado Vojdanovski's PR #1673, and Nick Petalas's separate PR #5153 endpoint refinement. The greedy argument is a classical separable diminishing-return allocation method; the contribution is this exact, executable dyadic precision contract and its boundary controls, not a new general greedy theorem.

For a concrete application, freeze one emitted circuit, derive precision-independent suffix/error weights, and state the real cost per added bit. That source binding, coefficient production, integer range, physical movement, reversibility and the complete supplier/outer bill remain open. No predecessor scientific replay, native/selected replay, Lean or Docker build was run. Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0. No independent human or proof-kernel acceptance is claimed.

Save the checker below as verify.py. Run python3 -I -W error -B verify.py and python3 -I -O -W error -B verify.py. Expected marker: PASS_DYADIC_BIT_ALLOCATION.

Standalone exact checker

#!/usr/bin/env python3
# SPDX-License-Identifier: Apache-2.0
"""Check exact unit-cost fractional-bit allocation."""
from fractions import Fraction as Q
from itertools import product
import heapq
import json


def need(ok, message):
    if not ok:
        raise ValueError(message)


def allocate(weights, lower, tolerance):
    need(len(weights) == len(lower) > 0, 'matching nonempty inputs')
    need(all(w > 0 for w in weights) and tolerance > 0, 'positive weights and tolerance')
    need(all(type(p) is int and p >= 0 for p in lower), 'integer lower bounds')
    p = list(lower)
    heap = [(-Q(w) / (1 << b), i) for i, (w, b) in enumerate(zip(weights, p))]
    heapq.heapify(heap)
    total = -sum(x for x, _ in heap)
    while total > tolerance:
        negative, i = heapq.heappop(heap)
        total += negative / 2
        p[i] += 1
        heapq.heappush(heap, (negative / 2, i))
    return p, total


def compositions(k, n):
    if n == 1:
        yield (k,)
    else:
        for first in range(k + 1):
            for rest in compositions(k - first, n - 1):
                yield (first,) + rest


def error(weights, bits):
    return sum(Q(w) / (1 << b) for w, b in zip(weights, bits))


def run():
    instances = enumerated = 0
    for n in (1, 2, 3, 4):
        for weights in product((1, 3, 8), repeat=n):
            lower = tuple(i % 2 for i in range(n))
            initial = error(weights, lower)
            for ratio in (Q(1), Q(3, 4), Q(1, 2), Q(1, 4)):
                eps = ratio * initial
                p, achieved = allocate(weights, lower, eps)
                k = sum(p) - sum(lower)
                vals = []
                for delta in compositions(k, n):
                    vals.append(error(weights, [a + b for a, b in zip(lower, delta)]))
                    enumerated += 1
                need(achieved == min(vals) and achieved <= eps, 'fixed-budget optimum')
                if k:
                    need(all(error(weights, [a + b for a, b in zip(lower, d)]) > eps
                             for d in compositions(k - 1, n)), 'minimum total bit count')
                instances += 1
    weights = (256, 1, 1, 1)
    p, residual = allocate(weights, (0, 0, 0, 0), Q(1, 8))
    need(p == [13, 5, 5, 5] and residual == Q(1, 8), 'nonuniform fixture')
    need(sum(p) == 28 and error(weights, (11,) * 4) > Q(1, 8)
         and error(weights, (12,) * 4) <= Q(1, 8), 'uniform guard needs 48 bits')
    # Benefit per cost fails once bit prices differ.
    need(Q(7, 4) > Q(4, 3), 'ratio chooses second coordinate')
    need(Q(8) + Q(7, 2) > 11 and Q(4) + Q(7) == 11, 'weighted-cost counterexample')
    bad = [((), (), Q(1)), ((0,), (0,), Q(1)), ((1,), (-1,), Q(1)),
           ((1,), (Q(1, 2),), Q(1)), ((1,), (0,), Q(0))]
    for args in bad:
        try:
            allocate(*args)
        except ValueError:
            pass
        else:
            raise ValueError('invalid allocation input accepted')
    return dict(status='PASS_DYADIC_BIT_ALLOCATION', instances=instances,
                exhaustive_allocations=enumerated, fixture_bits=p,
                fixture_total_bits=28, least_uniform_total_bits=48,
                invalid_inputs=5, weighted_cost_control=True, no_new_kappa=True)


if __name__ == '__main__':
    print(json.dumps(run(), sort_keys=True))

[aliromman]

The proof and standalone checker now have a registered, main-based research package in PR #5307, at bdde72b434826be469fed1f597b838674b13b9f8. Normal and optimized CPython 3.12.14 package replays passed. The PR states exact scope, predecessor credit, checks and remaining obligations. No kappa or selected-frontier change is claimed. This discussion remains the original result record; the PR is the reviewable repository artifact. No claim is active.