From 48e312ff18d5b66b0969148f615fdf5ce0f92edd Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 10:07:34 +0000 Subject: [PATCH] feat(research): construct sharp four-axis reversible rounding --- .../four-axis-reversible-grid/ENGINEERING.md | 29 +++ .../four-axis-reversible-grid/ORIGIN.json | 9 + research/four-axis-reversible-grid/PROOF.md | 156 +++++++++++++++ research/four-axis-reversible-grid/README.md | 84 +++++++++ .../four-axis-reversible-grid/SOURCES.json | 24 +++ research/four-axis-reversible-grid/TASK.json | 114 +++++++++++ .../four-axis-reversible-grid/VERIFY.json | 32 ++++ .../four-axis-reversible-grid/construction.py | 115 +++++++++++ research/four-axis-reversible-grid/kernel.py | 49 +++++ research/four-axis-reversible-grid/verify.py | 178 ++++++++++++++++++ 10 files changed, 790 insertions(+) create mode 100644 research/four-axis-reversible-grid/ENGINEERING.md create mode 100644 research/four-axis-reversible-grid/ORIGIN.json create mode 100644 research/four-axis-reversible-grid/PROOF.md create mode 100644 research/four-axis-reversible-grid/README.md create mode 100644 research/four-axis-reversible-grid/SOURCES.json create mode 100644 research/four-axis-reversible-grid/TASK.json create mode 100644 research/four-axis-reversible-grid/VERIFY.json create mode 100644 research/four-axis-reversible-grid/construction.py create mode 100644 research/four-axis-reversible-grid/kernel.py create mode 100644 research/four-axis-reversible-grid/verify.py diff --git a/research/four-axis-reversible-grid/ENGINEERING.md b/research/four-axis-reversible-grid/ENGINEERING.md new file mode 100644 index 0000000000..961caddf4b --- /dev/null +++ b/research/four-axis-reversible-grid/ENGINEERING.md @@ -0,0 +1,29 @@ +# Verification boundaries + +The deliverable includes a deterministic constructor and a separate finite +predicate checker. Literal inverse, sum and native error checks exercise the +actual integer map. No predecessor replay or shared verification code is changed. + +All new functions are under 60 physical lines. No recursion or dynamic code +loading is used. The augmenting path uses at most 64 sources, 4,096 graph edges +and 64 backtracking steps. The candidate generator visits at most 65,536 offsets +per key; there are 64 keys. Each offset and payload has exactly sixteen real +coordinates. The semantic fixture count is fixed at 4,164, with two directions. +Every validator raises ValueError in ordinary and optimized Python. + +Power of Ten deviation, rules 3 and 9. Python allocates managed integers, +tuples, dictionaries and iterators, and the control harness uses ten bounded +callables. These language mechanisms prevent a literal allocation-free runtime +or a ban on all indirect calls. Bounds above fix all collection cardinalities; +public data have at most 4,096 bits per component. Tables are local arguments, +not a mutable global cache. The maximum live candidate set is one sixteen-value +offset and one graph with at most 4,096 offsets, not the candidate enumeration. +No files, network or subprocesses are opened by the mathematical kernel. +The verifier reads its own package files only for source-bound stdout receipts. +Follow-up is a fixed-capacity native implementation if physical costing is pursued. + +The packing format is checked rather than assumed: all offsets must fit signed +bytes, and the packed key/forward/inverse payload must be exactly 3,072 bytes. +Warning-strict normal and optimized execution are registered. The dense Walsh +reference is deliberately simple. Its ordinary arithmetic, table lookup, setup, +Boolean lowering, tape movement and cleanup are not assigned a physical tariff. diff --git a/research/four-axis-reversible-grid/ORIGIN.json b/research/four-axis-reversible-grid/ORIGIN.json new file mode 100644 index 0000000000..aa5023d1db --- /dev/null +++ b/research/four-axis-reversible-grid/ORIGIN.json @@ -0,0 +1,9 @@ +{ + "source_pr": 6536, + "head": "83fee59d692b0764d716e8356a7d991e4d503868", + "author": "aliromman", + "path": "research/three-axis-coset-rounding/README.md", + "sha256": "4c097c377e99fc9b490176dedb34a6cb24600c177c7236ccc6049105e2071096", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/83fee59d692b0764d716e8356a7d991e4d503868/research/three-axis-coset-rounding/README.md", + "usage": "Question and credited context only. No runtime dependency, copied predecessor code or claim of checking its theorem." +} diff --git a/research/four-axis-reversible-grid/PROOF.md b/research/four-axis-reversible-grid/PROOF.md new file mode 100644 index 0000000000..fc3baa1e27 --- /dev/null +++ b/research/four-axis-reversible-grid/PROOF.md @@ -0,0 +1,156 @@ +# A sharp four-axis reversible grid map + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Claim and sources + +Let `pi=1+i`, `C=[[i,1],[1,i]]`, and `U=pi^-4 C^(tensor 4)` on +sixteen Gaussian entries. These are the retained native Gaussian conventions, +as in David Ganz / Dugongue's [PR5815, C1-C3](https://github.com/CrocSwap/integer-mult-bounds/blob/f0fcda576df410dc15cd5b8183d4f74d284eba2b/research/gaussian-exceptional-correction/consumer-construction.md). +Ali Romman's [PR6536](https://github.com/CrocSwap/integer-mult-bounds/pull/6536) +asks whether four or more axes have a sum-preserving optimal grid map with an +explicit inverse and practical table. Its three-axis theorem is a cited +predecessor, not a verification target here. + +**Theorem.** There is an explicit bijection `F: Z[i]^16 -> Z[i]^16` fixing +zero and preserving the complex sum, such that both + +`||F(x)-Ux||_2 <= sqrt(8)` and `||F^-1(y)-U* y||_2 <= sqrt(8)`. + +No integer-output map can improve either uniform constant. Scaling every input +and output by a positive grid spacing h multiplies the error by h. The shared +real classification table, including both directions and keys, has a 3,072-byte +packed representation. This is a scoped proof with a finite construction +certificate, not a complete multiplication theorem, physical tariff or new kappa. + +## Reduction to two real Walsh maps + +Index coordinates by four-bit integers. Let `W_rs=(-1)^popcount(r&s)` and +`D_jj=(-i)^popcount(j)`. Then `W^2=16 I` and + +`U=-D W D/4`. + +Indeed, `pi^4=-4` and +`i^(4-popcount(r xor s))=D_rr W_rs D_ss`. +The one-axis matrix `C/pi` is unitary and has row sum one, so U is unitary +and preserves the complex sum. All phases and the leading minus sign are kept. + +We construct a bijection `R: Z^16 -> Z^16` approximating `W/4` and apply it +separately to real and imaginary components between these diagonal rotations. +For any integer vector z, put `q=Wz mod 4`, with residues in `{0,1,2,3}`. + +## The complete finite quotient + +Let v_s be column s of W. Modulo four, + +`v_s=v_0 + sum_(j:bit_j(s)=1) (v_(2^j)-v_0)`. + +This follows from `ab = a+b-1 mod 4` for signs a,b. Each difference has order +two and v_0 has order four. Therefore every q is represented by + +`a(t,b)=(t-sum b_j)e_0 + sum b_j e_(2^j)`, + +where `0<=t<4` and the four b_j are bits. The 64 keys are distinct: row zero +gives t and row `2^j` gives `t-2b_j mod 4`. This describes the whole quotient, +including all negative and arbitrarily large integer inputs. These elementary +Walsh/Smith quotient facts are prior algebra, not the new contribution. + +`construction.py` independently generates the column span modulo four. +`verify.py` generates the displayed 64 representatives and requires equality +of the two key sets. No enumeration of a large input box is used to infer coverage. + +## Finite correction certificate + +For each key q the certificate supplies an integer offset e(q) satisfying: + +1. `e(q)=-q mod 4`, component by component. +2. `||e(q)||_2^2 <= 64`. +3. `sum_j D_jj e(q)_j=0`. +4. `p(q)=W e(q)/4 mod 4` is a permutation of the 64 keys. +5. `e(0)=0`. + +The construction first lists a sufficient subset of corrections. For an odd +key, start with components -1 at residue 1 and +1 at residue 3; replace up to +six selected components by their negative triple. For an even key, choose +either sign of 2 at residue 2 and zero at residue zero. Keep zero weighted-sum +corrections and select the least squared norm on each reached quotient edge. +These are candidate subsets, not an exhaustive closest-vector search. + +A deterministic breadth-first augmenting-path matching chooses 64 edges. +The certificate checker checks conditions 1-5 directly, independently of the +matching search. It also checks the inverse offsets below, both weighted sums, +all table domains and the claimed norm bound. Thus correctness depends only +on the finite checked predicates, not on completeness or optimality of the +candidate search. The code uses no solver or pending Git object. + +The serialized rows, in lexicographic key order, consist of sixteen unsigned +key bytes, sixteen signed forward offset bytes and sixteen signed inverse +offset bytes. Both real components use the same table. The inverse offsets +are indexed by the same sorted key set; no permutation array is needed. +The verifier emits the payload hash and all package-file hashes to stdout. +It does not write or trust a prewritten receipt. + +## All-input inverse and error proof + +Define `R(z)=(Wz+e(q))/4`. Condition 1 makes it integral. Also `W e(q)` is +divisible by four: e(q) is congruent to `-Wz`, and `W^2 z=16z`. +For an output y, its key is + +`Wy mod 4 = W e(q)/4 mod 4 = p(q)`. + +Since p is a permutation, that key identifies q. Set + +`f(p(q))=-W e(q)/4`, and `R^-1(y)=(Wy+f(Wy mod 4))/4`. + +Substitution gives `R^-1(R(z))=z`. Conversely, this formula is integral on +every target class because `f(p)=-p mod 4`; substituting in the other order +gives every y back. This proves bijectivity on the entire integer lattice. +Since `W/4` is orthogonal, `||f(p(q))||=||e(q)||<=8`. +Both real forward and inverse errors are at most two. + +Let `R_C` apply R to both components. Define + +`F(x)=-D R_C(Dx)`, +`F^-1(y)=D^-1 R_C^-1(-D^-1 y)`. + +All rotations and R_C are bijections. The formula proves the literal inverse; +it does not assume an ideal square or fourth-power rewrite for F. +Two real squared errors at most four give total squared error at most eight, +in either direction. The zero offset fixes zero. + +The difference `F(x)-Ux` is `-D(e(q_real)+i e(q_imag))/4`. +Condition 3 makes its complex sum zero, so F preserves the exact sum. +Its bijective inverse then preserves that sum as well. + +## Sharpness and what improves + +Take `x=(2+2i,0,...,0)`. Every real and imaginary component of Ux is a +half-integer, because `Ux_j=-D_jj(1+i)/2`. Any Gaussian integer output has +squared error at least `32/4=8`. The same argument applies to U*. +This lower bound applies to every integer-output rule, including nonbijective +rules. The construction attains it while retaining the inverse and sum. + +This answers the four-axis part of PR6536's first open question. If an ambient +tensor has N entries and one group acts independently on sixteen-point blocks, +the aggregate error is at most `h sqrt(N/2)`. In particular, one four-axis group +has half the triangle-inequality bound obtained by two separately rounded groups +of sizes three and one. This comparison uses the predecessor's stated group +guarantees; it does not replay them or assert a complete caller implementation. +Phase covariance, exact fourth power, a physical speedup and optimal whole-call +error are not claimed. + +## Executed evidence and limits + +The verifier checks all 64 forward/inverse correction rows and all 4,096 pairs +of independent real quotient representatives. Another 64 signed fixtures, +three inputs with 128-, 1024- and 4090-bit components and the sharp witness give +4,164 endpoint fixtures. Each runs both directions, the literal inverse, exact +sum and an independently written direct native-matrix error oracle. Ten controls +reject missing or changed offsets and malformed or oversized inputs. + +The executable API caps components at 4,096 bits, keeping its allocation bounded. +For round trips, inputs with at most 4,090 bits leave ample output headroom. +The mathematical formula and written proof quantify over all Gaussian integers; +finite large-word cases do not establish that quantifier by themselves. +No inherited scientific result is audited. Independent human and formal +proof-kernel review are unclaimed. All five selected framework assumptions remain. diff --git a/research/four-axis-reversible-grid/README.md b/research/four-axis-reversible-grid/README.md new file mode 100644 index 0000000000..93fad26d02 --- /dev/null +++ b/research/four-axis-reversible-grid/README.md @@ -0,0 +1,84 @@ +# Sharp four-axis reversible Gaussian grid rounding + +This contribution was produced by Nick Petalas. Apache-2.0. + +A new sixteen-point integer-grid map has an explicit inverse, fixes zero and +preserves the exact complex sum. Its uniform Euclidean error is `sqrt(8) h` +for both the forward and adjoint ideal four-axis native Gaussian operators. +A half-grid witness proves that no integer-output rule can do better on this +block. Claim type: scoped written proof with a finite construction certificate. + +This answers the four-axis part of Ali Romman's +[PR6536 open question](https://github.com/CrocSwap/integer-mult-bounds/blob/83fee59d692b0764d716e8356a7d991e4d503868/research/three-axis-coset-rounding/README.md). +The new step is a sum-preserving matching on 64 real Walsh quotient classes, +reused for the real and imaginary parts. Keys and both correction directions +pack into 3,072 bytes. The table is constructed deterministically and certified +on every replay. + +For independent sixteen-point blocks in an N-entry tensor, the new group has +error at most `h sqrt(N/2)`. At four axes this halves the triangle-inequality +certificate of separately rounded groups of sizes three and one. This is an +error-bound improvement; the dense reference kernel has no claimed physical +cost advantage. No new kappa or selected-frontier change is supplied. + +## Proof and evidence + +[PROOF.md](PROOF.md) proves the all-input inverse, exact sum and sharp error +from the finite certificate. [construction.py](construction.py) builds the +matching; [kernel.py](kernel.py) executes the actual integer map. +[verify.py](verify.py) checks its predicates independently and emits a generated +receipt bound to every package file and the packed table hash. + +The replay checks 64 correction rows in both directions, all 4,096 real-class +pairs, another 68 signed/large-word/sharp fixtures and ten rejection controls. +Every one of the 4,164 fixtures runs both directions against a direct native +matrix oracle, including literal inversion and sum preservation. Maximum squared +error times sixteen is 128, exactly the sharp bound. Missing/altered offsets, +invalid component formats and the implementation's input-size limit are checked. + +From the repository root, CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/four-axis-reversible-grid/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/four-axis-reversible-grid/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/four-axis-reversible-grid +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/four-axis-reversible-grid --check-source-history +``` + +The absolute interpreter path is the publication environment; another CPython +3.12 executable works. Commands write only stdout. The package needs neither +pending Git objects nor network access. The code caps inputs at 4,096 bits per +component; the written algebraic proof covers all integers. Use 4,090-bit input +components to leave round-trip headroom within that executable cap. + +## Credit and boundaries + +Credit Ali Romman for PR6536's larger-block question and three-axis construction, +PR6534's two-axis construction and PR5821's Gaussian Smith execution. Credit +David Ganz / Dugongue for PR5815's Gaussian Smith construction. +Credit Brian / JoyboyBrian's PR5485 for the retained native rounded-call and +port context, PR4743's channel lineage, and the retained Gaussian native work +of David Ganz / Dugongue. Walsh transforms, finite quotient enumeration and +bipartite matching are classical. No predecessor result is replayed or audited. +The new result is the four-axis correction matching and its application. + +Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, +selected PR6030. Scope changes the uniform-transfer card from an actual-caller +assumption audit to a constructive local precision result. It discharges none +of the five selected assumptions. Independent human and formal proof-kernel +review are unclaimed. Phase covariance, exact fourth power, pointwise nearest +output, full-call optimality, Boolean/tape lowering, supplier admission and a +complete rounded multiplier remain unproved. [ENGINEERING.md](ENGINEERING.md) +records implementation bounds and managed-runtime deviations. + +## Open next questions + +1. Install the four-axis map in one literal native caller. First bind its + input/output charts, adjoint schedule, arbitrary dirty banks and full error + budget. Current local optimality does not prove caller admission. +2. Give a complete physical bill for the factored lookup. First lower the two + real transforms, residue classification and shared table to a reversible + Boolean/tape program with restored workspace. Table bytes do not price access. +3. Determine whether the same optimal error permits an exact fourth-power or + phase-covariance contract. First add those identities as finite quotient + constraints. The present matching certifies its explicit inverse only. diff --git a/research/four-axis-reversible-grid/SOURCES.json b/research/four-axis-reversible-grid/SOURCES.json new file mode 100644 index 0000000000..e64cd8bec5 --- /dev/null +++ b/research/four-axis-reversible-grid/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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/gaussian-exceptional-correction/consumer-construction.md", + "usage": "provenance", + "git_blob": "4a32aa48afd12bccd28165b4367ecb8c746accb6", + "sha256": "d88885b0a96996db56507af0062d652e9a10578b83e89d9bc757f7471483d13d" + } + ] +} diff --git a/research/four-axis-reversible-grid/TASK.json b/research/four-axis-reversible-grid/TASK.json new file mode 100644 index 0000000000..73fa33dc4b --- /dev/null +++ b/research/four-axis-reversible-grid/TASK.json @@ -0,0 +1,114 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "Construct an optimal-error four-axis Gaussian integer-grid bijection with an explicit inverse, exact sum and factored classification table.", + "scope_change_reason": "Take PR6536 first Open next question as a local constructive precision result rather than audit a selected framework assumption.", + "bottleneck_link": "A four-axis group halves the inherited three-plus-one triangle error certificate at four axes. Physical caller and tariff admission remain separate.", + "budget_minutes": 60, + "stop_rule": "Stop at the first finite correction matching proving the inverse, sum and sharp error; do not extend to larger groups or physical lowering.", + "outcome": "completed", + "evidence": "PROOF.md proves the all-integer theorem from 64 checked real correction rows. verify.py emits a file-bound receipt for 4164 two-direction endpoint fixtures, ten controls and 3072 packed table bytes.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can this block be installed in one literal native caller?", + "why_it_matters": "A local rounding guarantee is not caller admission.", + "first_step": "Bind entry/exit charts, adjoint schedule, dirty inputs and the complete error budget.", + "blocked_by": "No actual caller or inherited implementation obligation is discharged." + }, + { + "question": "What is the complete physical bill of the factored lookup?", + "why_it_matters": "Finite table size does not price runtime access and cleanup.", + "first_step": "Lower both real transforms, class lookup and inverse to a reversible Boolean/tape program.", + "blocked_by": "This dense indexed reference has no paid native tariff." + }, + { + "question": "Can optimal error coexist with exact fourth power or phase covariance?", + "why_it_matters": "Those identities could support additional caller rewrites.", + "first_step": "Impose the desired identities on the finite quotient matching.", + "blocked_by": "The present construction certifies its explicit inverse only." + } + ], + "claim_type": "scoped written proof and finite construction certificate", + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371090", + "source_pr": 6536, + "source_head": "83fee59d692b0764d716e8356a7d991e4d503868", + "source_author": "aliromman" + }, + "environment": { + "python": "3.12.15", + "platform": "macOS arm64", + "dependencies": "standard library only" + }, + "overlap": { + "open_pr_records": 521, + "discussion_records": 6526, + "sparse_local_notes": 120, + "omitted_local_notes": 8797, + "limits": "Open bodies and Discussions plus separate canonical main/merged object searches. No novelty guarantee for arbitrary diffs or unpublished work." + } +} diff --git a/research/four-axis-reversible-grid/VERIFY.json b/research/four-axis-reversible-grid/VERIFY.json new file mode 100644 index 0000000000..6b36a7b01e --- /dev/null +++ b/research/four-axis-reversible-grid/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Construct all correction rows; check finite matching predicates, complete real quotient-pair fixtures, native matrix error, inverse, sum and ten rejection controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete certificate and endpoint checks with Python assertions disabled." + } + ] +} diff --git a/research/four-axis-reversible-grid/construction.py b/research/four-axis-reversible-grid/construction.py new file mode 100644 index 0000000000..c80d588ef9 --- /dev/null +++ b/research/four-axis-reversible-grid/construction.py @@ -0,0 +1,115 @@ +"""A finite sum-preserving correction for the real Walsh-16 quotient. + +Produced by Nick Petalas. Apache-2.0. +""" +from itertools import combinations, product + +SIZE = 16 +WALSH = tuple(tuple(1 if (r & s).bit_count() % 2 == 0 else -1 + for s in range(SIZE)) for r in range(SIZE)) +WEIGHTS = (tuple((1, 0, -1, 0)[j.bit_count() % 4] for j in range(SIZE)), + tuple((0, -1, 0, 1)[j.bit_count() % 4] for j in range(SIZE))) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def walsh(values): + need(len(values) == SIZE, "Sixteen real coordinates") + return tuple(sum(a * b for a, b in zip(row, values)) for row in WALSH) + + +def quotient_keys(): + """Generate the entire column span modulo four, not sampled inputs.""" + keys = {(0,) * SIZE} + for column in zip(*WALSH): + keys = {tuple((a + t * b) % 4 for a, b in zip(key, column)) + for key in keys for t in range(4)} + need(len(keys) <= 64, "Walsh quotient capacity") + need(len(keys) == 64, "Complete Walsh quotient") + return tuple(sorted(keys)) + + +def corrections(key): + """A sufficient candidate subset; no exhaustive closest-vector claim.""" + base = tuple((0, -1, 2, 1)[a] for a in key) + if key[0] % 2: + for size in range(7): + for places in combinations(range(SIZE), size): + value = list(base) + for j in places: + value[j] = -3 * value[j] + yield tuple(value) + else: + half = tuple(j for j, value in enumerate(key) if value == 2) + for signs in product((-1, 1), repeat=len(half)): + value = list(base) + for j, sign in zip(half, signs): + value[j] = 2 * sign + yield tuple(value) + + +def correction_graph(keys): + indices = {key: j for j, key in enumerate(keys)} + graph = [] + for key in keys: + edges = {} + for value in corrections(key): + if any(sum(a * b for a, b in zip(weight, value)) for weight in WEIGHTS): + continue + image = walsh(value) + need(all(v % 4 == 0 for v in image), "Integral inverse offset") + target = indices[tuple((v // 4) % 4 for v in image)] + old = edges.get(target) + if old is None or sum(v * v for v in value) < sum(v * v for v in old): + edges[target] = value + graph.append(edges) + return tuple(graph) + + +def augment(source, graph, matched): + """Breadth-first augmenting path, at most 64 sources and 4096 edges.""" + queue = [source] + visited = {source} + parent = {} + for position in range(64): + if position == len(queue): + return False + current = queue[position] + for target in sorted(graph[current]): + if target in parent: + continue + parent[target] = current + previous = matched.get(target) + if previous is not None: + if previous not in visited: + visited.add(previous) + queue.append(previous) + continue + for _ in range(64): + current = parent[target] + old_target = next((t for t, s in matched.items() if s == current), None) + matched[target] = current + if old_target is None: + return True + target = old_target + raise ValueError("Augmenting path exceeds quotient capacity") + return False + + +def build_tables(): + keys = quotient_keys() + graph = correction_graph(keys) + matched = {} + for source in sorted(range(64), key=lambda s: (len(graph[s]), s)): + need(augment(source, graph, matched), "Complete correction matching") + need(len(matched) == 64 and len(set(matched.values())) == 64, + "Bijective quotient matching") + forward, backward = {}, {} + for target, source in sorted(matched.items()): + value = graph[source][target] + forward[keys[source]] = value + backward[keys[target]] = tuple(-v // 4 for v in walsh(value)) + return forward, backward diff --git a/research/four-axis-reversible-grid/kernel.py b/research/four-axis-reversible-grid/kernel.py new file mode 100644 index 0000000000..883c1c317d --- /dev/null +++ b/research/four-axis-reversible-grid/kernel.py @@ -0,0 +1,49 @@ +"""Indexed four-axis Gaussian grid map and its literal inverse. + +Produced by Nick Petalas. Apache-2.0. +""" +from construction import SIZE, need, walsh + +MAX_BITS = 4096 + + +def rotate(value, exponent): + a, b = value + return ((a, b), (-b, a), (-a, -b), (b, -a))[exponent % 4] + + +def validate(values): + need(type(values) in (tuple, list) and len(values) == SIZE, + "Sixteen Gaussian integer inputs") + need(all(type(z) in (tuple, list) and len(z) == 2 for z in values), + "Real/imaginary component pairs") + need(all(type(v) is int and v.bit_length() <= MAX_BITS + for z in values for v in z), "At most 4096 bits per component") + + +def real_map(values, table): + numerator = walsh(values) + key = tuple(v % 4 for v in numerator) + need(key in table, "Known Walsh quotient") + shifted = tuple(a + b for a, b in zip(numerator, table[key])) + need(all(v % 4 == 0 for v in shifted), "Exact quarter shifts") + return tuple(v // 4 for v in shifted) + + +def block(values, tables, inverse=False): + """Return a new block. Input and table values are never modified.""" + validate(values) + need(type(inverse) is bool, "Boolean inverse selector") + if inverse: + rotated = tuple(rotate((-a, -b), j.bit_count()) + for j, (a, b) in enumerate(values)) + else: + rotated = tuple(rotate(z, -j.bit_count()) for j, z in enumerate(values)) + table = tables[1 if inverse else 0] + real = real_map(tuple(z[0] for z in rotated), table) + imag = real_map(tuple(z[1] for z in rotated), table) + if inverse: + return tuple(rotate((a, b), j.bit_count()) + for j, (a, b) in enumerate(zip(real, imag))) + return tuple(rotate((-a, -b), -j.bit_count()) + for j, (a, b) in enumerate(zip(real, imag))) diff --git a/research/four-axis-reversible-grid/verify.py b/research/four-axis-reversible-grid/verify.py new file mode 100644 index 0000000000..c5057740a3 --- /dev/null +++ b/research/four-axis-reversible-grid/verify.py @@ -0,0 +1,178 @@ +"""Finite certificate and independent endpoint checks. Writes only stdout. + +Produced by Nick Petalas. Apache-2.0. +""" +import hashlib +import json +from itertools import product +from pathlib import Path +import struct +import sys + +from construction import build_tables, need +from kernel import block + +ROOT = Path(__file__).resolve().parent + + +def direct_walsh(values): + return tuple(sum((-1) ** ((j & k).bit_count()) * values[k] + for k in range(16)) for j in range(16)) + + +def representatives(): + result = {} + for t in range(4): + for bits in product((0, 1), repeat=4): + value = [0] * 16 + value[0] = t - sum(bits) + for j, bit in enumerate(bits): + value[1 << j] = bit + key = tuple(v % 4 for v in direct_walsh(value)) + need(key not in result, "Independent quotient representatives") + result[key] = tuple(value) + return result + + +def certify(tables): + forward, backward = tables + reps = representatives() + need(set(forward) == set(backward) == set(reps), "Complete table keys") + targets = set() + maximum = 0 + for key, value in sorted(forward.items()): + need(len(value) == 16 and all(type(v) is int for v in value), "Offset format") + need(all((a + b) % 4 == 0 for a, b in zip(key, value)), "Offset residues") + image = direct_walsh(value) + need(all(v % 4 == 0 for v in image), "Integral inverse offset") + target = tuple((v // 4) % 4 for v in image) + need(target not in targets, "Distinct quotient targets") + targets.add(target) + inverse = tuple(-v // 4 for v in image) + need(backward[target] == inverse, "Paired inverse offset") + for offset in (value, inverse): + norm = sum(v * v for v in offset) + need(norm <= 64, "Uniform real squared error at most four") + maximum = max(maximum, norm) + real = sum((1, 0, -1, 0)[j.bit_count() % 4] * v + for j, v in enumerate(offset)) + imag = sum((0, -1, 0, 1)[j.bit_count() % 4] * v + for j, v in enumerate(offset)) + need(real == imag == 0, "Preserved complex sum") + need(targets == set(reps), "Surjective quotient matching") + need(forward[(0,) * 16] == backward[(0,) * 16] == (0,) * 16, "Zero fixed") + need(maximum == 64, "Sharp real error attained") + return reps + + +def ideal_numerator(values, inverse=False): + """Four times C^tensor4 / (1+i)^4, directly from Hamming distance.""" + output = [] + phases = ((1, 0), (0, 1), (-1, 0), (0, -1)) + for r in range(16): + real = imag = 0 + for s, (a, b) in enumerate(values): + exponent = 4 - (r ^ s).bit_count() + c, d = phases[(-exponent if inverse else exponent) % 4] + real -= c * a - d * b + imag -= d * a + c * b + output.append((real, imag)) + return tuple(output) + + +def gaussian_sum(values): + return sum(z[0] for z in values), sum(z[1] for z in values) + + +def endpoint_case(values, tables): + original = tuple(values) + worst = 0 + for inverse in (False, True): + output = block(values, tables, inverse) + need(block(output, tables, not inverse) == original, "Literal inverse") + need(gaussian_sum(output) == gaussian_sum(values), "Endpoint sum") + numerator = ideal_numerator(values, inverse) + error = sum((4 * a - c) ** 2 + (4 * b - d) ** 2 + for (a, b), (c, d) in zip(output, numerator)) + need(error <= 128, "Sharp Gaussian squared error at most eight") + worst = max(worst, error) + need(tuple(values) == original, "Input preservation") + return worst + + +def endpoint_checks(reps, tables): + cases = 0 + worst = 0 + for real in reps.values(): + for imag in reps.values(): + values = tuple(zip(real, imag)) + worst = max(worst, endpoint_case(values, tables)) + cases += 1 + for number in range(64): + values = tuple((((j + 1) * (number + 3) << (number % 31)) - 17, + (j - 7) * (number + 1) * (-1) ** j) for j in range(16)) + worst = max(worst, endpoint_case(values, tables)) + cases += 1 + for bits in (128, 1024, 4090): + values = tuple(((-1) ** j * ((1 << bits) + j), + (-1) ** (j // 2) * ((1 << bits) - j)) for j in range(16)) + worst = max(worst, endpoint_case(values, tables)) + cases += 1 + witness = ((2, 2),) + ((0, 0),) * 15 + need(all(a % 4 == b % 4 == 2 for a, b in ideal_numerator(witness)), + "Every real component is half integral at the lower-bound witness") + need(endpoint_case(witness, tables) == 128, "Sharp Gaussian error attained") + return cases + 1, worst + + +def rejection_controls(tables): + controls = [] + key = (0,) * 16 + missing = (dict(tables[0]), dict(tables[1])) + del missing[0][key] + controls.append(lambda: certify(missing)) + for coordinate, delta in ((0, 1), (0, 4), (3, 12)): + changed = (dict(tables[0]), dict(tables[1])) + value = list(changed[0][key]) + value[coordinate] += delta + changed[0][key] = tuple(value) + controls.append(lambda changed=changed: certify(changed)) + changed = (dict(tables[0]), dict(tables[1])) + changed[1][key] = (4,) + (0,) * 15 + controls.append(lambda: certify(changed)) + for invalid in ((), ((0, 0),) * 15, ((0, 0, 0),) * 16, + ((True, 0),) * 16, ((1 << 4096, 0),) * 16): + controls.append(lambda invalid=invalid: block(invalid, tables)) + for check in controls: + try: + check() + except ValueError: + continue + raise ValueError("A malformed certificate or input was accepted") + return len(controls) + + +def main(): + need(len(sys.argv) == 1, "No verifier arguments") + tables = build_tables() + reps = certify(tables) + cases, worst = endpoint_checks(reps, tables) + controls = rejection_controls(tables) + payload = b"".join(struct.pack("16B32b", *key, *tables[0][key], *tables[1][key]) + for key in sorted(reps)) + need(len(payload) == 3072, "Shared real table payload") + receipt = { + "status": "PASS_FOUR_AXIS_REVERSIBLE_GRID", + "claim_type": "scoped written proof and finite construction certificate", + "real_classes": len(reps), "gaussian_class_pairs": len(reps) ** 2, + "table_payload_bytes": len(payload), "table_sha256": hashlib.sha256(payload).hexdigest(), + "endpoint_fixtures": cases, "directions_per_fixture": 2, + "maximum_squared_error_times_16": worst, "rejection_controls": controls, + "files_sha256": {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(ROOT.iterdir()) if p.is_file()}, + } + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()