From bbf28e1a678e1a9cbc633f35de5231eaab967f01 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 28 Oct 2026 12:53:35 +0000 Subject: [PATCH] feat(research): optimize logical suffix defect guards --- research/suffix-guard-allocation/README.md | 143 ++++++++++++++ research/suffix-guard-allocation/SOURCES.json | 36 ++++ research/suffix-guard-allocation/TASK.json | 83 +++++++++ research/suffix-guard-allocation/VERIFY.json | 36 ++++ research/suffix-guard-allocation/verify.py | 176 ++++++++++++++++++ 5 files changed, 474 insertions(+) create mode 100644 research/suffix-guard-allocation/README.md create mode 100644 research/suffix-guard-allocation/SOURCES.json create mode 100644 research/suffix-guard-allocation/TASK.json create mode 100644 research/suffix-guard-allocation/VERIFY.json create mode 100644 research/suffix-guard-allocation/verify.py diff --git a/research/suffix-guard-allocation/README.md b/research/suffix-guard-allocation/README.md new file mode 100644 index 0000000000..a2c34438af --- /dev/null +++ b/research/suffix-guard-allocation/README.md @@ -0,0 +1,143 @@ +# Optimal unequal guards for the THREE-base logical error ledger + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: finite certificate and scoped integer-optimality proof. There is +no new kappa or selected-frontier change. + +David Ganz / Dugongue's [PR #4510](https://github.com/CrocSwap/integer-mult-bounds/pull/4510) +supplies a complete suffix-error ledger for the historical THREE-base native +word rewritten in #4505. Its logical perturbation theorem permits unequal +ADD and SCALE defect tolerances. This package chooses those tolerances to +minimize a stated precision charge. The ledger and perturbation theorem are +cited premises, not new derivations or re-verification deliverables. This is +not the selected #6030 word. + +## Result and contract + +Fix a target logical output-error allowance `2^-b`, with integer `b >= 0`. +Inputs are exact. Every entire-field ADD defect has norm at most +`2^(-b-g_A)` and every entire-field SCALE defect at most `2^(-b-g_S)`. +All other event classes are exact, and logical free warp operators are +isometries, exactly as in #4510's ADD/SCALE corollary. The guards `g_A,g_S` +are nonnegative integers. They describe absolute logical defect tolerances, +not physical mantissa widths or componentwise rounding quanta. + +For each published output row `i`, write its ADD/SCALE weights as `a_i,s_i`. +The sufficient constraints are + +```text +a_i / 2^g_A + s_i / 2^g_S <= 1, for every output i. +``` + +Define the event-weighted guard charge + +```text +J = N_ADD * g_A + N_SCALE * g_S. +``` + +This is a declared logical precision objective. It is not peak storage, a +physical instruction bill, or measured runtime. A common base precision `b` +would add the same `(N_ADD+N_SCALE)*b` to every allocation. + +| Orientation | ADD/SCALE events | Least uniform guards | Unique optimal guards | Uniform J | Optimal J | Saved | +|---|---|---|---|---:|---:|---:| +| Forward | 16,263 / 1,168 | 11 / 11 | 11 / 9 | 191,741 | 189,405 | 2,336 | +| Backward | 16,271 / 1,168 | 13 / 13 | 13 / 11 | 226,707 | 224,371 | 2,336 | + +At the optimal assignments, the maximum sufficient output bound, divided by +`2^-b`, is `7257/8192` forward, attained at `L222`, and `827/1024` backward, +attained at `L328`. Every one of the 632 output constraints is checked in +each orientation. Both SCALE tolerances are four times their uniform values. +No smaller event-weighted charge satisfies this particular ledger. + +## Optimality proof + +Nonnegative weights make every constraint monotone in each guard. Forward, +`max a_i = 2355/2 > 2^10`, so every feasible allocation has `g_A >= 11`, +regardless of the SCALE guard. An allocation with `g_A >= 12` costs at least +`12*16263 = 195156 > 189405`, even with zero SCALE guard. Consequently any +allocation competitive with the displayed candidate must have `g_A = 11`. +At that guard, `g_S = 8` violates a published row, while `g_S = 9` satisfies +every row. Positivity of the SCALE event count makes the optimum unique. + +Backward, `max a_i = 4300 > 2^12` forces `g_A >= 13`. Taking `g_A >= 14` +costs at least `14*16271 = 227794 > 224371`. At `g_A = 13`, `g_S = 10` +violates a row, whereas `g_S = 11` satisfies every row. This proves the +second unique optimum. The rejecting maxima are `20155/16384` forward and +`2233/2048` backward. The generated receipt retains these exact values. Uniform +optimality is checked by the same monotonicity argument. + +The verifier separately enumerates every integer pair whose charge is at +most the uniform benchmark. That search clears row denominators and uses +integer inequalities, rather than the Fraction-based monotonicity certificate. +It confirms both optima without dropping or grouping output rows. + +## Reproduction + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/suffix-guard-allocation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/suffix-guard-allocation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/suffix-guard-allocation +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/suffix-guard-allocation --check-source-history +``` + +Any CPython 3.12 executable can replace the displayed local path. Expected +markers are `PASS_SUFFIX_GUARD_ALLOCATION`, `PASS_REGISTERED_RESEARCH_PACKAGE` +and `PASS_RESEARCH_COMMIT_BYTES`. The direct command prints a generated JSON +receipt bound to the input and every package file. It writes no output files. + +The source ledger is pinned to base +`721c03822c421b7f7fcbb2598993b947c4d88419` in SOURCES.json. In a sparse +checkout, materialize `research/native-suffix-errors` before running. The +verifier reads that JSON but imports or executes no predecessor code. + +Fifteen rejection controls cover insufficient ADD/SCALE guards, a needlessly +large ADD guard that cannot satisfy the optimality certificate, malformed +guards and corrupted input bytes. They remain active under optimization. +The code has no recursion, subprocesses or writes. Every function is below +60 lines; input bytes, rows, event counts and enumeration ranges are bounded. +Python allocates during exact arithmetic, a managed-runtime deviation from +fixed-capacity allocation; the authenticated one-MiB input and finite ranges +bound this artifact's live objects. No general-purpose optimizer is claimed. +Warning-strict compilation and the registered normal/optimized checks supply diagnostics; Ruff and Pyright were +unavailable. If this fixed artifact becomes a reusable allocation API, add +typed boundary validation and a configured static checker. The rejection helper +uses bounded indirect dispatch to only three local validators, with no external +callback registration; a reusable API should keep those targets explicit. + +## Limitations + +Optimality concerns the sufficient inequalities in the published ledger, +not the smallest true error of the native word. Physical norm conversion, +all non-ADD/SCALE defects, recursive feedback, rounding-grid ownership, +restoration, peak memory and a complete paid caller remain open. The allocation +must not be transferred to another word or to #6030 without new source-bound +weights. No selected framework assumption is discharged. Independent human +and formal proof-kernel review are unclaimed. + +The predecessor's scientific replay, the selected cold replay, Lean and +Docker were not run. Source integrity is checked; the underlying source +ledger's mathematical correctness is assumed. + +## Open next questions + +Can one physical implementation supply these unequal entire-field defect +contracts with a smaller complete arithmetic bill? Start with a literal ADD +and SCALE implementation, translate their componentwise errors into the +ledger norm, then price width conversion, routing and restoration. Those +physical contracts are the blocker. Optimizing this logical charge alone +does not establish the saving in a multiplier. + +## Credit + +David Ganz / Dugongue supplied #4510's logical perturbation theorem, complete +row ledger and unequal-budget interface, and #4505's rewritten native word. +Its #4502 borrowed adapters, #4499 gauges, #4494/#4489 source selectors and +the retained zxv, Jacob Alan Sussman, Cinna Davis and Jeremy Kothe lineage +retain their credit. Reverse sensitivity and impulse-response bounds are +classical. The new result is the explicit nonuniform allocation, its declared +objective and its exact optimum certificate. No predecessor credit line or +source file is changed. diff --git a/research/suffix-guard-allocation/SOURCES.json b/research/suffix-guard-allocation/SOURCES.json new file mode 100644 index 0000000000..127cb1623e --- /dev/null +++ b/research/suffix-guard-allocation/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/native-suffix-errors/RESULT.json", + "usage": "input", + "git_blob": "b65a4e82a695c9f2a26646dac4ac70fc6f94206d", + "sha256": "38fa4bc3b526b12dbb89a3841e71b4778a26746632198995794544ad2b91b6e6" + }, + { + "path": "research/native-suffix-errors/README.md", + "usage": "provenance", + "git_blob": "accede173c82a0855e0a1d30d11728e1171def67", + "sha256": "3edbe8802b9156711ea74ea946c94573a8cd51783d6b5a6cb5f8bd8beb568bfd" + }, + { + "path": "research/native-suffix-errors/PROOF.md", + "usage": "provenance", + "git_blob": "9dbbd98054303d2c121dd3cc9510d396f1a563a0", + "sha256": "ff669f68609f906a5f5263a5388bca88e6774b5ca1146126c5ea56cbd80adaee" + } + ] +} diff --git a/research/suffix-guard-allocation/TASK.json b/research/suffix-guard-allocation/TASK.json new file mode 100644 index 0000000000..aa8c2ffd20 --- /dev/null +++ b/research/suffix-guard-allocation/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Unique event-weighted integer ADD/SCALE guard optima on the published PR4510 rewritten THREE-base logical suffix ledger, in both orientations.", + "scope_change_reason": "This is a finite precision-allocation side result on a cited historical caller, not an audit or a proof of the selected precision_tape assumption.", + "bottleneck_link": "Unequal logical defect tolerances can lower a declared precision charge; physical rounding, norm conversion and a complete paid implementation remain necessary before a precision_tape benefit transfers.", + "budget_minutes": 60, + "stop_rule": "Ship the first improved feasible allocation with an exact certificate; do not extend to other words or event classes.", + "outcome": "completed", + "evidence": "verify.py checks 632 output constraints per orientation, unique optima (11,9) and (13,11), exact savings 2336 each, an integer-arithmetic exhaustive oracle and 15 rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a physical ADD/SCALE implementation realize these unequal logical defect tolerances at lower complete cost?", + "why_it_matters": "The event-weighted guard objective alone does not imply physical storage, runtime or a multiplication improvement.", + "first_step": "Translate literal componentwise ADD/SCALE error contracts into the retained logical norm and price all width conversion, routing and restoration.", + "blocked_by": "No physical rounding implementation or complete caller invoice is supplied." + } + ] +} diff --git a/research/suffix-guard-allocation/VERIFY.json b/research/suffix-guard-allocation/VERIFY.json new file mode 100644 index 0000000000..ddaf8d3f2f --- /dev/null +++ b/research/suffix-guard-allocation/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/native-suffix-errors/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact source pin; all 1264 new allocation constraints; monotonicity optimum certificates; independent integer enumeration; 15 rejection controls; generated hash-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact source pin; all 1264 new allocation constraints; monotonicity optimum certificates; independent integer enumeration; 15 rejection controls; generated hash-bound receipt." + } + ] +} diff --git a/research/suffix-guard-allocation/verify.py b/research/suffix-guard-allocation/verify.py new file mode 100644 index 0000000000..e3608d9315 --- /dev/null +++ b/research/suffix-guard-allocation/verify.py @@ -0,0 +1,176 @@ +#!/usr/bin/env python3 +"""Optimize two logical defect guards on the cited PR4510 suffix ledger. + +Produced by Nick Petalas. Apache-2.0. +The ledger and its logical perturbation theorem are David Ganz's PR4510. +""" +from fractions import Fraction +from hashlib import sha256 +import json +from pathlib import Path +import platform + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +INPUT = "research/native-suffix-errors/RESULT.json" +PIN = "38fa4bc3b526b12dbb89a3841e71b4778a26746632198995794544ad2b91b6e6" +EXPECTED = { + "forward": (16263, 1168, 11, 9, 189405, Fraction(7257, 8192)), + "backward": (16271, 1168, 13, 11, 224371, Fraction(827, 1024)), +} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def check_pin(raw): + require(len(raw) <= 2 * 1024 * 1024, "input exceeds two MiB") + require(sha256(raw).hexdigest() == PIN, "source hash mismatch") + + +def load_cases(raw): + check_pin(raw) + payload = json.loads(raw) + require(payload["status"] == "PASS_NATIVE_SUFFIX_ERROR_CERTIFICATES", + "unexpected input schema") + cases = {} + for direction in EXPECTED: + data = payload["results"]["rewritten"][direction] + source_rows = data["persistent_output_rows"] + require(len(source_rows) == 632, "expected 632 published output rows") + rows = tuple((Fraction(r["weights"]["add"]), + Fraction(r["weights"]["scale"])) for r in source_rows) + require(all(a >= 0 and s >= 0 for a, s in rows), "negative weight") + counts = data["events_per_class"] + costs = counts["add"], counts["scale"] + require(all(type(c) is int and 0 < c <= 20000 for c in costs), + "invalid event count") + cases[direction] = rows, costs, tuple(r["role"] for r in source_rows) + return cases + + +def bound(rows, guards): + ga, gs = guards + require(type(ga) is int and type(gs) is int, "guards must be integers") + require(0 <= ga <= 256 and 0 <= gs <= 256, "guard out of range") + return max(a / (1 << ga) + s / (1 << gs) for a, s in rows) + + +def certificate(rows, costs, guards): + """A monotonicity certificate excludes every cheaper integer pair.""" + ca, cs = costs + ga, gs = guards + require(ga > 0 and gs > 0, "this certificate needs positive guards") + maximum = bound(rows, guards) + require(maximum <= 1, "candidate violates an output constraint") + add_floor = max(a for a, _ in rows) / (1 << (ga - 1)) + require(add_floor > 1, "one fewer ADD guard is not excluded") + cost = ca * ga + cs * gs + require(ca * (ga + 1) > cost, "larger ADD guard could be cheaper") + scale_floor = bound(rows, (ga, gs - 1)) + require(scale_floor > 1, "one fewer SCALE guard is not excluded") + return {"guards": list(guards), "charge": cost, + "maximum_output_bound": str(maximum), + "add_only_lower_witness": str(add_floor), + "next_add_cost_floor": ca * (ga + 1), + "one_less_scale_witness": str(scale_floor)} + + +def enumerate_optimum(rows, costs, upper): + """Independent bounded search, using integer inequalities on every row.""" + ca, cs = costs + max_a, max_s = upper // ca, upper // cs + require(max_a <= 32 and max_s <= 256, "enumeration capacity exceeded") + # Clear rational row denominators before evaluating any candidate. + integer_rows = [] + for a, s in rows: + denominator = a.denominator * s.denominator + integer_rows.append((int(a * denominator), int(s * denominator), + denominator)) + winners, tested = [], 0 + best = upper + for ga in range(max_a + 1): + for gs in range((upper - ca * ga) // cs + 1): + tested += 1 + feasible = all(a * (1 << gs) + s * (1 << ga) + <= d * (1 << (ga + gs)) + for a, s, d in integer_rows) + cost = ca * ga + cs * gs + if feasible and cost <= best: + if cost < best: + winners = [] + best = cost + winners.append((ga, gs)) + require(winners, "no feasible allocation") + return best, winners, tested + + +def expect_rejection(function, *args): + try: + function(*args) + except (ValueError, TypeError): + return + raise ValueError("negative control was accepted") + + +def controls(cases, raw): + count = 0 + for direction, (rows, costs, _) in cases.items(): + _, _, ga, gs, _, _ = EXPECTED[direction] + for bad in [(ga - 1, gs), (ga, gs - 1), (ga + 1, gs)]: + expect_rejection(certificate, rows, costs, bad) + count += 1 + for bad in [(-1, gs), (ga, 257), (True, gs), (ga, "9")]: + expect_rejection(bound, rows, bad) + count += 1 + expect_rejection(check_pin, raw + b" ") + return count + 1 + + +def run_case(direction, case): + rows, costs, roles = case + ca, cs, ga, gs, expected_cost, expected_bound = EXPECTED[direction] + require(costs == (ca, cs), "source event counts differ") + result = certificate(rows, costs, (ga, gs)) + require(result["charge"] == expected_cost, "unexpected optimum charge") + require(Fraction(result["maximum_output_bound"]) == expected_bound, + "unexpected output bound") + uniform = ga + uniform_cost = (ca + cs) * uniform + require(bound(rows, (uniform, uniform)) <= 1, "uniform is infeasible") + require(bound(rows, (uniform - 1, uniform - 1)) > 1, + "uniform benchmark is not minimal") + best, winners, tested = enumerate_optimum(rows, costs, uniform_cost) + require(best == expected_cost and winners == [(ga, gs)], + "independent enumeration disagrees") + values = tuple(a / (1 << ga) + s / (1 << gs) for a, s in rows) + result.update({"output_rows": len(rows), "event_counts": list(costs), + "uniform_guards": [uniform, uniform], + "uniform_charge": uniform_cost, + "charge_saved": uniform_cost - expected_cost, + "unique_optimum": True, "pairs_enumerated": tested, + "maximizing_roles": [r for r, v in zip(roles, values) + if v == expected_bound]}) + return result + + +def main(): + raw = (ROOT / INPUT).read_bytes() + cases = load_cases(raw) + result = {direction: run_case(direction, cases[direction]) + for direction in EXPECTED} + control_count = controls(cases, raw) + names = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + hashes = {name: sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in names} + print(json.dumps({"status": "PASS_SUFFIX_GUARD_ALLOCATION", + "claim_type": "finite certificate and scoped optimum", + "python": platform.python_version(), "input_sha256": PIN, + "package_sha256": hashes, "results": result, + "rejection_controls": control_count}, sort_keys=True)) + + +if __name__ == "__main__": + main()