From 6112144851cc13fdd7183d4e909c6dcc841ea8e1 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 30 Oct 2026 11:33:24 +0000 Subject: [PATCH] feat(research): prove linear drift in a rounded native loop --- research/native-loop-linear-drift/PROOF.md | 193 ++++++++++ research/native-loop-linear-drift/README.md | 110 ++++++ .../native-loop-linear-drift/SOURCES.json | 48 +++ research/native-loop-linear-drift/TASK.json | 101 ++++++ .../native-loop-linear-drift/VALIDATION.md | 84 +++++ research/native-loop-linear-drift/VERIFY.json | 36 ++ research/native-loop-linear-drift/verify.py | 336 ++++++++++++++++++ 7 files changed, 908 insertions(+) create mode 100644 research/native-loop-linear-drift/PROOF.md create mode 100644 research/native-loop-linear-drift/README.md create mode 100644 research/native-loop-linear-drift/SOURCES.json create mode 100644 research/native-loop-linear-drift/TASK.json create mode 100644 research/native-loop-linear-drift/VALIDATION.md create mode 100644 research/native-loop-linear-drift/VERIFY.json create mode 100644 research/native-loop-linear-drift/verify.py diff --git a/research/native-loop-linear-drift/PROOF.md b/research/native-loop-linear-drift/PROOF.md new file mode 100644 index 0000000000..7d95914d30 --- /dev/null +++ b/research/native-loop-linear-drift/PROOF.md @@ -0,0 +1,193 @@ +# A drift orbit and its correction-state consequence + +This contribution is produced by Nick Petalas. New work is Apache-2.0. + +## Fixed maps and inherited facts + +Use precisely PR5492's four signed rank-one recipes. In their stored order, +the edges are `0→29`, `0→2`, `2→341`, `29→341`. One cycle applies the first +backwards, the second and third forwards, and the fourth backwards. Denote +this rounded map by C. PR5492 already identifies the cycle as an ideal +Gaussian-rational identity and proves that its independently rounded edges +need not be flat. Those facts and its original witness are inherited. + +For Gaussian integers a,b, define L_epsilon by + +```text +D = a-b +S = b + floor(D/2) +E = epsilon*i*D +B = S - floor(E/2) +A = B+E +L_epsilon(a,b) = (A,B), epsilon in {+1,-1}. +``` + +Floors act separately on the real and imaginary components. This is the +retained pair convention, with epsilon=-1 for an inverse edge. Signed affine +wrappers are exact coordinate permutations and powers of i. The verifier +imports no predecessor executable. + +## A four-coordinate invariant circuit + +Let V be the Gaussian-integer sublattice supported on coordinates +`(1,10,39,44)`. Write its entries as `(a,b,c,d)`. The source recipes restrict +to the following four stages. In each row both pair operations read the +same incoming vector, and their output assignments occur simultaneously. + +| Stage | First pair and assignments | Second pair and assignments | +|---|---|---| +| 0 | `(A,B)=L_-(a,-c)`; `c'=iA, a'=-iB` | `(P,Q)=L_-(b,-d)`; `b'=P, d'=-Q` | +| 1 | `(A,B)=L_+(a,-b)`; `a'=A, b'=-B` | `(P,Q)=L_+(-id,ic)`; `c'=P, d'=-Q` | +| 2 | `(A,B)=L_+(-ic,ia)`; `a'=A, c'=-B` | `(P,Q)=L_+(b,-d)`; `b'=P, d'=-Q` | +| 3 | `(A,B)=L_-(a,-b)`; `a'=A, b'=-B` | `(P,Q)=L_-(c,-d)`; `d'=iP, c'=-iQ` | + +The complete wrapper plans verify this restriction exactly. Every active +kernel input is paired with another active input, every output returns to +V, and the complementary zero pairs stay zero. Consequently C maps V to V. +The circuit is also recorded as eight pairs of integer/phase tuples in +`verify.py:CIRCUIT`. `derive_circuit` reconstructs every tuple from the +byte-authenticated source recipes; it does not infer support from probes. + +## Integral-shift lemma + +Suppose a pair is shifted by `(u,v)` with both components of `u-v` even. +Then for every Gaussian-integer a,b, + +```text +L_epsilon(a+u,b+v) = L_epsilon(a,b) + U_epsilon(u,v), +``` + +where U_epsilon is the ideal linear pair obtained by replacing each floor +with exact division by two. Indeed +`floor((z+2m)/2)=floor(z/2)+m` componentwise, and multiplication by +`epsilon*i` preserves evenness. Substitute this equality into D,S,E,B,A. +The shift term is independent of a,b. The same proof works for every +integer multiple of `(u,v)`, including negative multiples. Exact monomial +wrappers transport the shift linearly. + +Define + +```text +x = (3+2i, 1, 3i, 3+i) +delta = (-4+4i, 4+4i, 4+4i, 4-4i). +``` + +Transporting delta through the four ideal stages gives this exact certificate. + +| Cut | Shift on `(a,b,c,d)` | +|---|---| +| Entry | `(-4+4i, 4+4i, 4+4i, 4-4i)` | +| After 0 | `(8i, 0, 0, -8i)` | +| After 1 | `(-4+4i, -4-4i, -4-4i, 4-4i)` | +| After 2 | `(-8, 0, 0, 8)` | +| After 3 | `(-4+4i, 4+4i, 4+4i, 4-4i)` | + +Every incoming shifted pair difference is even. The verifier checks all +eight differences before division, using the displayed circuit. Hence the +lemma proves, for every v in V and every integer k, + +```text +C(v+k*delta) = C(v)+k*delta. (1) +``` + +This universal statement follows from parity and the floor identity. The +128 random fixtures only corroborate it. + +## Finite orbit certificate + +Executing the fixed circuit 24 times on x gives + +```text +C^24(x) = (-1+6i, 5+4i, 4+7i, 7-3i) = x+delta. (2) +``` + +The verifier enumerates all 25 cycle boundaries and all 96 internal edge +boundaries. Every internal boundary agrees with a second interpreter on +all 512 coordinates. That interpreter separately decodes each signed affine +wrapper using explicit bit sums and uses these component formulas for L_+. +For `D=(r,s)` and `b=(p,q)`, + +```text +A = (p+floor(r/2)-floor(s/2), q+floor(s/2)+ceil(r/2)) +B = (p+floor(r/2)+ceil(s/2), q+floor(s/2)-floor(r/2)). +``` + +L_- exchanges A and B. These follow directly from the pair definition, +using `ceil(t/2)=t-floor(t/2)`. The finite domain `[-3,3]^4` corroborates the +formula and exact pair inverse on all 2,401 Gaussian input pairs. The full +orbit and the hash of its 96 cuts are printed in the generated receipt. +Equation (2) is a finite exact computation, not a universal theorem inferred +from samples. + +Combining (1) and (2) by induction proves + +```text +C^(24k)(x) = x+k*delta, k >= 0. (3) +``` + +More generally, if `0<=r<24`, then +`C^(24k+r)(x)=C^r(x)+k*delta`. The bounded replay checks 769 consecutive +instances of this formula. Since delta is nonzero, (3) proves infinite +order and unbounded defect relative to the ideal identity. Its squared +Euclidean norm is `8*4^2=128`, so the defect is `8 sqrt(2) k` after `24k` +traversals. No minimal drift period is asserted. + +For every integer g>=0, execute the same integer-coordinate convention on +`h Z[i]^512`, h=2^-g. Scaling (3) gives exactly +`C_h^(24k)(h x)=h x+k h delta`. Therefore no finite absolute defect envelope +independent of path length exists at any fixed grid. This does not preclude +a path-length-dependent error budget or a changing grid. + +## Exact correction requires growing side information + +Fix K>=0. Suppose a correction service receives only an unchanged rounded +payload y and a tag s in a finite set S. Its deterministic decoder D must +recover every original v in V after each permitted length `0,24,...,24K`. +Tag generation may depend arbitrarily on v and the path. The decoder has no +separate path length, saved original or other path-dependent input. + +For each k in `0,...,K`, choose `v_k=x-k*delta` and use path length 24k. +Equations (1) and (3) give + +```text +C^(24k)(v_k) = C^(24k)(x-k*delta) = x. +``` + +All final payloads are identical. The originals v_k are pairwise distinct +because delta is nonzero and Gaussian-integer addition is torsion-free. +Their tags must therefore be pairwise distinct: otherwise the same decoder +input `(x,s)` would have two different required outputs. Thus `|S|>=K+1`. +A b-bit fixed-width tag has at most `2^b` states, giving +`b>=ceil(log2(K+1))`. There is no fixed finite tag alphabet that works for +all K under this contract. The checker executes the collision family for +K=32, with 33 distinct original vectors and one common final payload. + +The all-input premise matters. The collision originals have increasing +magnitude, so this argument does not give a uniform-in-K lower bound on a +fixed bounded source box. Giving the decoder a path counter, the original +input or a modified payload changes the information contract. Reversing a +known complete path remains exactly possible and is not contradicted. + +## Diagnostic bill and remaining obligations + +One traversal consists of exactly four rank-one native edges. The finite +24-traversal certificate therefore uses 96 native edges and 192 signed +wrappers. Its reduced circuit uses 192 active Gaussian pairs; the independent +full-bank interpreter executes 24,576 pairs and decodes all 98,304 wrapper +entries. These are diagnostic verification operations, not recursive costs +claimed for a production supplier. The 24,576 pairs exclude the separate +covariance, oracle and control computations. They are not a whole-verifier +operation count. + +The scalar reference uses ordinary unbounded integers, floor division, +monomial preparation and array accesses. Physical tape movement, ownership, +precision overflow, setup/cleanup and recursive child costs are not supplied +by this checker and are not assigned zero. Receipt hashes authenticate +finite inputs and outputs; they are not human or proof-kernel review. + +PR5492's cycle joins occurrences on different fields, so no repeated +chronological supplier segment is constructed. The result is an obstruction +to path-independent exact rounded frame service and to a path-length-free +absolute error envelope for the specified edges. It does not refute the +conditional selected supplier, arbitrary rounding policies or integer +multiplication. All five selected framework assumptions remain explicit. diff --git a/research/native-loop-linear-drift/README.md b/research/native-loop-linear-drift/README.md new file mode 100644 index 0000000000..ef689a57f0 --- /dev/null +++ b/research/native-loop-linear-drift/README.md @@ -0,0 +1,110 @@ +# Linear drift in a repeated rounded native cycle + +This contribution is produced by Nick Petalas. + +For the unchanged fixed-grid native cycle `29→0→2→341→29` of +[JoyboyBrian's PR5492](https://github.com/CrocSwap/integer-mult-bounds/pull/5492), +let C be one rounded traversal. On coordinates `(1,10,39,44)`, take + +```text +x = (3+2i, 1, 3i, 3+i) +d = (-4+4i, 4+4i, 4+4i, 4-4i). +``` + +All other 508 coordinates are zero. The new exact identity is + +```text +C^(24k)(x) = x + k d, k >= 0. +``` + +Thus this rounded identity cycle has infinite order and Euclidean defect +`8 sqrt(2) k` after `24k` traversals. At grid spacing `h=2^-g`, the same +witness has defect `8 sqrt(2) k h`. A fixed grid therefore admits no absolute +error bound independent of the number of traversals. + +A second consequence concerns exact correction. If the unchanged rounded +payload and a tag are the decoder's only inputs, correction for every signed +integer input and paths of length `0,24,...,24K` needs at least `K+1` tag +states, hence at least `ceil(log2(K+1))` bits in a fixed-width tag. The proof +allows an arbitrary deterministic decoder, not only additive corrections. +Supplying the path length separately supplies additional side information. +A fixed bounded input domain is outside this storage lower bound. + +This is a **scoped proof with an exact finite certificate**. The universal +iteration statement follows from a proved integral-shift covariance lemma +and a checked 24-step orbit, rather than extrapolation from a long run. +[PROOF.md](PROOF.md) gives the circuit, shift certificate and decoder argument. +It also states the diagnostic's complete claim boundary. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/native-loop-linear-drift/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/native-loop-linear-drift/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/native-loop-linear-drift +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/native-loop-linear-drift --check-source-history +``` + +The direct verifier prints generated JSON with status +`PASS_NATIVE_LOOP_LINEAR_DRIFT`. Its normal and optimized modes check the +same finite domain: + +- All 96 edges of the new orbit with two implementations, one on four + coordinates and one on the full 512-coordinate bank. +- Eight exact even-difference tests establishing the shift certificate, + plus 128 signed covariance fixtures, including 80-bit inputs. +- 2,401 complete small pair inputs against a separate component formula + and exact inverse, 769 consecutive iterate formulas, and 33 distinct + originals producing one identical final payload. +- Four rejecting controls and two positive controls, including a periodic + input. The theorem asserts existence of drift, not drift on every input. + +No predecessor executable or scientific receipt is replayed. The unchanged +recipe data are authenticated before use. Optional `--receipt /absolute/path` +writes a new hash-bound receipt outside the checkout and refuses overwrite; +`--check-receipt /absolute/path` recomputes it. No receipt is handwritten or +committed. [VALIDATION.md](VALIDATION.md) records local execution and limits. +The direct commands also work in the official Git-free package export. + +## Scope and credit + +PR5492 supplies the actual signed native recipes, ideal identity loop, +one-traversal defect and source binding. The new contribution is the drift +orbit, integral-shift certificate, infinite-order proof and correction-state +lower bound. Credit JoyboyBrian; Tekalign's P104 reversible lifting; +Cao Yifan's round-three word; ywz65's native adapters; the coherent-frame +additivity work; and the retained P104/native/controller/geometry lineage. +Sricharan Vagvala's PR1631 supplies a related orbit-based rounding obstruction +for a different shear-equivariance contract, and Sagar Thakrar's PR1537 +constructs exact paid infinite-order returns. Neither studies this rounded +identity cycle. Reversible lifting, floor translation and the pigeonhole +principle are classical. No literature-priority claim is made. + +The cycle joins occurrences on different supplier roles. It is a frame +consistency diagnostic, not a chronological supplier subword. Width one +already establishes this scoped obstruction; other tensor widths, every +initial input, dynamic grids and changed edge maps are unclaimed. Every +finite reverse word still restores its input exactly. + +The result supplies no paid replacement, full physical implementation, +new kappa or selected-frontier change. Native pricing, owned erasure, +compiler closure, complete precision/tape and analytic recovery remain +open. Source pins are in [SOURCES.json](SOURCES.json); the current source-binding +orientation passed for selected PR6030 at canonical main +`2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority revision 8. Independent +human and formal proof-kernel review are unclaimed. New work is Apache-2.0. + +## Open next questions + +1. Bind an equivalent drift segment to an actual chronological caller with + its full entry and restored exit. Start from one named caller; no such + embedding is supplied by this diagnostic. +2. Specify a changed rounded-edge ABI that removes the drift, with an explicit + storage, erasure and scalar-ADD contract. Price the complete physical and + recursive bill before claiming a supplier improvement. + +The structured questions and blockers are in [TASK.json](TASK.json). Research +stops at this first verified result. Minimal drift periods and other cycles +were not investigated. diff --git a/research/native-loop-linear-drift/SOURCES.json b/research/native-loop-linear-drift/SOURCES.json new file mode 100644 index 0000000000..dc3ecba9cf --- /dev/null +++ b/research/native-loop-linear-drift/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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-rounded-loop-defect/RECIPES.json", + "usage": "input", + "git_blob": "ec453b2741a28a472689ab640ac9e3c325b97304", + "sha256": "97f769fe20aada89d065f538af137f6385d4fbcdb21e0832dd850429f679b8b2" + }, + { + "path": "research/native-rounded-loop-defect/README.md", + "usage": "provenance", + "git_blob": "1f5c8849d44af1fbd1e2248cfcf7d9ea52af6824", + "sha256": "71de2059290b95a8c9c0521396d26c4ea8e082ddc7d2abb90c1bc83ce228a5fc" + }, + { + "path": "research/native-rounded-loop-defect/PROOF.md", + "usage": "provenance", + "git_blob": "51a633ae554dfce0da4a83900d4537d3a67e843e", + "sha256": "44e1e608b3e5befdf4f037b93f9296e3ce0a44e66622ecd377f1a7317a1e430f" + }, + { + "path": "research/p104-reversible-lifting/README.md", + "usage": "provenance", + "git_blob": "05eddb238528e00e0985a2cdb2e04e7595cbbb51", + "sha256": "051a886e9777b6ace444920df1fd46c285dc0251d7ef6fac570dc12cca7c4bc8" + }, + { + "path": "research/coherent-frame-additivity/README.md", + "usage": "provenance", + "git_blob": "5c72c03ba7887aedad30acf4c20f40346da2fee5", + "sha256": "cf6889e806a9b4fa9a75beccefaa998627a9b35b77be529f0fe26718f60b9d67" + } + ] +} diff --git a/research/native-loop-linear-drift/TASK.json b/research/native-loop-linear-drift/TASK.json new file mode 100644 index 0000000000..70bdbef357 --- /dev/null +++ b/research/native-loop-linear-drift/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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": "Prove linear iterated drift and a correction-state lower bound for the fixed-grid width-one native cycle of PR5492.", + "scope_change_reason": "The assignment requests original research rather than an audit. This new dynamics theorem builds on PR5492 instead of rechecking its one-traversal result.", + "bottleneck_link": "A proposed rounded native frame-potential service needs path-independent output or a funded correction interface. Unbounded drift rules out a path-length-independent absolute error envelope for these unchanged edges.", + "budget_minutes": 60, + "stop_rule": "Package the first verified original orbit/covariance result; do not broaden into other cycles, minimal periods or a complete supplier.", + "outcome": "negative-result", + "evidence": "PROOF.md; source-authenticated verify.py with independent full-bank interpreter; generated hash-bound receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an actual chronological caller reach and repeat an equivalent drift segment under its owned-field and frame contracts?", + "why_it_matters": "The present cycle is a consistency diagnostic, not a consecutive supplier subword.", + "first_step": "Select a named caller and exhibit its complete entry, repeated segment and restored exit before pricing it.", + "blocked_by": "No chronological embedding or complete paid caller is constructed here." + }, + { + "question": "Can a changed rounded-edge ABI remove this drift while preserving reversibility and the scalar ADD contract at a favorable complete cost?", + "why_it_matters": "The theorem fixes the old edge maps and does not exclude a coherent changed implementation.", + "first_step": "Specify where path information is stored and how it is erased, including path length if supplied externally.", + "blocked_by": "A physical implementation, numerical budget, ownership proof and full signed invoice are missing." + } + ], + "claim_type": "scoped proof with exact finite certificate", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19291984", + "source_question": { + "pr": 5492, + "author": "JoyboyBrian", + "head": "09f88edea964b16ffe8569be156f4efce066fa56" + }, + "upstream_refresh": { + "commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "priority_revision": 8, + "checked_utc": "2026-10-30T11:24:00Z" + } +} diff --git a/research/native-loop-linear-drift/VALIDATION.md b/research/native-loop-linear-drift/VALIDATION.md new file mode 100644 index 0000000000..8744e95e6a --- /dev/null +++ b/research/native-loop-linear-drift/VALIDATION.md @@ -0,0 +1,84 @@ +# Validation boundary and implementation constraints + +This contribution is produced by Nick Petalas. + +The direct normal and optimized checks passed on the required CPython 3.12 +interpreter. Both produced identical generated receipts. No hosted pass is +currently claimed. + +## Exact coverage + +`verify.py` authenticates PR5492's unchanged recipe JSON before decoding it. +It derives the four-coordinate circuit from all eight 512-coordinate signed +wrappers, checks the new 96-edge orbit against a second full-bank decoder, +and tests all eight shift-pair parity premises. The written proof turns +these finite facts into the universal iterate and correction-state results. +No predecessor verifier or receipt is imported or executed. + +The receipt includes each package file's SHA256, the exact source hash, +all 25 cycle-boundary vectors, the shift cuts and the hash of all 96 edge +cuts. It is generated on demand, and is never handwritten. Its normal and +optimized bytes must agree. Finite checks do not establish mathematical +literature priority, human acceptance or proof-assistant acceptance. + +## Engineering inspection + +Playbook: investigation. The original assignment also authorizes adding a +new scoped package. Build the Lever led to the standalone, deterministic +certificate checker; Prove It Works led to full-bank comparison at every +new orbit edge and direct Git-free replay. Unslop applies to the prose. + +The checker has no recursion, network, subprocess, dynamic code loading or +third-party dependency. All science loops have explicit fixed bounds: +512 addresses, nine bits, 24 traversals, four stages, 256 pairs per ambient +edge, 128 covariance fixtures, 2,401 pair inputs, 769 consecutive iterates, +and 33 collision paths of at most 768 traversals each. Source files are +limited to 64 KiB, package hashing to 16 files of at most 1 MiB each, and +receipt reads to 1 MiB. Each function is below 60 physical lines. Schema +and range checks occur before source-controlled loops. Explicit exceptions +keep acceptance active under `-O`. The source is read-only; the only optional +write creates a new receipt outside the checkout and checks the byte count. + +Power of Ten rule 3 deviation: CPython allocates integers, tuples, lists and +JSON data during the bounded check. The fixed dimensions and iteration +limits bound live mathematical storage. The largest primary state is the +512-coordinate bank; only 96 four-coordinate cuts and 25 orbit boundaries +are retained. The loaded JSON and eight 512-entry plans are fixed-size +setup data. Python allocator internals are not a byte-exact heap bound. +Replacing managed allocation would require a separate runtime and becomes +a follow-up only if this checker becomes a reusable unbounded service. + +Power of Ten rule 10 boundary: warning-strict normal and optimized Python +runs are registered. No separate static analyzer is configured for this +isolated standard-library package. AST inspection checks function lengths +and syntax without generating bytecode. No repository-wide tooling change +is part of the scientific result. + +The exact proof, code and diff received local self-review. Independent human +and formal proof-kernel review remain unclaimed. + +## Local and hosted checks + +Both exact registered commands were also timed individually on local +CPython 3.12. Normal execution completed in 0.741 seconds and optimized +execution in 0.747 seconds, each with return code zero and identical output. +These single observations check the replay deadline; no speedup or portable +timing guarantee is claimed. The enclosing registered replay reported +`PASS_REGISTERED_RESEARCH_PACKAGE` with outcome `negative-result`. + +AST inspection passed for all 21 functions, with a maximum of 31 physical +lines, and whitespace checks passed. Publication-byte/source-history and +official export checks run against the publication commit and are reported +in the PR body. The direct exported verifier needs only this package and its +one declared recipe input; no Git executable is required. + +The selected baseline orientation reported +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY` for selected PR6030 at canonical main +`2485805a6d47f36ea83ddde6327d453ac82d44dc`. This authenticates bindings and +metadata; it is not a selected science replay. The final upstream refresh +retained that main commit and unchanged relevant guidance, selected record +and recipe inputs. + +Full selected supplier replay, other tensor widths, chronological caller +embedding, physical tape realization, dynamic-grid error analysis, Lean, +Docker, all-size multiplication and hosted CI are unrun here. diff --git a/research/native-loop-linear-drift/VERIFY.json b/research/native-loop-linear-drift/VERIFY.json new file mode 100644 index 0000000000..1053a902df --- /dev/null +++ b/research/native-loop-linear-drift/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/native-rounded-loop-defect/RECIPES.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact 24-traversal orbit, independent 512-coordinate interpreter, integral shift covariance, all-iteration corroboration, correction-state collision family and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same exact checks with Python assertions disabled; acceptance uses explicit exceptions." + } + ] +} diff --git a/research/native-loop-linear-drift/verify.py b/research/native-loop-linear-drift/verify.py new file mode 100644 index 0000000000..9a2bede580 --- /dev/null +++ b/research/native-loop-linear-drift/verify.py @@ -0,0 +1,336 @@ +"""Exact iterated native-loop drift certificate, produced by Nick Petalas. + +Apache-2.0. The signed recipes are JoyboyBrian / PR5492's unchanged input. +No predecessor executable is imported or run. +""" + +import argparse +from hashlib import sha256 +import json +from pathlib import Path +import random + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +SOURCE = "research/native-rounded-loop-defect/RECIPES.json" +SOURCE_HASH = "97f769fe20aada89d065f538af137f6385d4fbcdb21e0832dd850429f679b8b2" +SUPPORT = (1, 10, 39, 44) +START = ((3, 2), (1, 0), (0, 3), (3, 1)) +DRIFT = ((-4, 4), (4, 4), (4, 4), (4, -4)) +STEPS = ((0, True), (1, False), (2, False), (3, True)) +# Each pair lists (input index, input phase, output index, output phase). +# Indices here refer to SUPPORT, not the 512-coordinate ambient bank. +CIRCUIT = ( + (((0, 0, 2, 1), (2, 2, 0, 3)), ((1, 0, 1, 0), (3, 2, 3, 2))), + (((0, 0, 0, 0), (1, 2, 1, 2)), ((3, 3, 2, 0), (2, 1, 3, 2))), + (((2, 3, 0, 0), (0, 1, 2, 2)), ((1, 0, 1, 0), (3, 2, 3, 2))), + (((0, 0, 0, 0), (1, 2, 1, 2)), ((2, 0, 3, 1), (3, 2, 2, 3))), +) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def rotate(value, phase): + real, imag = value + return ((real, imag), (-imag, real), (-real, -imag), (imag, -real))[phase % 4] + + +def lifting_pair(a, b, inverse=False, require_even=False): + difference = (a[0] - b[0], a[1] - b[1]) + if require_even: + need(all(x % 2 == 0 for x in difference), "shift difference must be even") + middle = (b[0] + difference[0] // 2, b[1] + difference[1] // 2) + turned = rotate(difference, -1 if inverse else 1) + second = (middle[0] - turned[0] // 2, middle[1] - turned[1] // 2) + return (second[0] + turned[0], second[1] + turned[1]), second + + +def compile_wrapper(record): + expected = {"matrix_rows", "offset", "linear_Z4", "quadratic_rows", "phase"} + need(type(record) is dict and set(record) == expected, "wrapper schema") + rows, linear, quadratic = (record[k] for k in + ("matrix_rows", "linear_Z4", "quadratic_rows")) + need(all(type(v) is list and len(v) == 9 for v in (rows, linear, quadratic)), + "wrapper dimension") + need(all(type(x) is int and 0 <= x < 512 for x in rows + quadratic), "binary row") + need(all(type(x) is int and 0 <= x < 4 for x in linear), "linear phase") + need(type(record["offset"]) is int and 0 <= record["offset"] < 512, "offset") + need(type(record["phase"]) is int and 0 <= record["phase"] < 4, "global phase") + result = [] + for x in range(512): + y = record["offset"] + for j, row in enumerate(rows): + y ^= ((row & x).bit_count() % 2) << j + phase = record["phase"] + sum(((x >> j) & 1) * linear[j] for j in range(9)) + phase += 2 * sum(((x >> j) & 1) * ((x >> k) & 1) * ((quadratic[j] >> k) & 1) + for j in range(9) for k in range(j + 1, 9)) + result.append((y, phase % 4)) + need(sorted(y for y, _ in result) == list(range(512)), "wrapper bijection") + return tuple(result) + + +def inverse_wrapper(plan): + result = [None] * 512 + for x, (y, phase) in enumerate(plan): + result[y] = (x, -phase % 4) + need(all(value is not None for value in result), "inverse wrapper totality") + return tuple(result) + + +def load_source(): + path = ROOT / SOURCE + need(path.stat().st_size <= 65536, "source size bound") + raw = path.read_bytes() + need(sha256(raw).hexdigest() == SOURCE_HASH, "source authentication") + records = json.loads(raw) + need(type(records) is list and len(records) == 4, "four native recipes") + plans = [] + for record in records: + need(type(record) is dict and set(record) == {"left", "right", "rank"}, + "native recipe schema") + need(type(record["rank"]) is int and record["rank"] == 1, "native rank") + plans.append((compile_wrapper(record["left"]), compile_wrapper(record["right"]))) + return records, tuple(plans) + + +def derive_circuit(plans): + circuit = [] + for j, inverse in STEPS: + left, right = plans[j] + before, after = ((inverse_wrapper(left), inverse_wrapper(right)) + if inverse else (right, left)) + entries = {before[x][0]: (i, before[x][1]) for i, x in enumerate(SUPPORT)} + need(len(entries) == 4, "four distinct kernel entries") + pairs = [] + for address in sorted(entries): + if address % 2: + continue + need(address + 1 in entries, "support closed under kernel pairing") + pair = [] + for t in (address, address + 1): + output, phase = after[t] + need(output in SUPPORT, "support closed under wrapper output") + pair.append((*entries[t], SUPPORT.index(output), phase)) + pairs.append(tuple(pair)) + need(len(pairs) == 2, "exactly two active pairs") + circuit.append(tuple(pairs)) + need(tuple(circuit) == CIRCUIT, "literal four-coordinate circuit") + + +def reduced_edge(values, stage, circuit=CIRCUIT, require_even=False): + output = [None] * 4 + for first, second in circuit[stage]: + a = rotate(values[first[0]], first[1]) + b = rotate(values[second[0]], second[1]) + c, d = lifting_pair(a, b, STEPS[stage][1], require_even) + output[first[2]] = rotate(c, first[3]) + output[second[2]] = rotate(d, second[3]) + need(all(value is not None for value in output), "reduced edge totality") + return tuple(output) + + +def reduced_loop(values, circuit=CIRCUIT): + for stage in range(4): + values = reduced_edge(values, stage, circuit) + return values + + +def literal_wrapper(values, record, inverse): + """Second decoder: explicit bit sums rather than compiled wrapper plans.""" + output = [None] * 512 + for x in range(512): + bits = tuple((x >> j) & 1 for j in range(9)) + y = record["offset"] + for j in range(9): + parity = sum(bits[k] * ((record["matrix_rows"][j] >> k) & 1) + for k in range(9)) % 2 + y ^= parity << j + phase = record["phase"] + sum(bits[j] * record["linear_Z4"][j] for j in range(9)) + phase += 2 * sum(bits[j] * bits[k] * ((record["quadratic_rows"][j] >> k) & 1) + for j in range(9) for k in range(j + 1, 9)) + if inverse: + output[x] = rotate(values[y], -phase) + else: + output[y] = rotate(values[x], phase) + need(all(value is not None for value in output), "literal wrapper totality") + return output + + +def literal_edge(values, record, inverse): + values = literal_wrapper(values, record["left" if inverse else "right"], inverse) + for x in range(0, 512, 2): + ar, ai = values[x] + br, bi = values[x + 1] + dr, di = ar - br, ai - bi + # Independent component formula; ceil(t/2) = -floor(-t/2). + first = (br + dr // 2 - di // 2, bi + di // 2 - (-dr // 2)) + second = (br + dr // 2 - (-di // 2), bi + di // 2 - dr // 2) + values[x], values[x + 1] = (second, first) if inverse else (first, second) + return literal_wrapper(values, record["right" if inverse else "left"], inverse) + + +def embed(values): + result = [(0, 0)] * 512 + for address, value in zip(SUPPORT, values, strict=True): + result[address] = value + return result + + +def translate(values, multiplier): + return tuple((a + multiplier * c, b + multiplier * d) + for (a, b), (c, d) in zip(values, DRIFT, strict=True)) + + +def check_orbit(records): + reduced, literal = START, embed(START) + orbit, cuts = [reduced], [] + for _ in range(24): + for stage, (j, inverse) in enumerate(STEPS): + reduced = reduced_edge(reduced, stage) + literal = literal_edge(literal, records[j], inverse) + need(literal == embed(reduced), "independent full-bank orbit edge") + cuts.append(reduced) + orbit.append(reduced) + need(reduced == translate(START, 1), "24-traversal nonzero drift identity") + need(any(value != (0, 0) for value in DRIFT), "drift nonzero") + need(sum(a * a + b * b for a, b in DRIFT) == 128, "squared drift norm") + return tuple(orbit), sha256(canonical(cuts)).hexdigest() + + +def check_covariance(): + shifts = [DRIFT] + shift = DRIFT + for stage in range(4): + shift = reduced_edge(shift, stage, require_even=True) + shifts.append(shift) + need(shift == DRIFT, "shift returns exactly") + rng = random.Random(5492) + for case in range(128): + width = 4 if case < 64 else 80 + values = tuple((rng.getrandbits(width + 1) - (1 << width), + rng.getrandbits(width + 1) - (1 << width)) for _ in range(4)) + multiplier = case - 64 + need(reduced_loop(translate(values, multiplier)) == + translate(reduced_loop(values), multiplier), "signed covariance fixture") + return shifts + + +def check_pair_oracle(): + count = 0 + for ar in range(-3, 4): + for ai in range(-3, 4): + for br in range(-3, 4): + for bi in range(-3, 4): + a, b = (ar, ai), (br, bi) + c, d = lifting_pair(a, b) + need(lifting_pair(c, d, True) == (a, b), "pair two-sided inverse") + dr, di = ar - br, ai - bi + expected = ((br + dr // 2 - di // 2, bi + di // 2 - (-dr // 2)), + (br + dr // 2 - (-di // 2), bi + di // 2 - dr // 2)) + need((c, d) == expected, "independent component formula") + count += 1 + return count + + +def check_iterates(orbit): + values = START + for n in range(24 * 32 + 1): + quotient, remainder = divmod(n, 24) + need(values == translate(orbit[remainder], quotient), "complete iterate formula") + if n < 24 * 32: + values = reduced_loop(values) + collision_inputs = [] + for k in range(33): + values = translate(START, -k) + collision_inputs.append(values) + for _ in range(24 * k): + values = reduced_loop(values) + need(values == START, "correction decoder collision family") + need(len(set(collision_inputs)) == 33, "distinct original inputs at one payload") + return 24 * 32 + 1, len(collision_inputs) + + +def check_controls(): + failures = 0 + try: + lifting_pair((1, 0), (0, 0), require_even=True) + except ValueError as error: + need(str(error) == "shift difference must be even", "exact parity rejection") + failures += 1 + need(failures == 1, "odd shift rejected") + values = START + for _ in range(12): + values = reduced_loop(values) + need(values != START and values != translate(START, 1), "false short-period control") + failures += 1 + altered = [[list(pair) for pair in stage] for stage in CIRCUIT] + entry = list(altered[0][0][0]) + entry[3] = (entry[3] + 1) % 4 + altered[0][0][0] = tuple(entry) + values = START + for _ in range(24): + values = reduced_loop(values, altered) + need(values != translate(START, 1), "absolute wrapper phase control") + failures += 1 + need(translate(START, -1) != translate(START, 1), "drift sign control") + failures += 1 + values = ((1, 0), (0, 0), (0, 0), (0, 0)) + before = values + for _ in range(12): + values = reduced_loop(values) + need(values == before, "periodic positive control") + need(reduced_loop(((0, 0),) * 4) == ((0, 0),) * 4, "zero positive control") + return failures, 2 + + +def run(): + records, plans = load_source() + derive_circuit(plans) + orbit, cut_hash = check_orbit(records) + shifts = check_covariance() + pair_cases = check_pair_oracle() + iterates, collisions = check_iterates(orbit) + rejection_controls, positive_controls = check_controls() + files = sorted(path for path in PACKAGE.iterdir() if path.is_file()) + need(len(files) <= 16 and all(path.stat().st_size <= 1048576 for path in files), + "package inventory bound") + return { + "status": "PASS_NATIVE_LOOP_LINEAR_DRIFT", "support": SUPPORT, + "start": START, "drift": DRIFT, "drift_squared_norm": 128, + "orbit": orbit, "shift_cuts": shifts, "orbit_edge_sha256": cut_hash, + "independent_full_bank_edges": 96, "shift_pair_evenness_checks": 8, + "covariance_fixtures": 128, "pair_oracle_cases": pair_cases, + "iterate_formula_checks": iterates, "same_payload_distinct_inputs": collisions, + "rejection_controls": rejection_controls, "positive_controls": positive_controls, + "source_sha256": SOURCE_HASH, + "package_sha256": {path.name: sha256(path.read_bytes()).hexdigest() for path in files}, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + parser.add_argument("--check-receipt", type=Path) + args = parser.parse_args() + need(not (args.receipt and args.check_receipt), "one receipt mode") + result = canonical(run()) + b"\n" + if args.receipt: + need(args.receipt.is_absolute() and not args.receipt.is_relative_to(ROOT), + "receipt must be outside the checkout") + with args.receipt.open("xb") as stream: + need(stream.write(result) == len(result), "complete receipt write") + if args.check_receipt: + need(args.check_receipt.stat().st_size <= 1048576, "receipt size bound") + need(args.check_receipt.read_bytes() == result, "generated receipt equality") + print(result.decode(), end="") + + +if __name__ == "__main__": + main()