Relax QQ16 producer tolerance by one bit (no κ)

research/qq16-producer-one-bit-feedback/PROOF.md

@@ -0,0 +1,115 @@
+# A sufficient common offset of 101
+
+## Contract and cited premises
+
+Fix the literal QQ16 F0 then B_1_2 words and the completed-operation
+contracts in commdata2338's [PR3235 envelope](../qq16-rounded-producer-envelope/README.md).
+Original data have norm at most H>0, persistent dirty helpers have norm at
+most `2^delta H`, and beta, delta are nonnegative integers. The norm is the
+maximum owner payload Hilbert norm, then the maximum over fields. Native
+children, adapters and cover maps obey the cited isometry and destination
+contracts. ADD/SCALE defects use the cited actual-operand relative bounds.
+Owned private CLEARs are exact and precede every private read. Additional
+inexact handoff operations are not covered by this contract.
+
+We use the predecessor's nonnegative path-polynomial envelope and its
+published ledger as premises. They are not new measurements or replays:
+
+```text
+F0: N_F = 26057,  J_F = 10632335516156845470267 / 4096
+B1: N_B = 26977,  J_B = 34778728470688788237067911 / 8.
+```
+
+For an entry bound A, each initialized field has a polynomial q with
+nonnegative rational coefficients and degree at most N. Its ideal/actual
+error is bounded by `A [q(1+u)-q(1)]`. At every relevant cut,
+`q'(1) <= J_F` or `J_B`. The same ledger bounds completed data and helper
+outputs. F0's ideal data endpoint has norm at most 58H, independently of
+dirty helper values, and its ideal helpers return isometrically. These are
+also cited PR3235 premises. B1's ideal data endpoint is independent of its
+arbitrary helper inputs. The proof below is conditional on these premises.
+
+## Smaller feedback factor
+
+For 1 <= n <= N and u >= 0,
+
+```text
+(1+u)^n - 1 = u sum_(j=0)^(n-1) (1+u)^j
+           <= n u (1+u)^(N-1).
+```
+
+If Nu<1, the binomial theorem and `binom(N,k) <= N^k` give
+
+```text
+(1+u)^(N-1) <= (1+u)^N <= sum_(k>=0) (Nu)^k = 1/(1-Nu).
+```
+
+Multiply the monomial inequalities by q's nonnegative coefficients and sum.
+The constant term contributes zero. Thus
+
+```text
+q(1+u)-q(1) <= u q'(1)/(1-Nu).
+```
+
+In particular, `Nu <= 1/17` implies an error bound `(17/16) A u J`.
+This retains feedback; replacing the factor by exactly one is generally
+false, as the polynomial `q(z)=z^2` shows for every u>0.
+
+## The new common tolerance
+
+Set `0 <= u <= 2^(-beta-delta-101)`. Since beta, delta >= 0 and
+`17*26977 < 2^101`, both stages satisfy `N u < 1/17`. The improved
+feedback estimate therefore applies to every permitted error pattern.
+
+For F0 take `A_F=2^delta H`. Its all-cut error divided by
+`eta_F=H 2^(-beta-8)` is at most
+
+```text
+r_F = (17/16) J_F 2^(8-101)
+    = 180749703774666372994539 / 649037107316853453566312041152512
+    < 1.
+```
+
+Consequently its actual completed data have norm at most `58H+eta_F` and
+its helpers have norm at most `2^delta H+eta_F`. With beta, delta >= 0,
+both are below `A_B=2^(delta+6)H`. This is a bound on actual B1 inputs,
+so correlated F0 helper errors are carried into the second stage.
+
+B1 is compared with its ideal map applied to that actual input. Divide
+its all-cut error bound by `eta_B=H 2^(-beta-13)` to obtain
+
+```text
+r_B = (17/16) 2^6 J_B 2^(13-101)
+    = 591238384001709400030154487 / 618970019642690137449562112
+    < 1.
+```
+
+The strict normalized slack is
+`27731635640980737419407625 / 618970019642690137449562112`.
+These exact inequalities prove the stated common tolerance for every
+beta, delta and H in the contract, not just the finite test parameters.
+The predecessor common offset is 102; the new sufficient tolerance is
+twice as large. No further guard optimization is claimed.
+
+## Decoder consequence and limits
+
+If the separate decoder implementation supplies
+`eps_D <= H 2^(-beta-1)`, Nick Petalas's cited
+[PR2965 transfer](../qq16-producer-defect-transfer/README.md) gives
+
+```text
+original-data error <= 49 eta_F + 1923 eta_B + eps_D
+                    <= (7587/8192) H 2^-beta < H 2^-beta.
+```
+
+The order is unchanged: B1's completed defect is relative to its actual
+F0 output. Neither cancellation of independent defects nor exact borrowed
+restoration is inferred. The result is a conditional numerical interface
+lemma, not an implementation of any native event, a finite register-width
+minimum, a complete multiplication theorem or supplier admission.
+
+The verifier authenticates the cited source bytes and checks the new
+arithmetic and finite controls. It neither recomputes the predecessor's
+path ledger nor audits its native semantics. A failed certificate at offset
+100 rejects only this particular sufficient bound, not that physical
+tolerance in every possible analysis or implementation.

