Prove exact nearest-even shear history from binary code weight

research/nearest-even-shear-history/README.md

@@ -0,0 +1,174 @@
+# Exact history for nearest-even rounded shears
+
+For a fixed rational matrix A, retain the integer source x and return
+`z = R(y + A*x)`, where y is an arbitrary independent integer destination and
+R rounds each whole sum to its nearest integer, breaking half ties toward the
+even integer. The minimum fixed binary history needed to reconstruct every y
+is exactly
+
+```
+tau(A) = max over integer x of #{i : (A*x)_i is a half integer}.
+```
+
+A half integer means an integer plus 1/2. For `A = B/2` with B integral, tau
+is the maximum Hamming weight in the binary linear code `im(B mod 2)`.
+Even rational and binary rank one can require arbitrarily many history bits.
+This is a scoped mathematical proof with exact finite corroboration, with no
+physical history circuit, completed native child or new kappa.
+
+## Contract and quantified result
+
+Let A have m rows and n columns, with m,n positive and finite. Its coefficients
+are fixed rationals. The map is
+
+`F_A : Z^n x Z^m -> Z^n x Z^m, (x,y) -> (x,R(y+A*x))`.
+
+There is no overflow, saturation, variable grid or hidden transcript. The
+decoder knows A and the retained source x. A history is an extra value from
+one fixed finite alphabet, and may depend on both x and y. All additional
+input-dependent metadata counts as history. The guarantee is worst case,
+without an average-length or input-distribution assumption.
+
+For fixed x, write t(x) for its number of half-integer coordinates. Every
+nonempty fiber over `(x,z)` has exactly `2^t(x)` elements. The smallest sufficient
+history alphabet therefore has exactly `2^tau(A)` values. The smallest fixed
+bit budget is tau(A), attained by the explicit decoder below. This is an
+injective encoding statement, not a reversible machine on a full dirty
+auxiliary state space.
+
+F_A itself is a bijection exactly when every reduced denominator of every
+entry of A is odd. Thus an integral dyadic A needs no history, while every
+nonintegral dyadic A loses some information on the full entrance grid. A common
+absolute grid precision does not change this statement after rescaling to
+integer units, with the same unrestricted source and destination contract.
+
+## Proof
+
+Fix a scalar offset a. Away from half integers there is a unique nearest
+integer, so `R(y+a)=y+R(a)` for all integer y. This coordinate is a bijective
+integer translation.
+
+If `a=k+1/2`, only even output integers z are possible. Each such z has exactly
+the two preimages `y=z-k-1` and `y=z-k`. Their unrounded sums are z-1/2 and
+z+1/2, which both round to the even integer z. No other integer y is within
+distance 1/2. Destination coordinates are independent once x is retained.
+Multiplying coordinate fiber sizes proves the exact `2^t(x)` statement.
+
+Let D be the least common multiple of all reduced entry denominators. Changing
+x by D times an integer vector changes A*x by an integer vector, preserving
+its half-integer positions. Thus tau(A) is attained on `(Z/DZ)^n`. A nonempty
+fiber at a maximizing source has `2^tau(A)` elements, which fewer history
+values cannot distinguish, by the pigeonhole principle.
+
+For the matching upper bound, enumerate the half-integer coordinates in row
+order. At offset `k_i+1/2`, store the bit `b_i=y_i-(z_i-k_i-1)`. The decoder
+returns `z_i-k_i-1+b_i`. At every other coordinate it returns
+`z_i-R((A*x)_i)`. The retained source identifies the tie coordinates, so no
+tie-location transcript is needed. Pack the t(x) bits in the low positions
+of a tau(A)-bit history and pad the unused bits with zero. This reconstructs
+every signed integer destination.
+
+For the bijectivity classification, a sum of rationals with odd denominators
+still has odd reduced denominator and cannot be a half integer. Conversely,
+choose a row whose least common denominator d is even, and write it as
+`(b_1,...,b_n)/d`. Minimality of d gives `gcd(d,b_1,...,b_n)=1`. Bezout's
+identity supplies an integer vector x with `sum b_j*x_j = d/2 mod d`.
+That row then has a half-integer offset. Hence tau is zero exactly for
+odd-denominator matrices. When tau is zero, every source fiber is a bijective
+translation; otherwise F_A has a collision.
+
+Finally, if `A=B/2`, a coordinate is a half integer exactly when the corresponding
+coordinate of `B*x mod 2` is one. Every binary source residue occurs, proving
+the maximum-codeword-weight formula.
+
+## Sharp consequences
+
+For m copies of the single coefficient 1/2, x=1 makes every coordinate a tie.
+The rational and binary ranks are both one, yet the fiber at the all-zero
+output contains every `y in {-1,0}^m`. Exactly m history bits are necessary
+and sufficient for every m>=1.
+
+Rank also fails to determine the answer with dimensions fixed. The matrices
+`B0=[[1,0],[1,1],[0,1]]` and `B1=[[1,0],[0,1],[0,1]]` both have rational and
+binary rank two. The image weights of B0 are zero or two; B1 attains weight
+three. Thus `tau(B0/2)=2` and `tau(B1/2)=3`.
+
+## Reproduction and evidence
+
+From the repository root, use CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/nearest-even-shear-history/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/nearest-even-shear-history
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/nearest-even-shear-history --check-source-history
+```
+
+Both VERIFY.json commands are timed by the package runner. One enables isolated
+optimized execution. All semantic checks remain active without assertions.
+The direct verifier prints a generated JSON receipt with the hashes of all five
+package files and writes nothing into the checkout. The written proof establishes
+the unbounded theorem; finite enumeration corroborates it.
+
+The independent literal oracle minimizes exact rational distance and breaks
+ties by parity. The encoder instead uses an integer-division rounder. Destination
+residues modulo two give a complete finite fiber oracle because
+`R(v+2)=R(v)+2`. All source residues modulo the exact denominator are enumerated.
+
+CPython 3.12.15 checks 682 binary matrices, with 5,003 source cases and 37,294
+literal destination cases; 668 rational fixtures, with 12,891 source cases and
+50,128 literal destination cases; 38,759 signed exact history round trips; and
+13 malformed-input/history/image rejections. The binary domain contains every
+matrix of each shape from 1-by-1 through 3-by-3. Rational fixtures include a
+signed scalar menu, a complete mixed-denominator 2-by-2 menu and all 2-by-2
+quarter-integral matrices with numerators zero through three. Rational fixtures
+may repeat equal reduced coefficients. Additional controls check signed half
+ties, the eight-element rank-one fiber, and increment/whole-sum distinctions.
+
+The replay API caps matrices at eight rows and six columns and each periodic
+corroboration at 4,096 source residues. All loops have finite fixture/dimension
+bounds. There is no recursion. Python/Fraction allocation is a managed-runtime
+deviation from fixed-memory rules; the live fiber Counter has at most 256
+entries. Every function is under 60 lines. Explicit invariant checks remain
+enabled with optimization. Warnings-as-errors run in both registered commands;
+no additional static analyzer is configured for this package.
+
+## Sources, scope and credit
+
+This contribution was produced by Nick Petalas. Independent human and formal
+proof-kernel review are unclaimed. New work is Apache-2.0.
+
+Ali Romman's [PR #5838](https://github.com/CrocSwap/integer-mult-bounds/pull/5838),
+head `a7fe04425abb083842686f29c54ca0fed6252d31`, distinguishes independently
+adverse completed defects from an actual rounder with stronger correlations.
+Its open question motivates this deterministic side result. Its error numbers
+and source word are not replayed or newly claimed. SOURCES.json records the
+exact README blob and SHA256 used as question context.
+
+ywz65's [PR #2555](https://github.com/CrocSwap/integer-mult-bounds/pull/2555)
+already gives a scalar whole-sum tie collision and the distinct positive
+increment-rounding translation contract. Its unchanged README is pinned as
+historical provenance. Rounding's general information loss, the pigeonhole
+principle, Bezout's identity and binary linear codes are standard facts.
+The new result is the exact rational-shear fiber/history classification,
+its attaining encoding and the maximum-codeword-weight specialization.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216882)
+records the question. The original `joint-query-controller` card is explicitly
+changed to this local arithmetic/cleanup theorem. Neither predecessor verifier
+is imported. Source context is provenance, not a live computational dependency.
+
+No history lifetime, physical register count, instruction count or reversible
+uncomputation cost is proved. Restricted reachable inputs, different tie rules,
+round-the-increment updates, extra retained outputs or discarded sources change
+the contract. No full P104 word, native recipe, rounded supplier, selected cold
+replay, compiler, tapes, Lean, outer arithmetic or complete multiplication
+theorem has been implemented or verified. The five selected assumptions remain.
+
+## Open next questions
+
+Can one actual completed P104 child retain and uncompute its required tie
+history within its complete physical bill? The encoding alone does not supply
+a zero-return native workspace. First freeze the actual rounding sites,
+entrance lattice and returned fields of one child, derive its fibers, then
+price a history lifecycle. The missing completed physical child and history
+restoration machine block that step. Structured details are in TASK.json.

research/nearest-even-shear-history/SOURCES.json

@@ -0,0 +1,33 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/dirty-prefix-full-grid/README.md",
+      "usage": "provenance",
+      "git_blob": "083fc7dc64ac554703d215f3de2923bd187bb81a",
+      "sha256": "409f8ab4d70d52fe1422f3a85c76482729535d6fe57bdf45a78e868a6ec45a00"
+    }
+  ],
+  "question_source": {
+    "pull_request": 5838,
+    "author": "Ali Romman",
+    "head": "a7fe04425abb083842686f29c54ca0fed6252d31",
+    "path": "research/p104-gauge-error-covariance/README.md",
+    "git_blob": "6e32f5c58c390d32fa2d72f1bf72fcdf2151d4d6",
+    "sha256": "0c621274810b65505f86f574efabf2568f8fca74a509af9129b55173451bdadd",
+    "usage": "Question and model context only; no executable or numerical result imported."
+  }
+}

research/nearest-even-shear-history/TASK.json

@@ -0,0 +1,104 @@
+{
+  "schema_version": 1,
+  "task_id": "joint-query-controller",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "joint-query-controller",
+    "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?",
+    "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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "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 an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.",
+    "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": [
+      "query demand",
+      "active mode",
+      "5720",
+      "5745",
+      "5747",
+      "caller"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.",
+        "evidence": "research/qq16-caller-install/README.md",
+        "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.",
+        "status": "author-checked",
+        "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630",
+        "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 the exact minimum fixed history for whole-sum nearest-even rational shears on arbitrary integer grids, including the half-integral binary-code formula.",
+  "scope_change_reason": "The card concerns a completed caller. PR5838 explicitly leaves deterministic rounding correlations open. This side result isolates the information that this concrete rounded primitive loses before any native/caller construction.",
+  "bottleneck_link": "An actual deterministic rounded child must preserve enough information for its required inverse/cleanup. A local relative-error bound does not certify injectivity. This is a necessary information contract, not an improved supplier.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved sharp history theorem and independently enumerated corroboration; do not extend into native or full-word construction.",
+  "outcome": "completed",
+  "evidence": "README.md contains the quantified proof and attaining encoding; verify.py enumerates complete small fibers and independently reconstructs signed inputs.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can one actual completed P104 child retain and uncompute the required tie history within its complete physical bill?",
+      "why_it_matters": "The information encoding alone does not implement a reversible native child or zero-return workspace.",
+      "first_step": "Freeze one physical child, its actual rounding sites, entrance lattice and retained output; derive its fibers before adding a history lifecycle.",
+      "blocked_by": "No physical completed child or history-restoration machine is supplied here."
+    }
+  ],
+  "question_source": {
+    "pull_request": 5838,
+    "author": "Ali Romman",
+    "head": "a7fe04425abb083842686f29c54ca0fed6252d31",
+    "path": "research/p104-gauge-error-covariance/README.md",
+    "git_blob": "6e32f5c58c390d32fa2d72f1bf72fcdf2151d4d6",
+    "sha256": "0c621274810b65505f86f574efabf2568f8fca74a509af9129b55173451bdadd",
+    "usage": "Question and model context only; no executable or numerical result imported."
+  },
+  "overlap_coverage": {
+    "canonical_main": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+    "priority_revision": 8,
+    "own_prs": 200,
+    "open_prs_initial": 100,
+    "helper_open_prs": 459,
+    "helper_discussion_records": 5402,
+    "helper_local_notes_searched": 200,
+    "helper_local_notes_omitted": 7645,
+    "limits": "Targeted merged/readme searches and live PR bodies are bounded; unpublished work, all diffs and all historical PRs are not exhaustively searched."
+  }
+}

research/nearest-even-shear-history/VERIFY.json

@@ -0,0 +1,33 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete small rational/binary fibers, code-weight identity, signed history inverse and rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same exact finite coverage with optimization, isolation and warnings as errors."
+    }
+  ]
+}