From 76447bc104e91e731ff1ddb663dcf867d7a52f86 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Mon, 2 Nov 2026 18:10:47 -0600 Subject: [PATCH 1/2] Certify complete adaptive row-menu bills --- research/adaptive-row-bill/PROOF.md | 100 ++++++++++++++++ research/adaptive-row-bill/README.md | 83 +++++++++++++ research/adaptive-row-bill/SOURCES.json | 18 +++ research/adaptive-row-bill/TASK.json | 105 +++++++++++++++++ research/adaptive-row-bill/VERIFY.json | 32 +++++ research/adaptive-row-bill/bills.py | 148 ++++++++++++++++++++++++ research/adaptive-row-bill/example.json | 7 ++ research/adaptive-row-bill/verify.py | 138 ++++++++++++++++++++++ 8 files changed, 631 insertions(+) create mode 100644 research/adaptive-row-bill/PROOF.md create mode 100644 research/adaptive-row-bill/README.md create mode 100644 research/adaptive-row-bill/SOURCES.json create mode 100644 research/adaptive-row-bill/TASK.json create mode 100644 research/adaptive-row-bill/VERIFY.json create mode 100644 research/adaptive-row-bill/bills.py create mode 100644 research/adaptive-row-bill/example.json create mode 100644 research/adaptive-row-bill/verify.py diff --git a/research/adaptive-row-bill/PROOF.md b/research/adaptive-row-bill/PROOF.md new file mode 100644 index 0000000000..607bdf91c6 --- /dev/null +++ b/research/adaptive-row-bill/PROOF.md @@ -0,0 +1,100 @@ +# Adaptive complete row bills + +At type i, let R_i be a finite nonempty set of nonnegative rational rows of +length n. A row must include all child, adapter and restoration charges of its +declared contract. Each node can choose its row independently. The local toll +is one. Define T(x)_i = max_{r in R_i} r x. A policy selects one row per type; +its matrix is A. These are mathematical costs, not physical native operations. + +The certificate has exactly two possible conclusions: + +1. A rational u >= 1 satisfies u = 1 + T(u). A policy A attains every row: + u = 1 + Au. The value u is the exact worst total over all finite depths and + adaptive choices. All allowed rows have the common strict contraction + bound r u <= q u_i, where q = max_i (u_i-1)/u_i < 1. +2. A legal policy A has a nonzero rational v >= 0 with Av >= v. Its unit-toll + work diverges in at least one type. Thus no finite worst total exists for + all types, and no common positive strict contraction weights exist. + +## Fixed policy alternative + +For M = I-A, eliminate columns without row swaps while each pivot is positive. +The off-diagonal Schur entries stay nonpositive. If pivot k is nonpositive, +set v_k=1 and v_j=0 for j>k. Solve the earlier triangular equations for v_i. +The signs give v>=0. The first k original equations are zero. The k-th original +equation is the nonpositive pivot, since earlier equations are zero. Every later +original row is nonpositive, since it sees only off-diagonal entries on the +support of v. Thus Mv<=0. This proves the second alternative. + +If all pivots are positive, substitution preserves nonnegativity. In particular +u=M^{-1}1 is positive, and Au=u-1>=0 gives u>=1. The weighted maximum norm +contracts by max_i (Au)_i/u_i<1. It follows that M^{-1}=sum_{j>=0} A^j>=0. +The vector u is the unit-toll total. This is the classical M-matrix alternative. + +## Finite policy improvement + +Start with any policy. Apply the fixed policy alternative. A noncontraction +witness ends the algorithm. Otherwise obtain its total u. For each type, select +a row that maximizes r u. Keep the old choice at a tie. Change only rows with +r u > u_i-1. If no row changes, u=1+T(u), as required. + +Suppose the next policy B also contracts, with total z. Then + + z-u = (I-B)^{-1}(1+Bu-u) >= 0. + +The last vector is nonzero, since some row changed strictly. The inverse contains +the identity, so at least one coordinate increases strictly. A policy cannot +recur: its total is unique, while all later totals are at least the preceding +total and each improvement is strict somewhere. There are only product_i |R_i| +policies. The uncapped exact algorithm therefore terminates. The implementation +has a declared 4096-policy default budget; exhaustion emits no certificate. +No polynomial runtime or small rational-growth bound is claimed. + +## Adaptive choices and exact attainment + +Let x_0=0 and x_{d+1}=1+T(x_d). Induction on depth proves that x_d is the maximum +work with d toll levels. Independent row choices are essential: every type may +use its own maximizing row at every node. More history cannot improve this +finite-horizon recursion. The positive vector u bounds every x_d from above. + +For x,y, nonnegative rows give + + |T(x)_i-T(y)_i| <= max_{r in R_i} r |x-y|. + +Thus T is q-Lipschitz in the u-weighted maximum norm. Iteration converges to u. +The fixed attaining policy has total (I-A)^{-1}1=u, so adaptivity cannot exceed +this one policy. More precisely, 0<=u-x_d<=q^d u. This also gives an explicit +finite-depth tail bound for every allowed schedule. + +For an unsafe witness, choose c>0 with 1>=cv. Then A^j1>=cv for every j. The +sum through d toll levels is at least dc v, which diverges on the nonzero +support of v. A positive weight w with Aw= 0 for x in values), 'Negative child coefficient') + parsed.append(values) + rows.append(parsed) + return rows + + +def dot(a, b): + return sum((x*y for x, y in zip(a, b)), Q(0)) + + +def fixed_policy(matrix): + """Return the unit-toll total or a nonnegative subeigenvector.""" + n = len(matrix) + a = [[Q(i == j)-matrix[i][j] for j in range(n)]+[Q(1)] + for i in range(n)] + for k in range(n): + if a[k][k] <= 0: + v = [Q(0)]*n + v[k] = Q(1) + for i in reversed(range(k)): + v[i] = -dot(a[i][i+1:n], v[i+1:])/a[i][i] + return None, v + for i in range(k+1, n): + if a[i][k]: + factor = a[i][k]/a[k][k] + for j in range(k, n+1): + a[i][j] -= factor*a[k][j] + total = [Q(0)]*n + for i in reversed(range(n)): + total[i] = (a[i][n]-dot(a[i][i+1:n], total[i+1:]))/a[i][i] + return total, None + + +def certify(problem, limit=4096): + rows = parse(problem) + require(type(limit) is int and limit > 0, 'Invalid policy budget') + policy = [0]*len(rows) + for step in range(limit): + total, witness = fixed_policy([r[a] for r, a in zip(rows, policy)]) + if witness is not None: + result = {'schema': 'adaptive-row-certificate/v1', 'status': 'unsafe', + 'policy': policy, 'witness': list(map(str, witness))} + check(problem, result) + return result + updated = policy.copy() + for i, choices in enumerate(rows): + values = [dot(row, total) for row in choices] + best = max(range(len(choices)), key=values.__getitem__) + if values[best] > total[i]-1: + updated[i] = best + if updated == policy: + q = max((x-1)/x for x in total) + result = {'schema': 'adaptive-row-certificate/v1', 'status': 'safe', + 'policy': policy, 'total': list(map(str, total)), + 'ratio': str(q)} + check(problem, result) + return result + policy = updated + raise ValueError('Policy budget exhausted; no certificate produced') + + +def check(problem, result): + """Check row inequalities and one attaining policy, without elimination.""" + rows = parse(problem) + n = len(rows) + require(type(result) is dict and result.get('schema') == 'adaptive-row-certificate/v1', + 'Invalid certificate') + policy = result.get('policy') + require(type(policy) is list and len(policy) == n + and all(type(a) is int and 0 <= a < len(rows[i]) + for i, a in enumerate(policy)), 'Invalid policy') + def vector(name): + value = result.get(name) + require(type(value) is list and len(value) == n, 'Wrong '+name+' width') + return list(map(rational, value)) + if result.get('status') == 'unsafe': + v = vector('witness') + require(all(x >= 0 for x in v) and any(v), 'Invalid witness') + require(all(dot(rows[i][a], v) >= v[i] for i, a in enumerate(policy)), + 'False unsafe witness') + return True + require(result.get('status') == 'safe', 'Invalid status') + total = vector('total') + q = rational(result.get('ratio')) + require(all(x >= 1 for x in total) and 0 <= q < 1, 'Invalid total or ratio') + for i, choices in enumerate(rows): + require(all(1+dot(row, total) <= total[i] for row in choices), + 'An allowed row exceeds the bill') + require(1+dot(choices[policy[i]], total) == total[i], 'Policy does not attain total') + require(all(dot(row, total) <= q*total[i] for row in choices), + 'False common contraction ratio') + return True + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('problem', type=Path) + parser.add_argument('--check', type=Path) + parser.add_argument('--policy-limit', type=int, default=4096) + args = parser.parse_args() + problem = json.loads(args.problem.read_text()) + if args.check: + check(problem, json.loads(args.check.read_text())) + print('PASS_ADAPTIVE_ROW_CERTIFICATE') + else: + print(json.dumps(certify(problem, args.policy_limit), indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/adaptive-row-bill/example.json b/research/adaptive-row-bill/example.json new file mode 100644 index 0000000000..79f1b83644 --- /dev/null +++ b/research/adaptive-row-bill/example.json @@ -0,0 +1,7 @@ +{ + "schema": "adaptive-row-bill/v1", + "rows": [ + [[0, "6/5"], ["1/5", 1]], + [["2/5", 0], [0, "1/4"]] + ] +} diff --git a/research/adaptive-row-bill/verify.py b/research/adaptive-row-bill/verify.py new file mode 100644 index 0000000000..9982a6a3df --- /dev/null +++ b/research/adaptive-row-bill/verify.py @@ -0,0 +1,138 @@ +"""Independent finite controls for the adaptive bill certificate. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +""" +from copy import deepcopy +from fractions import Fraction as Q +from itertools import combinations, combinations_with_replacement, permutations, product +import json +from pathlib import Path +from runpy import run_path + +ROOT = Path(__file__).resolve().parent +api = run_path(str(ROOT/'bills.py')) +certify, check = api['certify'], api['check'] + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def det(a): + n = len(a) + answer = Q(0) + for perm in permutations(range(n)): + value = Q((-1)**sum(perm[i] > perm[j] for i in range(n) for j in range(i+1, n))) + for i, j in enumerate(perm): + value *= a[i][j] + answer += value + return answer + + +def oracle(a): + n = len(a) + m = [[Q(i == j)-a[i][j] for j in range(n)] for i in range(n)] + for k in range(1, n+1): + for indices in combinations(range(n), k): + if det([[m[i][j] for j in indices] for i in indices]) <= 0: + return None + denominator = det(m) + return [det([[Q(1) if j == col else m[i][j] for j in range(n)] + for i in range(n)])/denominator for col in range(n)] + + +def problem(rows): + return {'schema': 'adaptive-row-bill/v1', + 'rows': [[[str(x) for x in row] for row in menu] for menu in rows]} + + +counts = {'families': 0, 'safe': 0, 'unsafe': 0, 'policies': 0, + 'prefix_checks': 0, 'rejections': 0} + + +def examine(rows): + p = problem(rows) + saved = deepcopy(p) + certificate = certify(p) + require(check(p, certificate), 'Certificate rejected') + totals = [] + for policy in product(*(range(len(menu)) for menu in rows)): + totals.append(oracle([rows[i][a] for i, a in enumerate(policy)])) + counts['policies'] += 1 + safe = all(t is not None for t in totals) + require((certificate['status'] == 'safe') == safe, 'Independent principal-minor decision differs') + if safe: + u = list(map(Q, certificate['total'])) + q = Q(certificate['ratio']) + expected = [max(t[i] for t in totals) for i in range(len(rows))] + require(u == expected and u in totals, 'Independent Cramer total differs') + value = [Q(0)]*len(rows) + for depth in range(9): + require(all(0 <= u[i]-value[i] <= q**depth*u[i] for i in range(len(rows))), + 'Finite-depth tail bound failed') + value = [1+max(sum(row[j]*value[j] for j in range(len(rows))) for row in menu) + for menu in rows] + counts['prefix_checks'] += 1 + require(p == saved, 'Input changed') + counts['families'] += 1 + counts[certificate['status']] += 1 + + +grid = list(product([Q(0), Q(1, 2), Q(3, 2)], repeat=2)) +menus = list(combinations_with_replacement(grid, 2)) +for rows in product(menus, repeat=2): + examine(rows) + +binary = list(product([Q(0), Q(1, 2)], repeat=3)) +for selected in product(binary, repeat=3): + examine([[row, tuple(Q(1, 2)-x for x in row)] for row in selected]) + +p = json.loads((ROOT/'example.json').read_text()) +c = certify(p) +require(c['total'] == ['5', '3'] and c['ratio'] == '4/5', 'Example differs') +examine([[[Q(x) for x in row] for row in menu] for menu in p['rows']]) + +bad = problem([[(0, 2), (0, 0)], [(0, 0), (2, 0)]]) +require(certify(bad)['status'] == 'unsafe', 'Mixed-row fault was missed') +require(oracle([[Q(0), Q(2)], [Q(0), Q(0)]]) is not None + and oracle([[Q(0), Q(0)], [Q(2), Q(0)]]) is not None, 'Whole-mode control failed') + +for n in [1, 4, 16, 64]: + rows = [] + for i in range(n): + row = [Q(0)]*n + if i+1 < n: + row[i+1] = Q(1, 2) + rows.append([[Q(0)]*n, row]) + result = certify(problem(rows)) + require(list(map(Q, result['total'])) == [2-Q(1, 2)**(n-i-1) for i in range(n)], + 'Chain total differs') + + +def rejects(function, *args): + try: + function(*args) + except (ValueError, TypeError, ZeroDivisionError): + counts['rejections'] += 1 + return + raise ValueError('Invalid input or certificate accepted') + + +for key, value in [('total', ['4', '3']), ('ratio', '1/2'), ('policy', [0, 0]), + ('policy', [True, 0]), ('total', ['5']), ('status', 'unknown')]: + fault = deepcopy(c) + fault[key] = value + rejects(check, p, fault) +unsafe = certify(bad) +for value in [['0', '0'], ['-1', '1'], ['1', '0'], ['1']]: + fault = deepcopy(unsafe) + fault['witness'] = value + rejects(check, bad, fault) +for value in [{}, {'schema': 'adaptive-row-bill/v1', 'rows': []}, + problem([[[-1]]]), problem([[[1, 0]]]), problem([[[]]]), + {'schema': 'adaptive-row-bill/v1', 'rows': [[[True]]]}]: + rejects(certify, value) +rejects(certify, p, 1) +rejects(certify, p, 0) +print(json.dumps({'status': 'PASS_ADAPTIVE_ROW_BILL', **counts}, sort_keys=True)) From 6621e59b773b179a0340627eadbe295eb5254d07 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Mon, 2 Nov 2026 18:12:14 -0600 Subject: [PATCH 2/2] Record adaptive bill verification and export evidence --- research/adaptive-row-bill/VALIDATION.md | 33 ++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 research/adaptive-row-bill/VALIDATION.md diff --git a/research/adaptive-row-bill/VALIDATION.md b/research/adaptive-row-bill/VALIDATION.md new file mode 100644 index 0000000000..37fcd390a0 --- /dev/null +++ b/research/adaptive-row-bill/VALIDATION.md @@ -0,0 +1,33 @@ +# Validation record + +Local interpreter: CPython 3.12.13, macOS arm64, standard library only. +The exact executable was +`/Users/aliromman/.local/share/uv/python/cpython-3.12-macos-aarch64-none/bin/python3.12`. + +The registered ordinary and optimized commands passed. Both emitted the same +receipt: 2538 families, 12200 policies, 181 safe, 2357 unsafe, 1629 prefix checks, +and 18 rejecting controls. A separate direct ordinary run also passed. +The independent oracle uses permutation determinants and Cramer's rule; it +imports neither the producer's elimination nor its policy decisions. + +At scientific commit `76447bc104e91e731ff1ddb663dcf867d7a52f86`, committed-byte +and owner-execute-mode checks passed for all eight package files. The official +export and its declared-input integrity check passed. Both scientific commands +passed from the exported files with empty PATH, no Git checkout and read-only +files/directories. All nine file hashes and modes, including export metadata, +remained unchanged. Ordinary and optimized stdout were identical. + +The checkout is shallow. Full-history source preflight was not claimed. The +package is a direct descendant of the declared canonical base; all provenance +pins resolve at that base. There are no external runtime inputs or side-branch +Git dependencies. This removes the missing-predecessor clean-checkout issue. + +Canonical main was fetched again before submission. Its base, priority and +selected-record files were unchanged. The initial complete overlap cache covered +409 open PRs and 6362 Discussion records. Submission checks read later Discussion +claims and new open PR bodies through PR6466. No matching row-menu certificate +was found. Sparse local notes and unpublished work remain coverage limits. + +Hosted CI is recorded in the PR after the published head is available. +No independent human review, formal proof-kernel acceptance, selected-supplier +replay or new kappa is claimed. No fragile workaround is used.