From 609792665b5bcf0ffdb7cf91d2241b2f25bd8c14 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 00:53:42 +0000 Subject: [PATCH] feat(research): relax QQ16 producer tolerance by one bit --- .../qq16-producer-one-bit-feedback/PROOF.md | 115 ++++++++++++ .../qq16-producer-one-bit-feedback/README.md | 107 +++++++++++ .../SOURCES.json | 36 ++++ .../qq16-producer-one-bit-feedback/TASK.json | 102 +++++++++++ .../VERIFY.json | 38 ++++ .../qq16-producer-one-bit-feedback/verify.py | 171 ++++++++++++++++++ 6 files changed, 569 insertions(+) create mode 100644 research/qq16-producer-one-bit-feedback/PROOF.md create mode 100644 research/qq16-producer-one-bit-feedback/README.md create mode 100644 research/qq16-producer-one-bit-feedback/SOURCES.json create mode 100644 research/qq16-producer-one-bit-feedback/TASK.json create mode 100644 research/qq16-producer-one-bit-feedback/VERIFY.json create mode 100644 research/qq16-producer-one-bit-feedback/verify.py diff --git a/research/qq16-producer-one-bit-feedback/PROOF.md b/research/qq16-producer-one-bit-feedback/PROOF.md new file mode 100644 index 0000000000..3db5e5462d --- /dev/null +++ b/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. diff --git a/research/qq16-producer-one-bit-feedback/README.md b/research/qq16-producer-one-bit-feedback/README.md new file mode 100644 index 0000000000..e0bc073093 --- /dev/null +++ b/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. diff --git a/research/qq16-producer-one-bit-feedback/SOURCES.json b/research/qq16-producer-one-bit-feedback/SOURCES.json new file mode 100644 index 0000000000..1b35dd05a9 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/qq16-producer-one-bit-feedback/TASK.json b/research/qq16-producer-one-bit-feedback/TASK.json new file mode 100644 index 0000000000..bc575f04f2 --- /dev/null +++ b/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" + } +} diff --git a/research/qq16-producer-one-bit-feedback/VERIFY.json b/research/qq16-producer-one-bit-feedback/VERIFY.json new file mode 100644 index 0000000000..f592cc9c24 --- /dev/null +++ b/research/qq16-producer-one-bit-feedback/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/qq16-producer-defect-transfer/README.md", + "research/qq16-rounded-producer-envelope/README.md", + "research/qq16-rounded-producer-envelope/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "New guard-101 rational implication, bounded nonnegative-polynomial and parameter controls, source-byte and stronger-certificate rejection." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same complete new-implication checks with Python assertions disabled." + } + ] +} diff --git a/research/qq16-producer-one-bit-feedback/verify.py b/research/qq16-producer-one-bit-feedback/verify.py new file mode 100644 index 0000000000..3ae5e1ce45 --- /dev/null +++ b/research/qq16-producer-one-bit-feedback/verify.py @@ -0,0 +1,171 @@ +#!/usr/bin/env python3 +"""Check the new guard implication, taking PR3235's ledger as a premise.""" + +from fractions import Fraction +from hashlib import sha1, sha256 +from itertools import product +import json +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +MAX_BYTES = 2_000_000 +FACTOR = Fraction(17, 16) +INPUTS = ( + "research/qq16-producer-defect-transfer/README.md", + "research/qq16-rounded-producer-envelope/README.md", + "research/qq16-rounded-producer-envelope/RESULT.json", +) + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def read_bytes(path: Path) -> bytes: + require(path.is_file() and not path.is_symlink(), "expected regular file") + require(path.stat().st_size <= MAX_BYTES, "input exceeds byte limit") + with path.open("rb") as stream: + data = stream.read(MAX_BYTES + 1) + require(len(data) <= MAX_BYTES, "input grew beyond byte limit") + return data + + +def authenticate(data: bytes, row: dict) -> None: + require(sha256(data).hexdigest() == row["sha256"], "source SHA256 mismatch") + header = b"blob " + str(len(data)).encode("ascii") + b"\0" + require(sha1(header + data).hexdigest() == row["git_blob"], "source blob mismatch") + + +def source_inputs() -> tuple[dict, dict]: + manifest = json.loads(read_bytes(PACKAGE / "SOURCES.json")) + require(len(manifest["files"]) == 5, "unexpected source inventory") + rows = {row["path"]: row for row in manifest["files"] if row["usage"] == "input"} + require(set(rows) == set(INPUTS), "unexpected live inputs") + hashes = {} + ledger = None + for name in INPUTS: + data = read_bytes(ROOT / name) + authenticate(data, rows[name]) + hashes[name] = sha256(data).hexdigest() + if name.endswith("RESULT.json"): + ledger = json.loads(data) + require(ledger is not None, "missing derivative premise") + return ledger, hashes + + +def feedback_bound(coefficients: tuple, sites: int, tolerance: Fraction) -> Fraction: + require(type(sites) is int and 1 <= sites <= 8, "invalid fixture site count") + require(1 <= len(coefficients) <= sites + 1, "degree exceeds site bound") + require(all(type(c) is int and c >= 0 for c in coefficients), "negative coefficient") + require(tolerance >= 0 and sites * tolerance < 1, "invalid feedback tolerance") + derivative = sum(i * c for i, c in enumerate(coefficients)) + return tolerance * derivative / (1 - sites * tolerance) + + +def polynomial_controls() -> int: + count = 0 + for coefficients in product(range(3), repeat=5): + derivative = sum(i * c for i, c in enumerate(coefficients)) + for tolerance in (Fraction(0), Fraction(1, 68), Fraction(1, 136), + Fraction(1, 8), Fraction(1, 5)): + difference = sum(c * ((1 + tolerance) ** i - 1) + for i, c in enumerate(coefficients)) + require(difference <= feedback_bound(coefficients, 4, tolerance), + "geometric feedback inequality failed") + if 4 * tolerance <= Fraction(1, 17): + require(difference <= FACTOR * tolerance * derivative, + "17/16 feedback inequality failed") + count += 1 + tolerance = Fraction(1, 68) + require((1 + tolerance) ** 2 - 1 > 2 * tolerance, + "feedback-omission control did not distinguish the formulas") + return count + + +def guard_certificate(ledger: dict, guard: int) -> dict: + require(type(guard) is int and 1 <= guard <= 102, "invalid guard") + cases = ledger["cases"] + jf = Fraction(cases["F_0"]["all_cut"]["J"]["J"]) + jb = Fraction(cases["B_1_2"]["all_cut"]["J"]["J"]) + sites = max(cases[name]["defect_sites"] for name in ("F_0", "B_1_2")) + require(jf > 0 and jb > 0 and 1 <= sites <= 30_000, "invalid ledger premise") + require(17 * sites <= 2**guard, "feedback premise failed") + f_ratio = FACTOR * jf * Fraction(2**8, 2**guard) + b_ratio = FACTOR * jb * Fraction(2**19, 2**guard) + require(f_ratio < 1 and b_ratio < 1, "completed-stage allowance exceeded") + require(Fraction(49, 256) + Fraction(1923, 8192) + Fraction(1, 2) + == Fraction(7587, 8192) < 1, "decoder transfer inequality failed") + return {"guard": guard, "feedback_factor": str(FACTOR), + "inherited_J_F": str(jf), "inherited_J_B": str(jb), + "inherited_max_sites": sites, "F_allowance_ratio": str(f_ratio), + "B_allowance_ratio": str(b_ratio), "B_strict_slack": str(1 - b_ratio)} + + +def parameter_controls(ledger: dict) -> int: + cases = ledger["cases"] + jf = Fraction(cases["F_0"]["all_cut"]["J"]["J"]) + jb = Fraction(cases["B_1_2"]["all_cut"]["J"]["J"]) + count = 0 + for beta, delta in product((0, 1, 2, 63, 64, 127), (0, 1, 5, 64)): + tolerance = Fraction(1, 2 ** (beta + delta + 101)) + eta_f, eta_b = Fraction(1, 2 ** (beta + 8)), Fraction(1, 2 ** (beta + 13)) + require(FACTOR * 2**delta * tolerance * jf < eta_f, "F parameter case failed") + data_bound, helper_bound = 58 + eta_f, 2**delta + eta_f + require(max(data_bound, helper_bound) <= 2 ** (delta + 6), "noisy entry failed") + require(FACTOR * 2 ** (delta + 6) * tolerance * jb < eta_b, + "B parameter case failed") + count += 1 + return count + + +def rejection_controls(ledger: dict) -> int: + rejected = 0 + try: + guard_certificate(ledger, 100) + except ValueError as error: + require(str(error) == "completed-stage allowance exceeded", "wrong guard rejection") + rejected += 1 + else: + raise ValueError("one-stronger fixed certificate unexpectedly passed") + invalid = (((1, -1), 1, Fraction(0)), ((1, 1, 1), 1, Fraction(0)), + ((1, 1), 0, Fraction(0)), ((1, 1), 1, Fraction(-1)), + ((1, 1), 1, Fraction(1)), ((True, 1), 1, Fraction(0))) + for coefficients, sites, tolerance in invalid: + try: + feedback_bound(coefficients, sites, tolerance) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid polynomial fixture accepted") + manifest = json.loads(read_bytes(PACKAGE / "SOURCES.json")) + for row in manifest["files"]: + if row["usage"] == "input": + try: + authenticate(read_bytes(ROOT / row["path"]) + b" ", row) + except ValueError as error: + require(str(error) == "source SHA256 mismatch", "wrong source rejection") + rejected += 1 + else: + raise ValueError("source-byte mutation accepted") + return rejected + + +def main() -> None: + ledger, hashes = source_inputs() + certificate = guard_certificate(ledger, 101) + counts = {"polynomial_cases": polynomial_controls(), + "parameter_cases": parameter_controls(ledger), + "rejected_controls": rejection_controls(ledger)} + for name in ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py"): + hashes[f"research/{PACKAGE.name}/{name}"] = sha256(read_bytes(PACKAGE / name)).hexdigest() + print(json.dumps({"status": "PASS_QQ16_PRODUCER_ONE_BIT_FEEDBACK", + "claim_type": "scoped proof conditional on the cited PR3235 ledger", + "certificate": certificate, "controls": counts, + "file_sha256": hashes}, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()