research/qq16-producer-one-bit-feedback/README.md

@@ -0,0 +1,107 @@
+# One fewer guard bit for the bounded-dirty QQ16 producer
+
+For the literal QQ16 F0 followed by B_1_2 producer of
+[commdata2338's PR3235](https://github.com/CrocSwap/integer-mult-bounds/pull/3235),
+the common completed-operation relative tolerance
+
+```text
+u <= 2^(-beta-delta-101)
+```
+
+suffices for the same completed-stage allowances. The predecessor supplies
+the sufficient offset 102. This result doubles the permitted local defects,
+for every integer beta, delta >= 0, with the same bounded dirty inputs,
+destination-local error contracts, exact private CLEARs and native isometry
+premises. It changes no word or recursive invoice.
+
+Claim type: a scoped written proof conditional on the cited producer ledger,
+with exact rational corroboration. The new step retains the ledger's exact
+derivative values and bounds feedback by 17/16 instead of two.
+[PROOF.md](PROOF.md) gives the all-parameter argument and inherited premises.
+No minimum guard or physical accuracy implementation is asserted.
+
+## Exact margin
+
+After dividing the B1 error bound by its allowed `H 2^(-beta-13)`, the new
+upper bound is
+
+```text
+591238384001709400030154487 / 618970019642690137449562112 < 1.
+```
+
+The strict slack is
+`27731635640980737419407625 / 618970019642690137449562112`.
+This is a sufficient upper bound, not a realized rounding error. The decoder
+transfer, if separately implemented to its existing allowance, still gives
+the credited `7587/8192` original-input error ratio.
+
+## Reproduce
+
+From the repository root with standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/qq16-producer-one-bit-feedback/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/qq16-producer-one-bit-feedback/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/qq16-producer-one-bit-feedback
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/qq16-producer-one-bit-feedback --check-source-history
+```
+
+Any standard-library CPython 3.12 executable may replace the local path.
+The direct marker is `PASS_QQ16_PRODUCER_ONE_BIT_FEEDBACK`. Replay reads
+three authenticated predecessor files, imports no predecessor executable,
+checks the new rational implication and bounded polynomial/parameter controls,
+and prints a generated receipt bound to nine file hashes. It writes no files.
+The 100-bit rejection only shows that this fixed sufficient certificate
+cannot justify that stronger tolerance. It is not an impossibility theorem.
+
+## Scope and remaining obligations
+
+The predecessor derivative ledger and native/owner/sweep semantics are cited
+premises. They are not audited or recomputed here. The result permits all five
+declared defect categories and carries F0 helper errors into B1. It supplies
+neither finite component widths nor a native implementation achieving those
+defects. Exact borrowed-bit restoration, native interiors, grid/overflow,
+physical storage/movement, a paid F17 consumer and supplier admission remain
+open. No new kappa or selected-frontier change is claimed. The five framework
+assumptions retain their status. Independent human and formal proof-kernel
+review are unclaimed.
+
+The current joint-query-controller card is explicitly changed to this small
+producer-precision side theorem. It does not meet the card's complete physical
+caller gate. The first selected-baseline control passed at main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected PR6030.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363489)
+states the exact numerical target.
+
+## Open next questions
+
+1. Can one actual finite native child meet the enlarged destination-local
+   defect allowance, including all scratch effects? Begin at a literal child
+   followed by a half-ADD. The absent physical child implementation and its
+   tariff block a supplier consequence.
+2. Can a complete producer/decoder/consumer exploit the relaxed tolerance in
+   a priced format? Begin with a single reached grid/range contract, exact
+   helper return and every conversion charge. A relative tolerance exponent
+   alone does not determine a register width or recursive saving.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Credit commdata2338 / PR3235
+for the positive path-polynomial method as applied to the complete producer,
+the exact derivative ledger, operation contract and noisy-helper composition;
+Nick Petalas / PR2965 for the completed-output decoder transfer; Ali Romman
+and the joint-query team, ywz65 / PR2540 and PR2707, Arham Tahir / PR2681,
+and the retained native, geometry and supplier lineage. Positive majorants
+and elementary geometric-series estimates are classical. The new contribution
+is this source-bound one-bit sufficient guard improvement. Apache-2.0.
+
+## Verification bounds
+
+Power-of-Ten rule 3 deviation: Python allocates integer, Fraction, JSON and
+collection objects during verification. Each input is bounded to 2 MB; only
+five source rows, three live inputs, 243 coefficient vectors of length five,
+five tolerances per vector and 24 parameter cases are visited. No recursion,
+subprocess or unbounded work queue is used. The largest fixture exponent is
+127+64+101. The fixed capacities and read-only execution bound live work;
+this is not a physical-memory invoice. A native fixed-storage implementation
+would require its own representation and allocation proof.

research/qq16-producer-one-bit-feedback/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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/qq16-producer-defect-transfer/README.md",
+      "usage": "input",
+      "git_blob": "16903a0090c020d033d24712cce11c633031e688",
+      "sha256": "30cf4389425f7704b1ed45af6cf4b5165e7b5c04af5077640ac96399c61cd703"
+    },
+    {
+      "path": "research/qq16-rounded-producer-envelope/README.md",
+      "usage": "input",
+      "git_blob": "2624a443e21a53b63fbedfd3d602892c5f33b6aa",
+      "sha256": "7e45a72f4d5a160d4b62478259c6d6b664d22799e98b0dd997be75367636edac"
+    },
+    {
+      "path": "research/qq16-rounded-producer-envelope/RESULT.json",
+      "usage": "input",
+      "git_blob": "db80a6a402d933b49d940982f602048d836da733",
+      "sha256": "9f3a0ec4b18ce259e754318efa05a8a2f05c160f69f7c44b79d84f70edf8b963"
+    }
+  ]
+}

research/qq16-producer-one-bit-feedback/TASK.json

@@ -0,0 +1,102 @@
+{
+  "schema_version": 1,
+  "task_id": "joint-query-controller",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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": "A source-bound sufficient common completed-operation relative-defect offset of 101, replacing PR3235's 102, for its bounded-dirty QQ16 F0 then B_1_2 producer.",
+  "scope_change_reason": "The current card asks for changed query demand and a complete physical invoice. This contribution is explicitly a smaller producer-precision side theorem using the same cited word and native contracts; it does not satisfy that complete-supplier gate.",
+  "bottleneck_link": "A completed producer needs a numerical contract before a finite implementation can be priced. This result relaxes that contract by one bit while leaving native realization, exact borrowed return and the full caller invoice open.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified sufficient guard improvement; do not optimize a further guard or expand a physical construction.",
+  "outcome": "completed",
+  "evidence": "Written all-parameter proof conditional on PR3235's source-bound ledger; standalone exact rational certificate, polynomial feedback fixtures, noisy-entry parameter fixtures and rejecting controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can one actual finite native child meet the enlarged destination-local relative-defect allowance, including its scratch effects?",
+      "why_it_matters": "A sufficient numerical contract does not implement or price a native child.",
+      "first_step": "Bind a literal child followed by a half-ADD and retain every rounding and scratch side effect.",
+      "blocked_by": "No finite native implementation or complete tariff is supplied."
+    },
+    {
+      "question": "Can a complete producer/decoder/consumer exploit the relaxed tolerance in a priced format?",
+      "why_it_matters": "A one-bit tolerance change is not a register-width or recursive-invoice improvement.",
+      "first_step": "Fix a reached grid and range, exact helper return and all conversion charges.",
+      "blocked_by": "Physical layout, finite native contracts and an affordable consumer remain open."
+    }
+  ],
+  "source_question": {
+    "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/3235",
+    "author": "commdata2338",
+    "relation": "New sufficient-bound refinement of the cited numerical contract; not an audit or a claim to solve its physical child questions."
+  },
+  "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363489",
+  "upstream_checkpoint": {
+    "commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+    "priority_revision": 8,
+    "selected_pr": 6030,
+    "checked_at_utc": "2026-11-03T00:51:15.133669+00:00"
+  }
+}