From d4f642424b374cdabd20355427ee903165871257 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 30 Oct 2026 13:51:35 +0000 Subject: [PATCH] feat(research): prove exact rounded-native fiber radius --- .../rounded-native-fiber-radius/MATRIX.json | 918 ++++++++++++++++++ research/rounded-native-fiber-radius/PROOF.md | 113 +++ .../rounded-native-fiber-radius/README.md | 123 +++ .../rounded-native-fiber-radius/SOURCES.json | 36 + .../rounded-native-fiber-radius/TASK.json | 112 +++ .../rounded-native-fiber-radius/VERIFY.json | 34 + .../rounded-native-fiber-radius/WITNESS.json | 117 +++ .../rounded-native-fiber-radius/verify.py | 186 ++++ 8 files changed, 1639 insertions(+) create mode 100644 research/rounded-native-fiber-radius/MATRIX.json create mode 100644 research/rounded-native-fiber-radius/PROOF.md create mode 100644 research/rounded-native-fiber-radius/README.md create mode 100644 research/rounded-native-fiber-radius/SOURCES.json create mode 100644 research/rounded-native-fiber-radius/TASK.json create mode 100644 research/rounded-native-fiber-radius/VERIFY.json create mode 100644 research/rounded-native-fiber-radius/WITNESS.json create mode 100644 research/rounded-native-fiber-radius/verify.py diff --git a/research/rounded-native-fiber-radius/MATRIX.json b/research/rounded-native-fiber-radius/MATRIX.json new file mode 100644 index 0000000000..0aa9f78163 --- /dev/null +++ b/research/rounded-native-fiber-radius/MATRIX.json @@ -0,0 +1,918 @@ +{ + "schema": "literal-eight-mode-columns-v1", + "source_path": "research/coded-native-caller/NORMALIZERS.json", + "mode_columns": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + -1, + 1, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + 1, + 1, + -1, + -1, + -1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + -1, + 1, + -1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + -1, + 1, + -1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + -1, + 1, + 0, + 0, + -1, + 1, + 1, + 1, + 0, + -1, + -1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + -1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 1, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 1, + 1, + 1, + 0, + 1, + 0, + 0, + 0, + 1, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0 + ], + [ + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + 0, + -1, + -1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + -1, + -1, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 0, + 1, + 0, + 1, + -1, + 0, + 0, + 0, + 1, + 0, + 1, + 1, + 0, + 0, + 0, + 1, + 0, + 0, + -1, + -1, + -1, + 1, + 1, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + -1, + -1, + -1, + 0, + 0 + ], + [ + 0, + 1, + 1, + 0, + 1, + 1, + -1, + 0, + 0, + 1, + 0, + 0, + 0, + -1, + 0, + 0, + 1, + 0, + -1, + -1, + 1, + 1, + 0, + 0, + -1, + -1, + 0, + 0, + -1, + 0, + 0, + 0, + -1, + 0, + 0, + 1, + -1, + -1, + 0, + 1, + 1, + 0, + 0, + -1, + -1, + -1, + -1, + -1, + 1, + 0, + 0, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 0, + 0, + -1, + 0, + 0, + 1, + 1, + 0, + 0, + -1, + -1, + 0, + 0, + -1, + 0, + 0, + -1, + 0, + 0, + 1, + -1, + 0, + 0, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 0, + 0, + 0, + -1, + 1, + 0, + -1, + -1, + -1, + -1, + 0, + -1, + -1, + 0, + 1, + 0, + 0, + 1, + 0, + 0, + 1, + 1 + ], + [ + 0, + 1, + 0, + 1, + 0, + 0, + -1, + 0, + -1, + 0, + 1, + 1, + -1, + 0, + -1, + -1, + 0, + -1, + 0, + 0, + -1, + -1, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + -1, + -1, + 1, + 0, + 0, + -1, + -1, + 0, + 0, + -1, + -1, + -1, + -1, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 0, + -1, + 0, + 0, + 0, + -1, + -1, + 0, + 0, + 1, + -1, + 0, + 0, + -1, + -1, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 0, + -1, + 0, + -1, + 0, + 0, + 1, + 1, + 0, + 1, + 0, + 1, + 1, + 0, + -1, + 0, + -1, + 0, + 0, + -1, + 0, + -1, + 0, + 0, + -1, + 0, + 1, + 1, + -1, + 0, + 0, + -1, + -1 + ], + [ + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + -1, + 0, + 0, + 1, + 1, + -1, + -1, + 0, + -1, + -1, + 0, + 0, + -1, + -1, + -1, + 0, + -1, + -1, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + -1, + -1, + 0, + 1, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + -1, + -1, + 0, + 0, + -1, + 1, + -1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + -1, + -1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + -1, + -1, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 1, + 1, + -1, + -1 + ], + [ + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + -1, + 1, + 0, + 0, + 1, + -1, + 0, + 0, + -1, + 1, + 1, + -1, + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 1, + -1, + 0, + -1, + 1, + 0, + 1, + -1, + -1, + 1, + 0, + 0, + 0, + 1, + -1, + 0, + -1, + 1, + 0, + -1, + 1, + -1, + 1, + 0, + 0, + 0, + -1, + 1, + 0, + 1, + -1, + -1, + 1, + 0, + 0, + -1, + 1, + -1, + 1, + 0, + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + 0, + 0, + 0, + 0, + -1, + 1, + 0, + 0, + 0, + -1, + 1, + 0, + 0, + -1, + 1, + 0, + -1, + 1, + 1, + -1 + ] + ] +} diff --git a/research/rounded-native-fiber-radius/PROOF.md b/research/rounded-native-fiber-radius/PROOF.md new file mode 100644 index 0000000000..ddedab3957 --- /dev/null +++ b/research/rounded-native-fiber-radius/PROOF.md @@ -0,0 +1,113 @@ +# The exact input radius is three + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Fixed contract and credited premises + +Let M be the literal 112 by 8 signed integer matrix in MATRIX.json, copied +byte for byte from zxv's PR5444, research/precision-state-frontier/FIXTURE.json. +Every row has four nonzero entries of absolute value one, and M^T M = 56 I. +The map is exactly + + F(x) = 8x - M R(8 M^T x / 52), x in Z^112, + +where R rounds each component to nearest, with half ties away from zero. +For an output y, put s=M^T y and write q for its rounded quotient. PR5444's +fiber theorem and its source lattice calculation give these premises. + +1. Preimages are exactly x=(y+Mq)/8 with y+Mq divisible by 8 and + R((s+56q)/52)=q. For each coordinate, the latter condition leaves at most + thirteen consecutive integers, with its stated half-tie endpoint rules. +2. ker(M modulo 8) consists exactly of 4v with v modulo 2 in a binary + linear code C of size sixteen. In particular, every fiber's quotients + have one fixed residue modulo 4, and at most sixteen parity classes + after dividing differences by 4. +3. M has full column rank, as also follows from the displayed Gram identity. + +These are credited predecessor results, not new theorems of this package. +The source's maximum fiber at this scale is 4096. Its published sufficient +radius is sixteen, and its finite-range threshold question is explicitly open. + +Define H_* as the least nonnegative integer H for which some output y has +4096 distinct preimages satisfying ||x||_infinity <= H. We prove H_*=3. +The same fixed origin-centered box must contain the whole fiber. + +## Lower bound, for every output + +Fix y. Partition its quotient candidates by their residues modulo 8. +There are at most sixteen nonempty cells by premise 2. Within each cell, +each quotient coordinate lies in an interval of thirteen consecutive +integers and in one residue modulo 8. It therefore has at most two values. +Every cell has at most 2^8=256 points. If the fiber contains 4096 points, +it has exactly sixteen full cells, and each is the complete Cartesian +product of eight two-point sets, every pair separated by eight. + +Let c be the coordinatewise midpoint of one such quotient cell. In owner +coordinate i, the corresponding inputs have midpoint + + (y_i + (Mc)_i) / 8 + +and range of width four. Indeed, the four signed nonzero row entries +independently select endpoints separated by eight, so their total range +is 32 before division by eight. This uses the full Cartesian cell. + +Suppose all these inputs lie in [-2,2]^112. Every width-four owner +interval must then be exactly [-2,2], so its midpoint is zero. Thus + + y + Mc = 0. + +This holds for every one of the sixteen cells. Distinct cells have distinct +quotient midpoints: the two members in a coordinate have a fixed common +residue modulo eight, and their midpoint is that residue plus four modulo +eight. By full column rank, M sends distinct midpoints to distinct vectors. +Two full cells already contradict y+Mc=0 for both. Hence H_*>2. + +This argument excludes every output, not just the attaining output below. +It concerns a full 4096-point fiber, not every smaller collision set. + +## Upper bound by a literal output + +The 112-entry vector y in WITNESS.json satisfies the exact integer identities + + y_i in {-4,0,4}, M^T y = 0, y + 2 M 1 = 0 modulo 8. (1) + +The verifier checks all entries of (1). This vector is new witness data; +the old sufficient-radius construction is not replayed. + +Take all q in {-6,-2,2,6}^8 for which y+Mq is divisible by eight. The +quotient q=2*1 satisfies this congruence. By premise 2 the other solutions +are obtained by q=2*1+4v with v modulo two in C. Each permitted parity +class has two choices in each coordinate. Thus there are exactly + + |C| 2^8 = 16 * 256 = 4096 + +solutions. Their reconstructed inputs are distinct because M is injective. +Equation (1) gives M^T x=7q. Therefore the actual forward quotient is + + R(8 M^T x / 52) = R(14q/13) = q, + +since |q_j|<=6 and |14q_j/13-q_j|<=6/13<1/2. There are no rounding ties. +Every reconstructed input maps to y under the literal forward map. + +Finally, |(Mq)_i|<=24 and |y_i|<=4, so |y_i+(Mq)_i|<=28. These numerators +are divisible by eight, so their absolute values are at most 24. Every +input therefore has ||x||_infinity<=3. This proves H_*<=3. + +For completeness, all preimages of this particular y have been included. +Since s=0, the scalar rounding inequality forces |q_j|<=6. Its lattice +congruence and the particular solution 2*1 force q_j=2 modulo four. The +only possibilities are exactly {-6,-2,2,6}. No larger quotient is omitted. +Together with the lower bound, H_*=3. + +## Verification and scope + +verify.py enumerates all 4^8 quotient tuples, tests the congruence, reconstructs +every accepted integer input, and evaluates F literally. It independently +counts distinct inputs, their radii, sixteen Cartesian cells and every +owner interval. The all-output lower bound is the written midpoint proof; +enumerating one fiber alone would not establish minimality. + +This settles one finite-range threshold of PR5444. It proves no native +implementation, reversible codec cost, physical owner access, full supplier +invoice, new kappa or complete multiplication theorem. Independent human +and formal proof-kernel review are unclaimed. diff --git a/research/rounded-native-fiber-radius/README.md b/research/rounded-native-fiber-radius/README.md new file mode 100644 index 0000000000..beb180409d --- /dev/null +++ b/research/rounded-native-fiber-radius/README.md @@ -0,0 +1,123 @@ +# A full rounded-native fiber already fits at radius three + +This contribution was produced by Nick Petalas. Apache-2.0. + +Scoped written proof with an exact finite certificate. For the fixed +112-owner rounded inverse of zxv's [PR5444](https://github.com/CrocSwap/integer-mult-bounds/pull/5444) +at three relative output bits, the least integer H admitting a full +4096-preimage fiber inside [-H,H]^112 is exactly **three**. The predecessor +gives radius sixteen as sufficient and explicitly leaves the finite-range +threshold open. The new result supplies a smaller attaining output and an +all-output lower bound. No new kappa is claimed. + + F(x) = 8x - M round_away(8 M^T x / 52), x in Z^112 + maximum fiber: 4096 inputs + minimum radius of a box containing such a fiber: 3 + +[PROOF.md](PROOF.md) proves that radius two is impossible: a maximal fiber +has sixteen full quotient cells, each inducing a width-four interval in +every owner. A radius-two box would force all cell midpoints to zero, +contradicting the injectivity of M on distinct quotient midpoints. + +[WITNESS.json](WITNESS.json) gives a literal output y with entries 0,+4,-4, +M^T y=0 and y+2M1 divisible by eight. Its complete quotient set lies in +{-6,-2,2,6}^8. All 4096 reconstructed inputs have magnitude at most three. +Their exact radius counts are 16 at radius one, 1055 at radius two and +3025 at radius three. These counts concern this particular fiber, not +maxima over smaller input boxes. + +## Reproduce + +From the repository root, using standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rounded-native-fiber-radius/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/rounded-native-fiber-radius/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rounded-native-fiber-radius +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rounded-native-fiber-radius --check-source-history +``` + +Another CPython 3.12 executable may replace the local interpreter path. +Expected markers are PASS_ROUNDED_NATIVE_FIBER_RADIUS, +PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES. +Every registered command has a 120-second timeout. The direct verifier +also runs from the eight-file package without Git, network or predecessors. +It writes no files. Its stdout receipt is generated and binds every +package file by SHA256; no receipt is handwritten. + +The checker enumerates all 65536 candidate quotient tuples, checks every +accepted input with a literal forward map, counts distinct inputs and +checks all sixteen 256-point Cartesian cells and their owner midpoints. +Fifteen boundary, rejection and changed-scale controls remain active under +optimized execution. The all-output minimality claim rests on the written +proof; one finite fiber alone would not establish it. + +## Scope, sources and credit + +Base is canonical main 2485805a6d47f36ea83ddde6327d453ac82d44dc, priority +revision eight. The selected source-binding orientation passes; it is not +a selected scientific replay. The selected conditional kappa .003125804 +and all five inherited framework assumptions are unchanged. + +The uniform-transfer-audit card is explicitly changed to this original +finite-range precision/erasure side result in [TASK.json](TASK.json). +It does not discharge a selected assumption or change an actual caller. +[Advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294731). +Live open PRs, recent account contributions, handoffs, active Discussions, +local reservations, main README terms and distinctive merged searches were +checked. Sparse notes, arbitrary historical diffs and unpublished work remain +coverage limits. Empty searches are not proof of novelty. + +Credit zxv for PR5444's fiber geometry, source lattice and code calculation, +relative-precision maximum and explicit finite-range question. Credit +Ali Romman/PR5323 for the same-grid recovery theorem, David Ganz/PR4929 +and Dillon Amburgey/PR4933 for the fixed native matrix/geometry, Brian/PR5035 +for the rounded kernel, and the retained native/controller/precision lineage. +Classical lattice, coding and rounding facts retain their classical status. +The new contribution is the minimum radius, midpoint exclusion and output +witness. MATRIX.json is an exact copy of the predecessor fixture; its bytes +and predecessor proof texts are pinned as provenance in SOURCES.json. +No predecessor scientific verifier or complete workload is imported or run. + +PR6182 concerns fixed coordinate-parity recovery tags at four relative bits. +That tag interface is separate from this finite-range threshold question; +no counterpart tag count or altered-precision tag theorem is targeted here. + +## Limits + +The result uses the exact fixed matrix, origin-centered coordinate box, +integer inputs and half-away rounding. It does not classify smaller fibers, +other precision levels, repeated maps or restricted physical input sets. +Native realization, reversible recovery cost, source access, restoration, +precision/tape/stock costs and a favorable complete supplier invoice remain +open. No full multiplier, independent human review or formal proof-kernel +acceptance is claimed. Lean, Docker and the selected cold replay are unrun. + +## Open next questions + +- Determine a finite-range threshold for another row of PR5444's table. + Begin with its equality geometry; no other precision is analyzed here. +- Bind this obstruction to one actual recovery site, including its lattice, + permitted values and observations. That caller and its complete bill + are the missing step toward a physical implication. + +TASK.json records relevance, first steps and blockers for these questions. + +## Code constraints + +The verifier has no recursion, subprocess, network, dynamic imports or output +file path. Functions are below sixty lines. Fixed dimensions bound all loops: +65536 quotient tuples, at most 4096 input vectors, sixteen cells with 256 +members, 112 owners with four entries and eight modes. Each file read is +capped at one MiB. Explicit exceptions enforce invariants under -O. + +Power of Ten rule 3 deviation: CPython allocates managed integers and +containers while checking. Scope is this fixed one-shot verifier. At most +4096 input vectors of 112 small coordinates and 4096 eight-coordinate +quotients are retained, with bounded JSON serialization and eight capped +file reads. Normal and optimized checks exercise these capacities. A future +embedded or unbounded-input implementation needs a separate allocation model. +Rule 9 deviation: six rejecting controls use callbacks with only the named +local validation functions as targets. No external dispatch is allowed. +Warning-strict normal/optimized replay and in-memory compilation supply +diagnostics; no external type checker or linter is installed in this environment. diff --git a/research/rounded-native-fiber-radius/SOURCES.json b/research/rounded-native-fiber-radius/SOURCES.json new file mode 100644 index 0000000000..2223356d1b --- /dev/null +++ b/research/rounded-native-fiber-radius/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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/precision-state-frontier/FIXTURE.json", + "usage": "provenance", + "git_blob": "0aa9f7816378c3eb11ec2e3d63ed9e85cfaa893c", + "sha256": "2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8" + }, + { + "path": "research/precision-state-frontier/README.md", + "usage": "provenance", + "git_blob": "9c21dc65e529bc234ddafc8683f311185b644c01", + "sha256": "0a62a71cea7e8ec40cf1a175b84b2d42cd81a3d94c7ab106ea7d6c765d75d8d2" + }, + { + "path": "research/precision-state-frontier/PROOF.md", + "usage": "provenance", + "git_blob": "79090050d47de95750b7321d89848143cc945abe", + "sha256": "f7e4d410cc108bc8b148ed8641c09be20c4c864fbc3908c533fa889b59dae341" + } + ] +} diff --git a/research/rounded-native-fiber-radius/TASK.json b/research/rounded-native-fiber-radius/TASK.json new file mode 100644 index 0000000000..300409e931 --- /dev/null +++ b/research/rounded-native-fiber-radius/TASK.json @@ -0,0 +1,112 @@ +{ + "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": "Exact minimum integer input radius for a full 4096-preimage fiber of the fixed PR5444 112-owner rounded inverse at three relative output bits.", + "scope_change_reason": "The selected-assumption audit card is changed to a new finite-range recovery theorem answering PR5444\u2019s explicit open finite-range threshold question. No predecessor audit, selected caller admission or discharge of a framework assumption is claimed.", + "bottleneck_link": "Precision/erasure side result: the maximum twelve-bit recovery information loss already occurs at input magnitude three. Bounded small inputs cannot dismiss that loss without a more specific caller restriction. Physical encoding, erasure and the full invoice are separate.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact threshold and its witness. Do not extend to other precisions, frames, tag interfaces or physical implementations.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-output radius-two exclusion and radius-three construction. verify.py enumerates all 65536 quotient candidates, reconstructs all 4096 inputs and checks every literal forward image and full-cell midpoint.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What are the exact finite-range thresholds at the other relative precisions in PR5444?", + "why_it_matters": "Worst-case recovery information can depend on the actual caller\u2019s magnitude range.", + "first_step": "Derive the equality geometry for one other row of the predecessor table and price any changed input contract.", + "blocked_by": "No other precision or caller range is analyzed here." + }, + { + "question": "Can a physical caller exploit or avoid the radius-three fiber under its actual input restrictions?", + "why_it_matters": "This determines whether the information obstruction applies to one real recovery/erasure site.", + "first_step": "Bind one site\u2019s lattice, permitted values, observations and restored outputs to the fixed map.", + "blocked_by": "A source-bound caller restriction and complete physical bill are absent." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294731", + "claim_type": "scoped proof with exact finite certificate", + "source_question": { + "source": "PR #5444", + "author": "zxv", + "question": "Finite-range frontier: smallest H attaining a chosen row of the precision-state table." + }, + "environment": { + "interpreter": "3.12.15", + "interpreter_path": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only at replay" + }, + "prior_state": { + "branch": "research/w4-1030a-helper-frontier", + "commit": "77ac6bd8dd9ea2db9024351956edec3f7152d9b1", + "preserved": true + }, + "upstream_checkpoint": { + "commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "priority_revision": 8, + "utc": "2026-10-30T13:45:00Z" + } +} diff --git a/research/rounded-native-fiber-radius/VERIFY.json b/research/rounded-native-fiber-radius/VERIFY.json new file mode 100644 index 0000000000..cd58dff758 --- /dev/null +++ b/research/rounded-native-fiber-radius/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 full-fiber enumeration, literal forward map, radius, Cartesian cell midpoints, source matrix bytes and semantic/boundary controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact full-fiber enumeration, literal forward map, radius, Cartesian cell midpoints, source matrix bytes and semantic/boundary controls." + } + ] +} diff --git a/research/rounded-native-fiber-radius/WITNESS.json b/research/rounded-native-fiber-radius/WITNESS.json new file mode 100644 index 0000000000..3893d17a89 --- /dev/null +++ b/research/rounded-native-fiber-radius/WITNESS.json @@ -0,0 +1,117 @@ +{ + "schema": "rounded-native-radius-witness-v1", + "output": [ + 0, + 0, + 0, + 0, + 0, + -4, + 0, + 0, + 0, + 0, + 0, + -4, + 4, + -4, + -4, + 0, + -4, + 4, + -4, + 0, + -4, + 0, + 4, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -4, + -4, + -4, + 4, + 0, + -4, + -4, + 0, + -4, + -4, + 0, + -4, + 0, + 0, + -4, + -4, + -4, + 0, + -4, + 4, + 0, + -4, + -4, + 0, + 4, + 0, + 0, + 0, + 0, + 0, + -4, + 0, + 0, + -4, + 0, + -4, + -4, + 0, + 0, + -4, + 0, + 4, + 4, + 0, + -4, + 4, + 4, + 0, + 0, + -4, + -4, + -4, + 4, + -4, + 0, + 0, + -4, + 4, + -4, + 4, + 4, + 0, + 4, + 4, + -4, + -4, + -4, + 0, + 0, + 0, + 0, + 0, + -4, + 0, + 0, + 0, + 4, + 0, + 0, + 4, + 0, + -4 + ] +} diff --git a/research/rounded-native-fiber-radius/verify.py b/research/rounded-native-fiber-radius/verify.py new file mode 100644 index 0000000000..3cc036a82e --- /dev/null +++ b/research/rounded-native-fiber-radius/verify.py @@ -0,0 +1,186 @@ +"""Exact finite certificate for the minimum full-fiber input radius.""" + +import hashlib +import itertools +import json +from collections import Counter +from pathlib import Path + + +ROOT = Path(__file__).resolve().parent +FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "MATRIX.json", "WITNESS.json", "verify.py") + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def read_bytes(name: str) -> bytes: + with (ROOT / name).open("rb") as stream: + data = stream.read(1024 * 1024 + 1) + require(len(data) <= 1024 * 1024, "file capacity exceeded") + return data + + +def load_matrix() -> tuple: + raw = read_bytes("MATRIX.json") + sources = json.loads(read_bytes("SOURCES.json")) + pins = [row for row in sources["files"] + if row["path"] == "research/precision-state-frontier/FIXTURE.json"] + require(len(pins) == 1, "unique predecessor matrix pin required") + require(hashlib.sha256(raw).hexdigest() == pins[0]["sha256"], "matrix source drift") + columns = json.loads(raw)["mode_columns"] + require(len(columns) == 8 and all(len(c) == 112 for c in columns), "matrix shape") + require(all(type(a) is int and a in (-1, 0, 1) + for c in columns for a in c), "signed matrix entries") + rows = tuple(tuple((j, columns[j][i]) for j in range(8) if columns[j][i]) + for i in range(112)) + require(all(len(row) == 4 for row in rows), "four signed entries per owner") + for j, k in itertools.product(range(8), repeat=2): + require(sum(columns[j][i] * columns[k][i] for i in range(112)) + == (56 if j == k else 0), "source Gram premise") + return rows + + +def apply_matrix(rows: tuple, q: tuple) -> tuple: + require(len(q) == 8, "eight quotient coordinates required") + return tuple(sum(sign * q[j] for j, sign in row) for row in rows) + + +def transpose(rows: tuple, x: tuple) -> tuple: + require(len(x) == 112, "112 owner coordinates required") + result = [0] * 8 + for row, value in zip(rows, x, strict=True): + for j, sign in row: + result[j] += sign * value + return tuple(result) + + +def nearest_away(numerator: int, denominator: int) -> int: + require(type(numerator) is int and type(denominator) is int + and denominator > 0, "integer ratio with positive denominator required") + magnitude = (2 * abs(numerator) + denominator) // (2 * denominator) + return magnitude if numerator >= 0 else -magnitude + + +def forward(rows: tuple, x: tuple, scale: int = 8) -> tuple: + q = tuple(nearest_away(scale * a, 52) for a in transpose(rows, x)) + correction = apply_matrix(rows, q) + return tuple(scale * a - b for a, b in zip(x, correction, strict=True)) + + +def validate_output(rows: tuple, output: tuple) -> None: + require(len(output) == 112 and all(type(a) is int for a in output), "output shape") + require(all(a in (-4, 0, 4) for a in output), "output amplitude") + require(transpose(rows, output) == (0,) * 8, "output must be perpendicular") + offset = apply_matrix(rows, (2,) * 8) + require(all((a + b) % 8 == 0 for a, b in zip(output, offset, strict=True)), + "quotient residue must be two modulo four") + + +def enumerate_fiber(rows: tuple, output: tuple) -> tuple: + validate_output(rows, output) + points, cells, radii = set(), {}, Counter() + candidates = 0 + for q in itertools.product((-6, -2, 2, 6), repeat=8): + candidates += 1 + correction = apply_matrix(rows, q) + fine = tuple(a + b for a, b in zip(output, correction, strict=True)) + if any(a % 8 for a in fine): + continue + x = tuple(a // 8 for a in fine) + require(forward(rows, x) == output, "literal forward map disagrees") + require(max(map(abs, x)) <= 3, "radius-three certificate failed") + require(x not in points, "duplicate input") + points.add(x) + key = tuple(((a + 6) // 4) % 2 for a in q) + cells.setdefault(key, []).append((q, x)) + radii[max(map(abs, x))] += 1 + require(len(points) == 4096 and len(cells) == 16, "full-fiber cardinality") + return points, cells, radii, candidates + + +def check_cells(rows: tuple, output: tuple, cells: dict) -> int: + centers = set() + for members in cells.values(): + require(len(members) == 256, "full binary quotient cell required") + choices = [sorted({q[j] for q, _ in members}) for j in range(8)] + require(all(len(c) == 2 and c[1] - c[0] == 8 for c in choices), + "cell side length eight required") + center = tuple((c[0] + c[1]) // 2 for c in choices) + centers.add(center) + image = apply_matrix(rows, center) + for i in range(112): + lo = min(x[i] for _, x in members) + hi = max(x[i] for _, x in members) + require(hi - lo == 4, "owner interval must have width four") + require(4 * (lo + hi) == output[i] + image[i], "cell midpoint identity") + require(len(centers) == 16, "different parity cells have different midpoints") + return len(centers) + + +def reject(call, message: str) -> None: + try: + call() + except ValueError: + return + raise ValueError(message) + + +def controls(rows: tuple, output: tuple, points: set) -> int: + count = 0 + for n, d, want in ((1, 2, 1), (-1, 2, -1), (3, 2, 2), (-3, 2, -2), + (25, 52, 0), (-25, 52, 0), (26, 52, 1), (-26, 52, -1)): + require(nearest_away(n, d) == want, "rounding boundary control") + count += 1 + changed = list(output) + changed[0] += 4 + reject(lambda: validate_output(rows, tuple(changed)), "changed output accepted") + count += 1 + reject(lambda: validate_output(rows, (0,) * 112), "wrong residue accepted") + count += 1 + reject(lambda: validate_output(rows, output[:-1]), "short output accepted") + count += 1 + reject(lambda: nearest_away(1, 0), "zero denominator accepted") + count += 1 + reject(lambda: nearest_away(True, 2), "Boolean numerator accepted") + count += 1 + radius_three = next(x for x in points if max(map(abs, x)) == 3) + reject(lambda: require(max(map(abs, radius_three)) <= 2, "radius two"), + "false radius accepted") + count += 1 + require(any(forward(rows, x, 4) != output for x in points), "wrong scale survived") + return count + 1 + + +def main() -> None: + rows = load_matrix() + witness = json.loads(read_bytes("WITNESS.json")) + output = tuple(witness["output"]) + points, cells, radii, candidates = enumerate_fiber(rows, output) + cell_count = check_cells(rows, output, cells) + control_count = controls(rows, output, points) + ordered = sorted(points) + receipt = { + "status": "PASS_ROUNDED_NATIVE_FIBER_RADIUS", + "claim_type": "scoped proof with exact finite certificate", + "minimum_integer_radius": 3, + "quotient_candidates": candidates, + "distinct_preimages": len(points), + "radius_histogram": dict(sorted(radii.items())), + "full_parity_cells": cell_count, + "inputs_per_cell": 256, + "controls": control_count, + "input_set_sha256": hashlib.sha256(json.dumps(ordered, separators=(",", ":")) + .encode()).hexdigest(), + "package_sha256": {name: hashlib.sha256(read_bytes(name)).hexdigest() + for name in FILES}, + "no_new_kappa": True, + } + print(json.dumps(receipt, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()