From 4d3f1c69be00a7c470064091b86f549256e7d87a Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 12 Nov 2026 18:31:52 +0000 Subject: [PATCH 1/2] feat(research): prove sharp endpoint-promised C prefix scales --- .../native-c-endpoint-prefix-scale/PROOF.md | 145 ++++++++++ .../native-c-endpoint-prefix-scale/README.md | 148 ++++++++++ .../SOURCES.json | 30 ++ .../native-c-endpoint-prefix-scale/TASK.json | 120 ++++++++ .../VERIFY.json | 34 +++ .../native-c-endpoint-prefix-scale/verify.py | 264 ++++++++++++++++++ 6 files changed, 741 insertions(+) create mode 100644 research/native-c-endpoint-prefix-scale/PROOF.md create mode 100644 research/native-c-endpoint-prefix-scale/README.md create mode 100644 research/native-c-endpoint-prefix-scale/SOURCES.json create mode 100644 research/native-c-endpoint-prefix-scale/TASK.json create mode 100644 research/native-c-endpoint-prefix-scale/VERIFY.json create mode 100644 research/native-c-endpoint-prefix-scale/verify.py diff --git a/research/native-c-endpoint-prefix-scale/PROOF.md b/research/native-c-endpoint-prefix-scale/PROOF.md new file mode 100644 index 0000000000..6e257715bf --- /dev/null +++ b/research/native-c-endpoint-prefix-scale/PROOF.md @@ -0,0 +1,145 @@ +# Sharp scale for endpoint-integral native C tensors + +This proof was produced by Nick Petalas. Apache-2.0. + +Put `O=Z[i]`, `pi=1+i`, and + +```text +C = [[1+i,1-i],[1-i,1+i]]/2 + = pi^-1 [[i,1],[1,i]]. +``` + +For `f>=1`, let `C_a` apply C on binary address bit a, and set +`F=C_0 ... C_(f-1)`. Let `C_S=product_(a in S) C_a`. Distinct axes +commute. The endpoint-promised input domain is + +```text +L_f = {x in O^(2^f) : F x in O^(2^f)}. +``` + +Both the input and final output are exact Gaussian integers. No assumption +about intermediate integrality is made. Arbitrary signs, imaginary parts +and independent spectator fibres are allowed. + +## Theorem + +For every `S subset {0,...,f-1}`, put `j=|S|` and `d=min(j,f-j)`. +The least nonnegative integer e such that + +```text +pi^e C_S L_f is contained in O^(2^f) +``` + +is exactly `d`. The least nonnegative integer s such that +`2^s C_S L_f` is integral is exactly `ceil(d/2)`. + +Consequently the least common Gaussian scale for every partial axis product +is `pi^floor(f/2)`, and the least common binary scale is + +```text +2^ceil(floor(f/2)/2). +``` + +The same common scales are minimal for the prefixes of any single fixed +axis ordering. They suffice for every ordering simultaneously. Minimality +is over all inputs in `L_f`, rather than for each individual input. + +## Upper bound from the two endpoints + +Direct multiplication gives + +```text +pi C = [[i,1],[1,i]], +pi C^-1 = [[1,i],[i,1]], +C^2 = [[0,1],[1,0]], +C (1,1)^T = (1,1)^T. +``` + +In particular, `pi C` and `pi C^-1` are Gaussian integral. If `x in L_f` +and `y=F x`, then + +```text +C_S x is in pi^-j O^(2^f), +C_S x = C_(S complement)^-1 y is in pi^-(f-j) O^(2^f). +``` + +For nonnegative a,b, the two fractional modules are nested and their +intersection is `pi^-min(a,b) O^(2^f)`. This proves the bound d, using +only the two endpoint promises. Since `pi^2=2i`, multiplying by +`2^ceil(d/2)` clears those denominators. + +## Matching input at every cut + +Pair d distinct axes in S with d distinct axes outside S. On each pair +use the integer array + +```text +v = e_00 + e_11. +``` + +On every unpaired axis use `u=e_0+e_1`. Let x be their tensor product, +with factors placed on the specified axes. This has only zero/one real +entries and zero imaginary parts. + +The complete transform fixes u and sends each v to `e_01+e_10`. +Indeed C is symmetric and `C^2` is the bit swap, so this identity follows +by multiplying the displayed two-by-two matrices. Thus both x and F x +are Gaussian integral, and x belongs to `L_f`. + +At the chosen cut, exactly one axis in each pair has been transformed. +Its four entries, in address order, are + +```text +(C tensor I) v = pi^-1 (i,1,1,i). +``` + +The same identity holds with the pair's axes exchanged. The unpaired u +factors remain fixed. Every coordinate of `C_S x` is therefore a Gaussian +unit times `pi^-d`. A Gaussian unit is not divisible by pi. Hence no +smaller exponent e can clear the Gaussian denominator. + +Multiplication by `2^s` increases pi divisibility by exactly `2s`, because +`2=-i pi^2`. The same example is integral after that multiplication if +and only if `2s>=d`. This proves the binary lower bound. At a middle cut +of any fixed ordering, `d=floor(f/2)`, proving both common-scale minima. + +## Arithmetic interface consequence + +Suppose a supplied array x and its intended `F x` are Gaussian integral. +Scale the input by the theorem's common binary factor, apply the ordinary +axis sequence, then divide the completed output by the same factor. +Every axis output is integral, and the final division is exact. The +returned mathematical output is exactly `F x`. + +This statement is an arithmetic composition. It supplies neither a +literal scaling program nor a signed-range bound. An implementation must +still pay both conversions, preserve ownership, allocate sufficient +intermediate signed width and scratch, and admit its actual producer's +endpoint promise. The argument applies independently to every spectator +fibre of the positive rank-one native leaf, so it covers arbitrary f in +the stated tensor model without asserting physical implementation. + +## Relation to earlier work and scope + +Jerry Chen / CubeJerry's PR7429 defines this positive C tensor at selected +MOVE24472 and requires every axis output to be integral and fit the signed +width. Its f=2 example already distinguishes final and intermediate +integrality. That distinction and the machine implementation are credited +premises, not new findings or replay targets here. + +Jose Manuel / jmbarrancoml's PR3091 supplies the physical axis method and +retains Alejandro Zarzuelo Urdiales's sharp `ceil(f/2)` binary reserve for +arbitrary inputs. The new bound uses the additional *integral final +output* premise, so it does not replace that unrestricted-input reserve. + +Clear1nsight's PR3382 characterizes the integral entrance on which every +partial coordinate product is already integral. That maximal exactness +lattice is an established result. The proof here does not reconstruct +or use its characterization. The new result is the exact scalar needed +to move the larger endpoint-promised domain into every partial-product +integrality domain, with a matching input at every cut. + +No denominator theorem for arbitrary Clifford words, intervening +noncommuting maps, nonintegral final outputs or rounded trajectories is +asserted. The statement concerns exactly the commuting coordinate C +tensors defined above. All five selected framework assumptions remain. diff --git a/research/native-c-endpoint-prefix-scale/README.md b/research/native-c-endpoint-prefix-scale/README.md new file mode 100644 index 0000000000..05de5603ca --- /dev/null +++ b/research/native-c-endpoint-prefix-scale/README.md @@ -0,0 +1,148 @@ +# Sharp integral-prefix scale for the positive native C tensor + +This scoped written proof with exact finite corroboration was produced by +Nick Petalas. Apache-2.0. No new kappa or selected-frontier change is claimed. + +For `C=[[1+i,1-i],[1-i,1+i]]/2`, suppose both x and `C^(tensor f) x` +are Gaussian-integer arrays. The least common binary input scale making +every axis prefix integral is exactly + +```text +2^ceil(floor(f/2)/2). +``` + +More precisely, at any cut with j processed axes, the sharp Gaussian +denominator exponent is `min(j,f-j)`, in units of `pi=1+i`. The sharp +binary scale at that cut is `2^ceil(min(j,f-j)/2)`. This covers every +subset of axes and therefore every fixed axis order. It allows arbitrary +Gaussian-integer inputs satisfying the final-output promise, with arbitrary +spectator fibres. + +[PROOF.md](PROOF.md) proves the all-f statement. From the input, the cut +has at most j Gaussian denominator factors. From the integral output, its +inverse suffix has at most f-j. Paired-coordinate integer inputs attain +the smaller exponent at every cut. + +## What changes + +Jerry Chen / CubeJerry's [PR7429](https://github.com/CrocSwap/integer-mult-bounds/pull/7429) +implements this tensor as the positive rank-one central leaf of selected +MOVE24472. It requires integral, width-fitting outputs at every axis and +already gives an f=2 example with integral endpoints but a nonintegral +intermediate. That example and the implementation are credited prior work. + +The new arithmetic bridge is to multiply an endpoint-promised input by the +sharp scale, run the ordinary axes with exact divisions, and divide the +completed output by the same scale. Every intermediate axis output is +integral and the original mathematical output is returned exactly. + +The unrestricted-input reserve `ceil(f/2)` is established prior work, +retained in Jose Manuel / jmbarrancoml's [PR3091](https://github.com/CrocSwap/integer-mult-bounds/pull/3091) +and credited there to Alejandro Zarzuelo Urdiales. The smaller exponent +here uses an additional endpoint promise. Clear1nsight's +[PR3382](https://github.com/CrocSwap/integer-mult-bounds/pull/3382) characterizes +the different entrance where all partial products are already integral. +Neither predecessor theorem nor executable is audited or replayed here. + +## Exact finite evidence + +The standard-library checker imports no predecessor code. It checks: + +- 164 sharp cut witnesses, covering every axis subset through f=6 and + every prefix cut for f=7 through 10. Each also executes the complete + scaled arithmetic program and exact final division. +- All 65,808 Gaussian arrays with real and imaginary components in `{0,1}` + for f=1,2,3. Exactly 968 have integral final outputs; all their 3,792 + checked prefixes satisfy both denominator bounds. The other 64,840 + inputs are outside the promised endpoint domain. +- 180 signed complex prefixes checked against a separately coded rational + butterfly, with direct tensor-entry comparisons through f=4. +- All 153 axis permutations at f=1 through 5 on the paired witnesses. +- Eight named semantic controls, including a scale one bit too small at + f=6, a missing endpoint promise, inexact divisions, inverse-phase + confusion and a signed complex dirty offset. + +Finite checks corroborate the written proof. They do not enumerate the +unbounded input lattice. Every acceptance check remains active under `-O`. +The verifier writes nothing and prints a generated receipt containing the +results, Python version and SHA256 of every package file. No receipt is +hand-written or checked in. + +## Reproduce + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/native-c-endpoint-prefix-scale/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/native-c-endpoint-prefix-scale/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/native-c-endpoint-prefix-scale +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/native-c-endpoint-prefix-scale --check-source-history +``` + +Substitute any installed CPython 3.12 path on another host. Expected markers +are `PASS_NATIVE_C_ENDPOINT_PREFIX_SCALE`, `PASS_REGISTERED_RESEARCH_PACKAGE` +and, after committing, `PASS_RESEARCH_COMMIT_BYTES`. The standalone verifier +also works in a Git-free package copy. Each registered command has a +120-second cap. Normal and optimized direct runs take less than a second +locally; these are check durations, not physical performance measurements. + +## Scope and source boundary + +The claim is a new numerical interface theorem for a stated tensor, with +no changed supplier word. It does not establish that a production caller +supplies the endpoint promise. Signed range, scratch width, physical +scaling/unscaling, ownership, tape movement, compiler closure, stock and +the complete paid/productive invoice remain separate obligations. All five +selected framework assumptions remain. No native machine, selected cold +replay, Lean, Docker or complete multiplication theorem is run or claimed. +Independent human and formal proof-kernel review are unclaimed. + +The base is canonical main `e54523517d0f03e58352e647c403a5af3e525a57`, +priority revision 8, selected #7000. [TASK.json](TASK.json) records the +explicit change from the formal-interface card to this written arithmetic +proof. [SOURCES.json](SOURCES.json) pins canonical provenance only. The +definition and proof are self-contained, with no external executable or +data inputs. TASK also records #7429's exact head, README path and the SHA256 +of the source text inspected. That external document is provenance, not a +registered replay dependency or an asserted independently certified input. + +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19571939). +Live claims, the account's recent contributions, the main-tree READMEs and +merged PRs were checked for the formula, tensor, endpoint promise and more +general partial-product forms. The overlap snapshot reported complete +pagination of 760 open PRs and 7,346 Discussion records, without warnings. +No same-scope result was found in that coverage. Arbitrary unpublished work +and unsearched diffs remain outside it. + +Power of Ten inspection found no recursion, dynamic evaluation, subprocesses +or writes in the verifier. All arithmetic domains are fixed: f is at most +10, arrays have at most 1,024 entries, and the exhaustive loop has at most +65,536 cases at one f. Every function is under 60 physical lines. All gates +use exact integers or Fractions and explicit failure checks. Receipt hashing +caps the inventory at twelve files and each file at 1 MiB. Managed Python +allocation is a deviation from fixed steady-state allocation; the fixed +domains bound live collections, but runtime allocation internals are not +measured. Warning-strict normal and optimized execution supplies the available +diagnostics; no separate static analyzer or native fixed-allocation version +is supplied. + +## Open next questions + +Can the sharp scale be installed around one literal positive C leaf with +a favorable complete physical bill? First supply an actual producer with +the required endpoint promise, bound every scaled intermediate magnitude, +and price both exact conversions together with movement, owners and retained +history. Those missing contracts prevent a supplier or kappa claim. This +package stops at the first sharp arithmetic result and reserves no follow-up. + +## Credit + +The new proof, matching all-cut witnesses and checker were produced by +Nick Petalas. Jerry Chen / CubeJerry supplies PR7429's literal leaf and its +explicit integrality boundary. Jose Manuel / jmbarrancoml supplies PR3091's +physical axis method, retaining Alejandro Zarzuelo Urdiales's C/parity and +tensor-reserve credit. Clear1nsight supplies PR3382's maximal simultaneous +exactness lattice. The selected native, Gaussian, controller and physical +lineage retains its predecessor credit. Fractional-ideal arithmetic and +tensor-product identities are classical; no literature-wide priority is +claimed for those methods. diff --git a/research/native-c-endpoint-prefix-scale/SOURCES.json b/research/native-c-endpoint-prefix-scale/SOURCES.json new file mode 100644 index 0000000000..4fcd4143c4 --- /dev/null +++ b/research/native-c-endpoint-prefix-scale/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/physical-gaussian-leaf/README.md", + "usage": "provenance", + "git_blob": "573a0c3c9df984a397c112026dfc2d8e2cc94c66", + "sha256": "60f82399ac13f3c0f1f10de6488021b64240711190a09962568f2d72ea302eb0" + }, + { + "path": "research/p104-clifford-exactness/README.md", + "usage": "provenance", + "git_blob": "581edcfcbcc31cf78c02f9873c14094f9b37e1bf", + "sha256": "7374b6b360fa6755f68ee513467de1c0436a48a22a9584a3c27687e73a16a7db" + } + ] +} diff --git a/research/native-c-endpoint-prefix-scale/TASK.json b/research/native-c-endpoint-prefix-scale/TASK.json new file mode 100644 index 0000000000..ba49b422d4 --- /dev/null +++ b/research/native-c-endpoint-prefix-scale/TASK.json @@ -0,0 +1,120 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact all-f Gaussian and binary scales clearing every partial-axis C tensor on Gaussian-integral inputs whose complete C tensor output is Gaussian integral.", + "scope_change_reason": "The formal-interface card is narrowed to a written numerical implication exposed by PR7429, without a proof-assistant build or selected-assumption discharge.", + "bottleneck_link": "Provides the sharp arithmetic scale converting an endpoint-integrality promise into the intermediate-integrality precondition of the positive C native leaf. Physical width, conversion tariffs and the full caller remain separate.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved sharp scale with exact attaining inputs and bounded finite corroboration; leave physical implementation and range pricing to an explicit next question.", + "outcome": "completed", + "evidence": "PROOF.md gives the two-boundary fractional-ideal argument and matching paired-coordinate input for every cut. verify.py checks exact finite witnesses, exhaustive small inputs, independent arithmetic oracles and semantic controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the sharp scale be installed around the literal positive C leaf with a favorable complete physical bill?", + "why_it_matters": "The theorem closes intermediate integrality under an endpoint promise, but extra scaling and wider signed fields may consume its benefit.", + "first_step": "Supply one actual endpoint-integral producer, bound every scaled intermediate magnitude, and price both exact conversions, tape movement, owners and retained history.", + "blocked_by": "No literal scaling wrapper, signed-range theorem, producer admission or complete recursive comparison is supplied." + } + ], + "playbook": "Autonomous local run", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19571939", + "predecessors": [ + { + "pr": 7429, + "author": "CubeJerry", + "head": "1a555e469b89af70d309bc966f8f813ac11dc887", + "path": "research/literal-positive-c-leaf/README.md", + "sha256": "d806cf3772570ecccb9b45de1570bdeba723765fe494192f074aee8f041ccdf5", + "usage": "Question and numerical-boundary provenance only; no executable or scientific receipt is imported.", + "url": "https://github.com/CubeJerry/integer-mult-bounds/blob/1a555e469b89af70d309bc966f8f813ac11dc887/research/literal-positive-c-leaf/README.md" + }, + { + "pr": 3091, + "author": "jmbarrancoml", + "path": "research/physical-gaussian-leaf/README.md", + "usage": "Credited physical axis method and retained unrestricted ceil(f/2) reserve; not replayed." + }, + { + "pr": 3382, + "author": "Clear1nsight", + "path": "research/p104-clifford-exactness/README.md", + "usage": "Related all-partial-product exactness lattice; its theorem is neither used nor replayed." + } + ] +} diff --git a/research/native-c-endpoint-prefix-scale/VERIFY.json b/research/native-c-endpoint-prefix-scale/VERIFY.json new file mode 100644 index 0000000000..45c095717e --- /dev/null +++ b/research/native-c-endpoint-prefix-scale/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact sharp cut witnesses, endpoint-promised exhaustive small-box inputs, independent rational and dense-tensor oracles, axis-order permutations, scaling composition and named semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact sharp cut witnesses, endpoint-promised exhaustive small-box inputs, independent rational and dense-tensor oracles, axis-order permutations, scaling composition and named semantic controls." + } + ] +} diff --git a/research/native-c-endpoint-prefix-scale/verify.py b/research/native-c-endpoint-prefix-scale/verify.py new file mode 100644 index 0000000000..a504d886ef --- /dev/null +++ b/research/native-c-endpoint-prefix-scale/verify.py @@ -0,0 +1,264 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the native C prefix-scale theorem. + +Produced by Nick Petalas. Apache-2.0. Standard library only. +No predecessor executable is imported or run. All checks survive -O. +""" + +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from itertools import permutations, product +from pathlib import Path +import json +import random +import sys + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def multiply(z, w): + return z[0] * w[0] - z[1] * w[1], z[0] * w[1] + z[1] * w[0] + + +def axis_numerator(values, axis): + """Apply 2C using real integer rows, without any division.""" + out = list(values) + for a in range(len(values)): + if a & (1 << axis): + continue + b = a | (1 << axis) + ar, ai = values[a] + br, bi = values[b] + out[a] = ar - ai + br + bi, ar + ai - br + bi + out[b] = ar + ai + br - bi, ai - ar + br + bi + return out + + +def prefixes(values, order): + result = [list(values)] + for axis in order: + result.append(axis_numerator(result[-1], axis)) + return result + + +def is_integral(numerators, denominator): + return all(a % denominator == b % denominator == 0 for a, b in numerators) + + +def divide(numerators, denominator): + need(is_integral(numerators, denominator), "nonintegral Gaussian value") + return [(a // denominator, b // denominator) for a, b in numerators] + + +def scaled_program(values, order, scale): + current = [(scale * a, scale * b) for a, b in values] + for axis in order: + current = divide(axis_numerator(current, axis), 2) + return divide(current, scale) + + +def rational_axis(values, axis): + """Independent complex multiplication with rational coefficients.""" + diagonal = Fraction(1, 2), Fraction(1, 2) + off = Fraction(1, 2), Fraction(-1, 2) + out = list(values) + for a in range(len(values)): + if a & (1 << axis): + continue + b = a | (1 << axis) + u, v = multiply(diagonal, values[a]), multiply(off, values[b]) + out[a] = u[0] + v[0], u[1] + v[1] + u, v = multiply(off, values[a]), multiply(diagonal, values[b]) + out[b] = u[0] + v[0], u[1] + v[1] + return out + + +def dense_tensor(values, f, selected): + """Direct tensor entries i^(d-HammingDistance)/pi^d on selected bits.""" + mask = sum(1 << a for a in selected) + d = len(selected) + denominator = (1, 0) + for _ in range(d): + denominator = multiply(denominator, (1, 1)) + norm = denominator[0] ** 2 + denominator[1] ** 2 + inverse = Fraction(denominator[0], norm), Fraction(-denominator[1], norm) + units = ((1, 0), (0, 1), (-1, 0), (0, -1)) + result = [] + for a in range(1 << f): + total = (0, 0) + for b in range(1 << f): + if (a ^ b) & ~mask: + continue + exponent = d - ((a ^ b) & mask).bit_count() + term = multiply(units[exponent % 4], values[b]) + total = total[0] + term[0], total[1] + term[1] + result.append(multiply(total, inverse)) + return result + + +def witness(f, selected): + selected = tuple(sorted(selected)) + other = tuple(a for a in range(f) if a not in selected) + pairs = tuple(zip(selected, other)) + values, endpoint = [], [] + for address in range(1 << f): + equal = all(((address >> a) ^ (address >> b)) & 1 == 0 for a, b in pairs) + opposite = all(((address >> a) ^ (address >> b)) & 1 == 1 for a, b in pairs) + values.append((int(equal), 0)) + endpoint.append((int(opposite), 0)) + return values, endpoint + + +def check_cut(f, selected): + x, expected = witness(f, selected) + order = tuple(selected) + tuple(a for a in range(f) if a not in selected) + history = prefixes(x, order) + need(divide(history[-1], 1 << f) == expected, "witness endpoint") + common = 1 << (((f // 2) + 1) // 2) + need(scaled_program(x, order, common) == expected, "scaled arithmetic program") + j = len(selected) + d = min(j, f - j) + pi_power = (1, 0) + for _ in range(d): + pi_power = multiply(pi_power, (1, 1)) + cut = [multiply(v, pi_power) for v in history[j]] + integral = divide(cut, 1 << j) + need(all(abs(a) + abs(b) == 1 for a, b in integral), "sharp Gaussian denominator") + binary = 1 << ((d + 1) // 2) + divide([(binary * a, binary * b) for a, b in history[j]], 1 << j) + if binary > 1: + need(not is_integral([(binary // 2 * a, binary // 2 * b) + for a, b in history[j]], 1 << j), "binary lower bound") + if f <= 4: + need(dense_tensor(x, f, selected) == + [(Fraction(a, 1 << j), Fraction(b, 1 << j)) for a, b in history[j]], + "direct tensor oracle") + return {"f": f, "cut": j, "gaussian_exponent": d, "binary_scale": binary} + + +def exhaustive_box(): + """Every Gaussian 0/1-component array through three axes.""" + counts = Counter() + for f in range(1, 4): + n = 1 << f + scale = 1 << (((f // 2) + 1) // 2) + for flat in product((0, 1), repeat=2 * n): + x = list(zip(flat[::2], flat[1::2])) + history = prefixes(x, range(f)) + counts["inputs"] += 1 + if not is_integral(history[-1], 1 << f): + counts["outside_endpoint_domain"] += 1 + continue + counts["endpoint_integral"] += 1 + for j, row in enumerate(history): + d = min(j, f - j) + pi = (1, 0) + for _ in range(d): + pi = multiply(pi, (1, 1)) + divide([multiply(z, pi) for z in row], 1 << j) + divide([(scale * a, scale * b) for a, b in row], 1 << j) + counts["prefixes"] += 1 + return dict(counts) + + +def independent_oracles(): + rng = random.Random(8527429) + count = 0 + for f in range(1, 6): + for _ in range(12): + x = [(rng.randrange(-7, 8), rng.randrange(-7, 8)) for _ in range(1 << f)] + order = tuple(rng.sample(range(f), f)) + integer = prefixes(x, order) + rational = [(Fraction(a), Fraction(b)) for a, b in x] + for j, axis in enumerate(order, 1): + rational = rational_axis(rational, axis) + need(rational == [(Fraction(a, 1 << j), Fraction(b, 1 << j)) + for a, b in integer[j]], "independent rational prefix") + if f <= 4: + need(rational == dense_tensor(x, f, order[:j]), "dense tensor prefix") + count += 1 + return count + + +def permutation_checks(): + count = 0 + for f in range(1, 6): + x, endpoint = witness(f, range(f // 2)) + scale = 1 << (((f // 2) + 1) // 2) + for order in permutations(range(f)): + history = prefixes(x, order) + need(divide(history[-1], 1 << f) == endpoint, "axis order endpoint") + for j, row in enumerate(history): + divide([(scale * a, scale * b) for a, b in row], 1 << j) + count += 1 + return count + + +def controls(): + checked = [] + x, endpoint = witness(6, range(3)) + h = prefixes(x, range(6)) + need(divide(h[-1], 64) == endpoint, "six-axis promise") + checked.append("six_axis_integral_endpoint") + need(not is_integral([(2*a, 2*b) for a, b in h[3]], 8), "one bit too little") + checked.append("one_bit_below_sharp_scale") + impulse = [(1, 0)] + [(0, 0)] * 7 + bad = prefixes(impulse, range(3)) + need(not is_integral(bad[-1], 8), "missing endpoint hypothesis") + checked.append("unpromised_endpoint") + need(not is_integral([(2*a, 2*b) for a, b in bad[-1]], 8), "unpromised scale") + checked.append("scale_without_endpoint_promise_fails") + for bad_denominator in (2, 4): + rejected = False + try: + divide([(1, 0)], bad_denominator) + except ValueError as error: + rejected = str(error) == "nonintegral Gaussian value" + need(rejected, "inexact division must reject") + checked.append("inexact_division_" + str(bad_denominator)) + minus = rational_axis([(Fraction(1), Fraction(0)), (Fraction(0), Fraction(0))], 0) + need(minus != [(Fraction(1,2), Fraction(-1,2)), + (Fraction(1,2), Fraction(1,2))], "inverse/phase confusion") + checked.append("forward_not_inverse_phase") + shifted = [(a - 8, b + 8) for a, b in x] + need(divide(prefixes(shifted, range(6))[-1], 64) == + [(a - 8, b + 8) for a, b in endpoint], "arbitrary signed dirty offset") + checked.append("signed_complex_dirty_offset") + return checked + + +def run(): + cuts = [] + for f in range(1, 7): + for mask in range(1 << f): + cuts.append(check_cut(f, tuple(a for a in range(f) if mask & (1 << a)))) + for f in range(7, 11): + for j in range(f + 1): + cuts.append(check_cut(f, tuple(range(j)))) + summary = { + "claim_type": "scoped written proof with exact finite corroboration", + "cut_witnesses": len(cuts), + "cut_profile_sha256": sha256(json.dumps(cuts, sort_keys=True).encode()).hexdigest(), + "exhaustive_box": exhaustive_box(), + "independent_prefixes": independent_oracles(), + "axis_permutations": permutation_checks(), + "controls": controls(), + "binary_scales_f1_to_f10": [1 << (((f // 2) + 1) // 2) for f in range(1, 11)], + } + here = Path(__file__).resolve().parent + files = sorted(p for p in here.iterdir() if p.is_file()) + need(len(files) <= 12, "package inventory cap") + need(all(p.stat().st_size <= 2**20 for p in files), "package byte cap") + receipt = {"result": summary, + "files": {p.name: sha256(p.read_bytes()).hexdigest() for p in files}, + "python": sys.version.split()[0]} + print(json.dumps(receipt, sort_keys=True, indent=2)) + print("PASS_NATIVE_C_ENDPOINT_PREFIX_SCALE") + + +if __name__ == "__main__": + run() From 8b0dd714d30e9c1574387587eb6418ae99ac34e1 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 12 Nov 2026 18:32:37 +0000 Subject: [PATCH 2/2] docs(research): state the production credit explicitly --- research/native-c-endpoint-prefix-scale/README.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/research/native-c-endpoint-prefix-scale/README.md b/research/native-c-endpoint-prefix-scale/README.md index 05de5603ca..d1a72ee127 100644 --- a/research/native-c-endpoint-prefix-scale/README.md +++ b/research/native-c-endpoint-prefix-scale/README.md @@ -1,7 +1,8 @@ # Sharp integral-prefix scale for the positive native C tensor -This scoped written proof with exact finite corroboration was produced by -Nick Petalas. Apache-2.0. No new kappa or selected-frontier change is claimed. +This contribution was produced by Nick Petalas. Apache-2.0. +Claim type: scoped written proof with exact finite corroboration. +No new kappa or selected-frontier change is claimed. For `C=[[1+i,1-i],[1-i,1+i]]/2`, suppose both x and `C^(tensor f) x` are Gaussian-integer arrays. The least common binary input scale making