Prove the exact radius-three full recovery fiber threshold (no κ)

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.

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.

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"
+    }
+  ]
+}