From 1262dbcf61a069412dbf1e826fc6a860c0c87f45 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 19:37:01 +0000 Subject: [PATCH] feat(research): bound skew-radix chirp table travel sharply --- research/chirp-radix-order/PROOF.md | 135 +++++++++++++++ research/chirp-radix-order/README.md | 64 +++++++ research/chirp-radix-order/SOURCES.json | 24 +++ research/chirp-radix-order/TASK.json | 83 +++++++++ research/chirp-radix-order/VERIFY.json | 34 ++++ research/chirp-radix-order/verify.py | 220 ++++++++++++++++++++++++ 6 files changed, 560 insertions(+) create mode 100644 research/chirp-radix-order/PROOF.md create mode 100644 research/chirp-radix-order/README.md create mode 100644 research/chirp-radix-order/SOURCES.json create mode 100644 research/chirp-radix-order/TASK.json create mode 100644 research/chirp-radix-order/VERIFY.json create mode 100644 research/chirp-radix-order/verify.py diff --git a/research/chirp-radix-order/PROOF.md b/research/chirp-radix-order/PROOF.md new file mode 100644 index 0000000000..94291e723d --- /dev/null +++ b/research/chirp-radix-order/PROOF.md @@ -0,0 +1,135 @@ +# Largest-radix-first cached chirp table movement + +This is a scoped written proof. It concerns the sequential table tape of +Ryanson Jonathan's PR #4325 suffix-product chirp enumerator, with a changed +axis layout. It does not audit that package or Cinna Davis's PR #4100. + +## Contract + +There are d >= 1 axes of dyadic lengths t_0,...,t_(d-1), each at least two, +and T is their product. The tape contains the tables in that order. Each +entry occupies P >= 1 consecutive cells. Table k starts at +O_k = P sum_(i= 2. + +To prove it, first omit the final return. The last table read is the final +entry of table zero, so the final head is t_0 P. If B is the total backward +distance in units of P, the total distance before return is t_0 P+2BP. +Returning adds another t_0 P. + +For each k < d-1, the reverse table traversal crosses from table k+1 to +entry zero of table k exactly T/L_(k+1) times, including initialization. +Its baseline backward distance is t_k+1. If the carry stops at j=k+1, +the newly read entry of table j has index b in 1,...,t_j-1, so this one +crossing has an additional backward distance b. Each such b occurs +T/L_(j+1) times. Thus + +``` +B = sum_(k=0)^(d-2) (t_k+1) T/L_(k+1) + + sum_(j=1)^(d-1) [t_j(t_j-1)/2] T/L_(j+1). +``` + +Substitution proves (1). Every forward sweep, initial seek and final +return is included; counting only the distance between entry starts would +give a different identity. + +## Sharp uniform bound after choosing a fastest axis + +Choose any largest radix M as t_0. The remaining axes can stay in their +relative order. Then + +``` +Q <= 7 T P. (2) +``` + +No bound on max(t_i)/min(t_i) is needed. For d=1, Q=2TP. +For d>=2 put b=2^(-(d-1)). Since t_i>=2 and t_i<=M, + +``` +2M/T <= 2b, +2 sum_(k=0)^(d-2) (t_k+1)/L_(k+1) + = 2 sum_(k=0)^(d-2) (1+1/t_k)/L_k + <= 2 + 2/M + (6/M)(1-2b), +sum_(j=1)^(d-1) (t_j-1)/L_j + <= (2-2/M)(1-b). +``` + +The middle sum over k>=1 is empty when d=2, and the displayed bound then +has 1-2b=0. Adding gives the explicit stronger estimate + +``` +Q/(TP) <= 4 + 6/M - 10b/M <= 7, +``` + +because M>=2 and b>0. This proves (2). + +The constant seven cannot be decreased uniformly in d. With every t_i=2, +(1) gives the exact formula + +``` +Q/P = 7*2^d - 10, +Q/(TP) = 7 - 10/2^d. +``` + +It approaches seven from below. This is sharpness of one specified table +schedule, not an optimality theorem over every possible tape algorithm. + +## First application and boundary + +On the skew two-axis layout (2,512), (1) gives Q=264708P. Choosing the +512-axis fastest gives (512,2) and Q=3078P, with T=1024. The latter is +1539/512 emitted word volumes. Both counts include the table-head return. +PR #4325's displayed 258.5 ratio omits that final return and rounds the +ratio; the metrics should not be silently mixed. + +The exact phase at an original named coordinate x is the product of the +same one-axis factors in either order. The new enumeration emits those +coordinates in the new order. A consumer must already accept that order, +or separately pay for layout conversion. This proof supplies no free +transpose, physical encoded controller, table construction, cache cleanup, +multiplier implementation, supplier admission or new kappa. + +## Executable scope + +The independent literal counter executes every table read and carry. The +closed-form implementation never calls that counter. Complete small +dyadic domains compare both, and a separate exact quadratic-exponent cache +checks the association of emitted phases with original axis names. The +binary family is checked through 64 axes by exact arithmetic. The written +argument, rather than that finite range, proves the all-size assertion. + +Executable inputs have at most 64 axes, radices at most 65536, word width +at most 64 and product bit length at most 1025. Literal enumerations are +capped at 131072 records; phase checks at 4096. These are verifier resource +bounds. All loops have finite bounds, and all contracts remain enabled +under optimized Python. Functions are below 60 lines. There is no recursion, +dynamic loading, network, or write path. Python's managed integer, JSON and +dictionary allocations are a Power-of-Ten rule-3 deviation, bounded by the +input and fixture limits. Standard-library iterator and key callbacks have +fixed targets and no shared mutable state. Warning-strict execution is the +available interpreted diagnostic; no global analyzer configuration changes. diff --git a/research/chirp-radix-order/README.md b/research/chirp-radix-order/README.md new file mode 100644 index 0000000000..b455a50d2d --- /dev/null +++ b/research/chirp-radix-order/README.md @@ -0,0 +1,64 @@ +# Sharp table travel for skew-radix cached chirps + +Choosing a largest radix as the fastest axis gives table-head movement +`Q <= 7TP` for the complete cached chirp enumeration, including initialization +and the final return to cell zero. Here `T` is the number of tensor records +and each table entry has `P` cells. There is no largest/smallest radix-ratio +restriction. The constant seven is sharp for this specified schedule: with +`d` binary axes, `Q/P = 7*2^d - 10`. + +On the two-axis layout `(2,512)`, the exact closed table walk costs +`264708P`. Putting the 512-axis first costs `3078P`, with the same 1024 +records. This is a count of unit head moves, not a timing measurement. + +Claim type: scoped written mathematical proof with exact finite +corroboration. [PROOF.md](PROOF.md) gives the exact movement identity, +its all-size bound, sharpness family and physical boundary. No new kappa +or selected-frontier change is claimed. + +## Reproduction + +From the repository root, CPython 3.12 and the standard library suffice: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/chirp-radix-order/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/chirp-radix-order +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/chirp-radix-order --check-source-history +``` + +The standalone verifier prints `PASS_CHIRP_RADIX_ORDER` with exact counts +and SHA256 hashes of all six package files. It compares a literal complete +table walker with a separately implemented closed formula, checks the sharp +binary family through 64 axes, and executes exact quadratic-phase caches +against direct values at every original named coordinate in five fixtures. +The registered replay runs both normal and optimized warning-strict checks. +No predecessor executable or numerical certificate is replayed. + +## Scope and credit + +This contribution was produced by Nick Petalas. Apache-2.0. + +Ryanson Jonathan, `pinterbanget`, supplies the sequential table layout and +suffix-product cache model in [PR #4325](https://github.com/CrocSwap/integer-mult-bounds/pull/4325), +retained as [pr4100-chirp-odometer-tariff](../pr4100-chirp-odometer-tariff/README.md). +Cinna Davis supplies the underlying chirp construction in PR #4100 and +Douglas Colkitt the retained compact-control ancestry. Their results and +notices are unchanged. The predecessor's balanced-radix travel and rounding +results are cited premises. The new result is the exact closed table-walk +identity and sharp uniform bound after changing the fastest axis. + +The bound covers table-head movement only. Counter and cache actions, +arithmetic, setup, cleanup and allocation remain separately chargeable. +The phase stream is exact symbolic arithmetic; no rounded-word equality is +asserted. A physical consumer must accept the changed named-coordinate +order or pay for its conversion. No free transpose, encoded controller, +complete multiplier or discharge of the five selected assumptions is supplied. +Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +Can an actual chirp consumer use the largest-radix-fastest payload order +without an extra full transpose? Start by writing the complete input/output +layout and movement bill for one real caller. The missing physical producer +and consumer, rather than this table-movement estimate, are the blocker. +The structured question is in [TASK.json](TASK.json). diff --git a/research/chirp-radix-order/SOURCES.json b/research/chirp-radix-order/SOURCES.json new file mode 100644 index 0000000000..28f775ef6a --- /dev/null +++ b/research/chirp-radix-order/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/pr4100-chirp-odometer-tariff/README.md", + "usage": "input", + "git_blob": "c0f8b2a006965074c38484964d05f0a9cc1f3008", + "sha256": "6ed0793017d3c84003b0c7921c7b9598b868c48f05e46b8c0a88c52cfb843ff5" + } + ] +} diff --git a/research/chirp-radix-order/TASK.json b/research/chirp-radix-order/TASK.json new file mode 100644 index 0000000000..7c0fe189eb --- /dev/null +++ b/research/chirp-radix-order/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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": "Scoped all-size proof of the sharp table-tape movement bound Q <= 7TP for a largest-radix-first cached chirp enumerator, without a radix-ratio restriction; exact travel formula and independent finite counter.", + "scope_change_reason": "The selected card concerns the five selected-caller assumptions. This is a side result on a changed layout in the PR4325/PR4100 chirp interface, not admission of a selected assumption or an audit of the predecessor.", + "bottleneck_link": "Side result for precision_tape: arbitrary radix skew need not cause superlinear cached phase table movement when the caller supplies a largest-axis-fastest layout. Layout conversion and the other physical charges remain open.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified sharp uniform table-movement improvement; do not optimize further axis orders or extend to a complete supplier.", + "outcome": "completed", + "evidence": "PROOF.md proves the exact movement identity, uniform constant seven and sharp binary family. verify.py independently executes complete table walks and exact named-coordinate phase streams and emits a receipt bound to package file hashes.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an actual chirp consumer accept a largest-radix-fastest payload layout without an added full transpose?", + "why_it_matters": "The movement saving is useful only after the physical payload order is funded.", + "first_step": "Specify one original payload layout and its complete changed producer/consumer order, including all data movement.", + "blocked_by": "No physical layout conversion or consumer is supplied by this table-only theorem." + } + ] +} diff --git a/research/chirp-radix-order/VERIFY.json b/research/chirp-radix-order/VERIFY.json new file mode 100644 index 0000000000..6dea99147c --- /dev/null +++ b/research/chirp-radix-order/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/pr4100-chirp-odometer-tariff/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact closed travel identity against literal complete table walks; sharp binary family; named-coordinate quadratic chirps; rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same scientific checks with optimized Python and active runtime contracts." + } + ] +} diff --git a/research/chirp-radix-order/verify.py b/research/chirp-radix-order/verify.py new file mode 100644 index 0000000000..8370d2f0f6 --- /dev/null +++ b/research/chirp-radix-order/verify.py @@ -0,0 +1,220 @@ +#!/usr/bin/env python3 +"""Exact table movement for a largest-radix-first cached chirp stream. + +Produced by Nick Petalas. Apache-2.0. +""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from math import prod +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def domain(radices, width): + need(isinstance(radices, tuple) and 1 <= len(radices) <= 64, "axis count") + need(type(width) is int and 1 <= width <= 64, "word width") + for radix in radices: + need(type(radix) is int and 2 <= radix <= 65536, "radix range") + need(radix & (radix - 1) == 0, "dyadic radix") + need(prod(radices).bit_length() <= 1025, "arithmetic capacity") + + +def largest_first(radices): + domain(radices, 1) + pivot = max(range(len(radices)), key=radices.__getitem__) + return (pivot,) + tuple(k for k in range(len(radices)) if k != pivot) + + +def exact_travel(radices, width): + """Closed formula, including initialization and final return to cell zero.""" + domain(radices, width) + total = prod(radices) + movement = 2 * radices[0] + prefix = 1 + for k in range(len(radices) - 1): + prefix *= radices[k] + movement += 2 * (radices[k] + 1) * (total // prefix) + prefix = radices[0] + for j in range(1, len(radices)): + movement += (radices[j] - 1) * (total // prefix) + prefix *= radices[j] + return movement * width + + +def literal_travel(radices, width): + """Execute every table read, sweep, carry and final table-head return.""" + domain(radices, width) + total = prod(radices) + need(total <= 131072, "enumeration capacity") + offsets = [0] * len(radices) + for k in range(1, len(radices)): + offsets[k] = offsets[k - 1] + radices[k - 1] * width + digits = [0] * len(radices) + head = movement = 0 + # Initialization is the first record's complete reverse-axis table read. + for record in range(total): + changed = len(radices) - 1 + if record: + for k in range(len(radices)): + digits[k] += 1 + if digits[k] < radices[k]: + changed = k + break + digits[k] = 0 + for k in range(changed, -1, -1): + entry = offsets[k] + digits[k] * width + movement += abs(entry - head) + width + head = entry + width + need(head == radices[0] * width, "last read is the last axis-zero entry") + return movement + head + + +def check_bound(radices, width): + domain(radices, width) + need(radices[0] == max(radices), "a largest radix must be fastest") + movement = exact_travel(radices, width) + need(movement <= 7 * prod(radices) * width, "seven-volume movement bound") + return movement + + +def phase_stream(radices, order): + """Cache exact chirp exponents, with emitted coordinates in original axes.""" + domain(radices, 1) + axes = len(radices) + need(tuple(sorted(order)) == tuple(range(axes)), "axis permutation") + total = prod(radices) + need(total <= 4096, "phase enumeration capacity") + modulus = 2 * max(radices) + digits = [0] * axes + cache = [0] * axes + for record in range(total): + changed = axes - 1 + if record: + for k in range(axes): + axis = order[k] + digits[axis] += 1 + if digits[axis] < radices[axis]: + changed = k + break + digits[axis] = 0 + for k in range(changed, -1, -1): + axis = order[k] + entry = -(2 * axis + 1) * (modulus // (2 * radices[axis])) + cache[k] = (entry * digits[axis] ** 2 + + (cache[k + 1] if k + 1 < axes else 0)) % modulus + yield tuple(digits), cache[0] + + +def check_phases(): + cases = ((2, 8), (4, 2, 8), (2, 4, 2, 16), (8, 4, 2), (2,)) + records = 0 + for radices in cases: + modulus = 2 * max(radices) + expected = {} + for coordinate in product(*(range(t) for t in radices)): + expected[coordinate] = sum( + -(2 * k + 1) * (modulus // (2 * t)) * coordinate[k] ** 2 + for k, t in enumerate(radices)) % modulus + actual = {} + for coordinate, phase in phase_stream(radices, largest_first(radices)): + need(coordinate not in actual, "each named coordinate appears once") + actual[coordinate] = phase + need(actual == expected, "named-coordinate quadratic phase equality") + records += len(actual) + return len(cases), records + + +def rejects(call, message): + try: + call() + except ValueError: + return + raise ValueError("control accepted: " + message) + + +def check_controls(): + rejects(lambda: check_bound((2, 512), 1), "largest-radix premise") + rejects(lambda: literal_travel((65536, 4), 1), "enumeration cap") + rejects(lambda: exact_travel((3, 4), 1), "non-dyadic input") + rejects(lambda: exact_travel((), 1), "empty axes") + rejects(lambda: exact_travel((2,), 0), "zero width") + rejects(lambda: exact_travel((True,), 1), "Boolean radix") + rejects(lambda: list(phase_stream((2, 8), (0, 0))), "duplicate axis") + correct = literal_travel((512, 2), 1) + need(correct - 512 != exact_travel((512, 2), 1), "omitted return rejected") + need(correct - 1 != exact_travel((512, 2), 1), "missing move rejected") + # The same integer tuple cannot be interpreted in the old axis order. + rows = list(phase_stream((2, 8), (1, 0))) + need(rows[1][0] == (0, 1) and rows[1][0] != (1, 0), "layout control") + return 10 + + +def check_movements(): + cases = ordered = 0 + for axes in range(1, 6): + for radices in product((2, 4, 8), repeat=axes): + if prod(radices) > 8192: + continue + for width in (1, 3, 8): + need(literal_travel(radices, width) == exact_travel(radices, width), + "independent literal/formula movement equality") + cases += 1 + order = largest_first(radices) + arranged = tuple(radices[k] for k in order) + check_bound(arranged, 1) + ordered += 1 + for axes in range(1, 65): + radices = (2,) * axes + expected = 7 * 2 ** axes - 10 + need(exact_travel(radices, 1) == expected, "sharp binary family") + check_bound(radices, 1) + skew = [literal_travel(t, 1) for t in ((2, 512), (512, 2))] + need(skew == [264708, 3078], "complete skew-layout comparison") + return cases, ordered, skew + + +def authenticate(): + package = Path(__file__).resolve().parent + root = package.parents[1] + sources = json.loads((package / "SOURCES.json").read_text()) + inputs = [row for row in sources["files"] if row["usage"] == "input"] + need(len(inputs) == 1, "one attributed predecessor input") + row = inputs[0] + need(row["path"] == "research/pr4100-chirp-odometer-tariff/README.md", + "predecessor path") + need(sha256((root / row["path"]).read_bytes()).hexdigest() == row["sha256"], + "predecessor bytes") + return {name: sha256((package / name).read_bytes()).hexdigest() for name in + ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "verify.py")} + + +def main(): + hashes = authenticate() + cases, ordered, skew = check_movements() + phase_cases, records = check_phases() + controls = check_controls() + print(json.dumps({ + "status": "PASS_CHIRP_RADIX_ORDER", + "literal_movement_cases": cases, + "largest_first_layouts": ordered, + "sharp_binary_dimensions": 64, + "phase_cases": phase_cases, + "named_phase_records": records, + "controls": controls, + "skew_closed_table_moves_per_P": skew, + "skew_ratio_after": str(Fraction(skew[1], 1024)), + "uniform_table_constant_including_return": 7, + "package_sha256": hashes, + }, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()