From 19947aa37abbc9cfd1fe3f2b2b9c5449f19a1652 Mon Sep 17 00:00:00 2001
From: Nick Petalas <webmasternikos@gmail.com>
Date: Tue, 3 Nov 2026 11:20:10 +0000
Subject: [PATCH] feat(research): prove a rounded inverse oracle error floor

---
 research/neumann-oracle-error-floor/PROOF.md  | 137 ++++++++++++
 research/neumann-oracle-error-floor/README.md | 133 ++++++++++++
 .../neumann-oracle-error-floor/SOURCES.json   |  24 +++
 research/neumann-oracle-error-floor/TASK.json |  95 +++++++++
 .../neumann-oracle-error-floor/VERIFY.json    |  34 +++
 research/neumann-oracle-error-floor/verify.py | 198 ++++++++++++++++++
 6 files changed, 621 insertions(+)
 create mode 100644 research/neumann-oracle-error-floor/PROOF.md
 create mode 100644 research/neumann-oracle-error-floor/README.md
 create mode 100644 research/neumann-oracle-error-floor/SOURCES.json
 create mode 100644 research/neumann-oracle-error-floor/TASK.json
 create mode 100644 research/neumann-oracle-error-floor/VERIFY.json
 create mode 100644 research/neumann-oracle-error-floor/verify.py

diff --git a/research/neumann-oracle-error-floor/PROOF.md b/research/neumann-oracle-error-floor/PROOF.md
new file mode 100644
index 0000000000..2545087dcf
--- /dev/null
+++ b/research/neumann-oracle-error-floor/PROOF.md
@@ -0,0 +1,137 @@
+# A linear error floor for rounded inverse oracles
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped written proof with exact finite corroboration.
+
+## Interface and theorem
+
+Use the maximum complex-coordinate norm. Write D_p for the closed complex
+unit disk intersected with 2^-p Z[i]. The numerical contract is Hanson Sun's
+PR1430: p>100, h=2^-p, eta=ph/3, a linear E with norm at most 21/50,
+and a deterministic T:D_p^s -> D_p^s satisfying
+
+```text
+||T(z)-Ez|| < eta  for every z in D_p^s.
+```
+
+An integer 1<=k<=p must satisfy ||E^k||<=h. The task is to approximate
+`(I+E)^(-1)u/2` for u in D_p^s. In the oracle model here, E is hidden.
+The algorithm receives p,k,u, the norm/error promises and access to T.
+It receives no other E-dependent information. It may make any number of
+valid adaptive queries, or even inspect the entire common function T.
+
+For every integer p>100, there are two admissible entrywise nonnegative
+two-coordinate operators E_- and E_+, with k=p and the same odd,
+zero-preserving oracle T, for which every deterministic algorithm has error
+greater than `(4/9)ph` on at least one instance. The same lower bound holds
+for worst-case expected error of randomized algorithms. No randomized
+algorithm can have success probability greater than 1/2 on both instances
+at any error radius less than the two-instance radius R_p below.
+
+Combined with PR1430's cited `<ph` Horner upper bound, the optimal worst-case
+error order from this contract alone is Theta(ph). The exact minimax constant
+for the entire contract class is not asserted.
+
+## One common rounded oracle
+
+Let S swap the two coordinates and put
+
+```text
+alpha = 2/5,  delta = (p/3-1)h,
+E_- = (alpha-delta)S,  E_+ = (alpha+delta)S.
+```
+
+For z=h(n+im), let Q(z) be h times the nearest Gaussian integer to
+`(2n/5)+i(2m/5)`. There are no ties, since the denominators are odd.
+Define T(z_0,z_1)=(Q(z_1),Q(z_0)).
+
+Each real rounding residual is at most 2h/5 in absolute value. Hence
+
+```text
+|Q(z)-alpha*z| <= (sqrt(8)/5)h < h.
+```
+
+Q, and therefore T, is odd and zero-preserving. For every disk input,
+`|Q(z)| <= alpha+sqrt(8)h/5 < 1`, so T maps the entire required grid into
+itself. For either hidden operator and every input in D_p^2,
+
+```text
+||T(z)-E_+ z|| < h+delta = eta,
+||T(z)-E_- z|| < h+delta = eta.
+```
+
+This establishes the full-domain promise, rather than a sampled-query
+promise. It also implies the retained bound
+`||T(z)|| < (21/50)||z||+eta`.
+
+For p>=101, `0<delta<1/50`. Indeed `(p/3-1)2^-p` decreases for p>4,
+and its value at p=101 is less than 1/50. Thus
+
+```text
+0 < alpha-delta < alpha+delta < 21/50 < 1/2.
+```
+
+Both operators are entrywise nonnegative, and have norm alpha-delta and
+alpha+delta respectively. They preserve coordinatewise positivity; no
+positive-semidefinite hypothesis is used. Since S is an isometry,
+`||E_+^p||=(alpha+delta)^p<h`, and the same holds for E_-.
+Choosing k=p therefore supplies the required tail premise for both.
+
+## Separated exact inverse answers
+
+Choose the common input u=(1,-1), which belongs to D_p^2 and satisfies
+Su=-u. Put a=1-alpha=3/5. The exact answers are
+
+```text
+y_- = u/[2(a+delta)],  y_+ = u/[2(a-delta)].
+||y_+-y_-|| = delta/(a^2-delta^2) = 2R_p,
+R_p = delta/[2(9/25-delta^2)].
+```
+
+All denominators are positive. In particular,
+
+```text
+R_p > (25/18)delta
+    = (25p/54-25/18)h
+    > (4p/9)h.
+```
+
+The last strict inequality is equivalent to p>75. This proves the stated
+constant for every p>100. The two-instance radius also satisfies
+`R_p/(ph) -> 25/54`; this is a property of these two instances, not a global
+optimality claim.
+
+## Indistinguishability
+
+Every query has exactly the same response in the two instances. By induction,
+an adaptive deterministic algorithm has the same transcript and the same
+output v. The triangle inequality gives
+
+```text
+2R_p = ||y_+-y_-|| <= ||y_+-v||+||v-y_-||.
+```
+
+At least one error is at least R_p, hence strictly greater than `(4/9)ph`.
+The midpoint of y_- and y_+ attains R_p on this two-instance decision problem.
+The lower bound survives arbitrary query budgets because the whole function
+T is identical, not just a selected finite transcript.
+
+A randomized algorithm has the same output distribution on both instances.
+Taking expectations in the triangle inequality proves the expected-error
+statement, including infinite expectation. For any radius r<R_p, the two
+closed success balls are disjoint. Their probabilities under that common
+distribution sum to at most one, so at least one success probability is at
+most 1/2. This does not assert which hidden instance is worse for a given
+algorithm or random seed.
+
+## What would evade this obstruction
+
+The exact operator is not supplied separately. An algorithm that can inspect
+an exact Gaussian formula, use E-dependent auxiliary data, refine the oracle
+precision, or invoke a stronger relative-error law is outside this theorem.
+The pair is not asserted to be an actual Gaussian resampling operator.
+The result concerns the absolute numerical interface, not physical running
+time, native calls, dirty restoration or a complete multiplication theorem.
+No selected assumption or frontier value is changed. The universal statements
+rest on this written proof. Finite checks do not enumerate all algorithms,
+all grid points at p>100, or all precisions.
diff --git a/research/neumann-oracle-error-floor/README.md b/research/neumann-oracle-error-floor/README.md
new file mode 100644
index 0000000000..b53ccddc74
--- /dev/null
+++ b/research/neumann-oracle-error-floor/README.md
@@ -0,0 +1,133 @@
+# Linear error is unavoidable for the absolute rounded inverse oracle
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped written proof with exact finite corroboration.
+
+For every integer p>100, two entrywise nonnegative 2-by-2 operators have
+the same odd, zero-preserving rounded oracle under PR1430's absolute error
+contract, but their inverse answers differ by more than `(8/9)p*2^-p`.
+Every algorithm that accesses the hidden operator only through that oracle
+therefore has worst-case error greater than `(4/9)p*2^-p`, even with
+arbitrarily many adaptive queries. The lower bound also holds for randomized
+expected error. At any radius smaller than the exact two-instance radius,
+one instance has success probability at most one half.
+
+Hanson Sun / bbMisk's [PR1430](https://github.com/CrocSwap/integer-mult-bounds/pull/1430)
+supplies the cited numerical contract and the `<p*2^-p` fixed-source Horner
+upper bound. This new lower bound makes the error order optimal for that
+oracle model. It is not an audit or replay of the predecessor. The exact
+minimax constant and an actual Gaussian implementation are not determined.
+
+The [proof](PROOF.md) uses
+
+```text
+h=2^-p, delta=(p/3-1)h, S=coordinate swap,
+E_+/-=(2/5 +/- delta)S, T=nearest-grid rounding of (2/5)S,
+u=(1,-1), k=p,
+R_p=delta/[2(9/25-delta^2)] > (4/9)ph.
+```
+
+T is identical as a function on the entire complex disk grid for the two
+instances. More oracle queries cannot distinguish them. A smaller asymptotic
+error therefore needs an extra hypothesis or additional operator information.
+
+## 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/neumann-oracle-error-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/neumann-oracle-error-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/neumann-oracle-error-floor
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/neumann-oracle-error-floor --check-source-history --check-modes
+```
+
+Another CPython 3.12 path can replace the local installation. Direct replay
+writes nothing and requires only this package. It emits
+`PASS_NEUMANN_ORACLE_ERROR_FLOOR` and a generated JSON report binding all six
+package files by SHA256. No receipt is handwritten or frozen.
+
+The verifier independently compares integer and Fraction rounding on every
+complex disk-grid point at p=0..7, covers all 25 rounding residue pairs, and
+checks 416 source-precision instances, p=101..512 plus 768,1024,2048,4096.
+The latter include literal inverse equations, the separation formula,
+boundary and complex oracle inputs, and six literal tail powers. It also
+checks 3,104 scalar two-answer decisions and 136 randomized mixtures.
+Six invalid precisions, four false inverse answers and four semantic
+discriminators cover the relevant boundary and failure modes. These finite
+domains corroborate the written proof; they do not establish its universal
+quantifiers by extrapolation. No predecessor executable is imported.
+
+## Scope, sources and research decision
+
+The exact hidden operator is accessible only through the fixed-precision T.
+Exact operator coefficients or a formula, additional E-dependent information,
+refined precision and stronger relative-error promises can evade the result.
+Nick Petalas's pending [PR6490](https://github.com/CrocSwap/integer-mult-bounds/pull/6490)
+assumes access to a family of oracles at every requested precision and reduces
+their precision volume. That changed-access model is outside this theorem;
+the present target is the error floor for PR1430's single fixed oracle.
+Entrywise nonnegative here means order-preserving; these swap matrices have
+a negative eigenvalue. The construction is an abstract numerical interface,
+with no claim that it occurs in an actual Gaussian resampling routine.
+
+Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priorities
+revision 8, selected PR6030. SOURCES.json pins the predecessor's retained
+README and the original catalogue/selected record as historical provenance.
+The source publication head is `1655c721a1c2aa92f584523afc93a192137cf910`.
+The original uniform-transfer-audit card is explicitly changed to this
+numerical-interface side theorem. The selected source-binding first command
+passed; no selected scientific suite was run. This closes one scope and
+provides no basis for extending a construction without its full cost ledger.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372374)
+followed live handoff, active/open work, recent account, main README,
+merged/general-form and local-reservation searches. The cached overlap helper
+adds bounded remote coverage and incomplete sparse notes; unpublished work
+and arbitrary historical diffs remain outside coverage. Searches do not prove
+novelty.
+
+Credit Hanson Sun / bbMisk for PR1430's absolute contract, Horner upper bound
+and stronger-structure question; eumemic, icekylinx and the retained Gaussian
+and Harvey–van der Hoeven resampling lineage for the underlying interface.
+The predecessor's Artus Krohn-Grimberghe, Effy Elden, Alan Grillo and other
+source attributions remain intact. Classical rounding and indistinguishable
+oracle arguments retain their credit. No general literature-priority claim,
+independent human review or formal proof-kernel acceptance is made.
+
+Physical coefficient preparation, native implementation, actual Gaussian
+structure, ownership/restoration, precision/tape/stock costs and complete
+supplier/outer admission remain unproved here. All five selected framework
+assumptions remain. There is no new kappa or selected-frontier change, and
+no Lean, Docker or full multiplication replay.
+
+## Open next questions
+
+1. Can a source-bound Gaussian routine supply E-dependent structure that
+   permits a smaller inverse error? Start with a proved local error law on
+   its actual complex grid. The present indistinguishable pair must be
+   excluded by that law, and physical precision/caller costs remain blockers.
+2. What is the exact minimax constant for the fixed absolute oracle contract?
+   Start with a scalar coefficient interval recovered from a complete oracle
+   table, then compare its radius with the Horner upper bound. The current
+   two-instance radius is a lower bound, not a solution of that whole problem.
+
+## Implementation constraints
+
+The standalone verifier uses exact rational arithmetic, direct calls and no
+recursion, external libraries, network, subprocesses or write path. Every
+loop has a fixed finite domain or a bound from the checked p<=4096 interface.
+The largest disk enumeration has 257 squared candidate coordinate pairs;
+only one point is retained at a time. All functions fit within sixty physical
+lines. Explicit exceptions preserve checks under optimization. Syntax parsing
+and warning-strict normal/optimized replay are the diagnostics used; no
+separate type or lint analyzer is claimed.
+
+Power of Ten rule 3 deviation: CPython allocates integers, Fractions and
+bounded temporary collections dynamically. Precision is capped at 4096,
+literal powered rational denominators below 70,000 bits,
+and each of the six hashed files at 1 MiB. Runtime allocation internals are
+not measured. A native steady-operation implementation would need a fixed
+arithmetic-storage contract. Rule 9 deviation: rejecting controls use two
+fixed callback targets, parameters and inverse-equation checks, only inside
+their bounded local loops. No callback is accepted from outside the program.
diff --git a/research/neumann-oracle-error-floor/SOURCES.json b/research/neumann-oracle-error-floor/SOURCES.json
new file mode 100644
index 0000000000..5d1bd60e77
--- /dev/null
+++ b/research/neumann-oracle-error-floor/SOURCES.json
@@ -0,0 +1,24 @@
+{
+  "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/neumann-rounding-audit/README.md",
+      "usage": "provenance",
+      "git_blob": "6c6c0899fc00144c2ba97f1760ecd50a22ba6d57",
+      "sha256": "332a166718e3671b0db06c8cb73ca7673ee0224ac2645eea61972041d50a110e"
+    }
+  ]
+}
diff --git a/research/neumann-oracle-error-floor/TASK.json b/research/neumann-oracle-error-floor/TASK.json
new file mode 100644
index 0000000000..e2d2e6e83c
--- /dev/null
+++ b/research/neumann-oracle-error-floor/TASK.json
@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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": "A new two-instance lower bound proving order-optimal inverse error under the absolute rounded-E oracle interface, including unlimited adaptive queries and randomized expected error.",
+  "scope_change_reason": "This is a numerical-interface side theorem motivated by PR1430, not a proof of one selected framework assumption at its physical caller.",
+  "bottleneck_link": "The retained precision interface bounds local rounded-operator error by p*2^-p/3. The result shows that an o(p*2^-p) inverse allowance requires additional operator information or a stronger oracle contract.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved indistinguishability lower bound, exact finite corroboration and one focused package.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the all-p proof. verify.py supplies exact finite rounding, two-operator, inverse, minimax and rejection checks without predecessor scientific replay.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can an actual Gaussian routine exclude the indistinguishable pair with a stronger error law?",
+      "why_it_matters": "Additional information is necessary to improve the error order in this oracle model.",
+      "first_step": "Derive a source-bound local rounding law on the actual complex grid and compare its hypotheses with the pair.",
+      "blocked_by": "Actual Gaussian structure and complete precision/caller cost evidence."
+    },
+    {
+      "question": "What is the exact minimax constant for the complete absolute oracle class?",
+      "why_it_matters": "The proof determines the error order and a lower constant, not the optimal constant.",
+      "first_step": "Analyze coefficient intervals consistent with one complete scalar rounded-oracle table.",
+      "blocked_by": "A matching upper bound for all admissible operators and oracle tables."
+    }
+  ],
+  "environment": {
+    "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12",
+    "version": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]",
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "machine": "arm64"
+  }
+}
diff --git a/research/neumann-oracle-error-floor/VERIFY.json b/research/neumann-oracle-error-floor/VERIFY.json
new file mode 100644
index 0000000000..11a3aaedda
--- /dev/null
+++ b/research/neumann-oracle-error-floor/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 finite rounding, common-oracle instances, inverse separation, minimax and rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The identical finite checks with assertion optimization enabled."
+    }
+  ]
+}
diff --git a/research/neumann-oracle-error-floor/verify.py b/research/neumann-oracle-error-floor/verify.py
new file mode 100644
index 0000000000..f00c56fb21
--- /dev/null
+++ b/research/neumann-oracle-error-floor/verify.py
@@ -0,0 +1,198 @@
+#!/usr/bin/env python3
+"""Exact finite corroboration of the rounded inverse oracle lower bound."""
+
+from fractions import Fraction as F
+from hashlib import sha256
+from pathlib import Path
+import ast
+import json
+
+
+def require(condition: bool, message: str) -> None:
+    if not condition:
+        raise ValueError(message)
+
+
+def parameters(p: int) -> tuple[F, F, F, F, F]:
+    require(type(p) is int and 101 <= p <= 4096, "precision outside 101..4096")
+    h = F(1, 2**p)
+    eta = p * h / 3
+    delta = eta - h
+    return h, eta, delta, F(2, 5) - delta, F(2, 5) + delta
+
+
+def rounded_numerator(n: int) -> int:
+    """Nearest integer to 2*n/5. Its odd denominator excludes ties."""
+    q, r = divmod(2 * n, 5)
+    return q + int(2 * r > 5)
+
+
+def oracle(z: tuple[tuple[int, int], tuple[int, int]]) -> tuple:
+    """Grid numerators of the two complex entries, with their roles swapped."""
+    return tuple(tuple(rounded_numerator(t) for t in w) for w in reversed(z))
+
+
+def inverse_answer(c: F) -> tuple[F, F]:
+    """Literal determinant inverse of [[1,c],[c,1]] on (1,-1)/2."""
+    determinant = 1 - c * c
+    require(determinant > 0, "singular or unsupported inverse")
+    return (F(1, 2) + c / 2) / determinant, (-c / 2 - F(1, 2)) / determinant
+
+
+def check_answer(c: F, answer: tuple[F, F]) -> None:
+    x, y = answer
+    require(x + c * y == F(1, 2), "first inverse equation")
+    require(c * x + y == -F(1, 2), "second inverse equation")
+
+
+def error_squared(actual: tuple[int, int], n: int, m: int, c: F, h: F) -> F:
+    return h * h * ((actual[0] - c * n) ** 2 + (actual[1] - c * m) ** 2)
+
+
+def check_rounding() -> dict:
+    points = 0
+    for p in range(8):
+        scale = 2**p
+        for n in range(-scale, scale + 1):
+            for m in range(-scale, scale + 1):
+                if n * n + m * m > scale * scale:
+                    continue
+                r, s = rounded_numerator(n), rounded_numerator(m)
+                literal = tuple((F(2 * t, 5) + F(1, 2)).__floor__() for t in (n, m))
+                require((r, s) == literal, "literal rounding disagrees")
+                require((5 * r - 2 * n) ** 2 + (5 * s - 2 * m) ** 2 <= 8,
+                        "complex rounding residual exceeds 8/25")
+                require(r * r + s * s <= scale * scale, "rounded disk exit")
+                require(rounded_numerator(-n) == -r, "rounding is not odd")
+                points += 1
+    residues = []
+    for n in range(5):
+        for m in range(5):
+            r, s = rounded_numerator(n), rounded_numerator(m)
+            residues.append((5 * r - 2 * n) ** 2 + (5 * s - 2 * m) ** 2)
+    require(max(residues) == 8 and len(residues) == 25, "residue coverage")
+    return {"disk_points": points, "residue_pairs": len(residues), "maximum_scaled_error_squared": 8}
+
+
+def source_fixtures(p: int) -> tuple:
+    scale = 2**p
+    return ((0, 0), (1, 1), (-1, 2), (scale, 0), (-scale, 0),
+            (0, scale), (scale // 2, -scale // 2),
+            (3 * scale // 5, 4 * scale // 5))
+
+
+def check_precision_cases() -> dict:
+    precisions = tuple(range(101, 513)) + (768, 1024, 2048, 4096)
+    samples = 0
+    tail_powers = 0
+    for p in precisions:
+        h, eta, delta, lo, hi = parameters(p)
+        require(0 < lo < hi < F(21, 50) < F(1, 2), "operator norm bounds")
+        require(delta + h == eta and F(8, 25) < 1, "strict local margin")
+        require(F(2, 5) + h < 1, "oracle disk bound")
+        a, b = inverse_answer(lo), inverse_answer(hi)
+        check_answer(lo, a)
+        check_answer(hi, b)
+        gap = max(abs(x - y) for x, y in zip(a, b))
+        radius = delta / (2 * (F(9, 25) - delta * delta))
+        require(gap == 2 * radius, "inverse separation formula")
+        require(radius > F(25, 18) * delta > F(4, 9) * p * h, "linear floor")
+        midpoint = tuple((x + y) / 2 for x, y in zip(a, b))
+        require(max(abs(x - y) for x, y in zip(a, midpoint)) == radius,
+                "two-instance midpoint radius")
+        for n, m in source_fixtures(p):
+            require(n * n + m * m <= 2 ** (2 * p), "fixture outside disk")
+            z = ((n, m), (-m, n))
+            got = oracle(z)
+            require(oracle(tuple(tuple(-t for t in w) for w in z)) ==
+                    tuple(tuple(-t for t in w) for w in got), "oracle oddness")
+            for c in (lo, hi):
+                for actual, (nr, ni) in zip(got, reversed(z)):
+                    require(error_squared(actual, nr, ni, c, h) < eta * eta,
+                            "common oracle violates local error")
+                    samples += 1
+        if p in (101, 128, 256):
+            for c in (lo, hi):
+                require(c**p < h, "literal tail-power check")
+                tail_powers += 1
+    return {"precision_cases": len(precisions), "local_component_checks": samples,
+            "literal_tail_powers": tail_powers, "largest_precision": max(precisions)}
+
+
+def rejected(call, message: str) -> None:
+    try:
+        call()
+    except ValueError:
+        return
+    raise ValueError("accepted control: " + message)
+
+
+def check_controls() -> dict:
+    invalid = (False, 100, 4097, F(101), 101.0, "101")
+    for value in invalid:
+        rejected(lambda value=value: parameters(value), "invalid precision")
+    h, eta, delta, lo, hi = parameters(128)
+    a, b = inverse_answer(lo), inverse_answer(hi)
+    wrong = ((lo, tuple(2 * t for t in a)), (hi, a),
+             (lo, tuple(-t for t in a)), (lo, (a[1], a[0])))
+    for c, answer in wrong:
+        rejected(lambda c=c, answer=answer: check_answer(c, answer), "false inverse")
+    scale = 2**128
+    got = oracle(((scale, 0), (0, 0)))[1]
+    require(max(error_squared(got, scale, 0, F(2, 5) + s * eta, h)
+                for s in (-1, 1)) > eta * eta, "omitted rounding margin undetected")
+    require(hi > h, "invalid one-call tail not detected")
+    require(a != b and oracle(((0, 0), (0, 0))) == ((0, 0), (0, 0)),
+            "hidden operator or zero-input discriminator")
+    positive_gap = delta / (F(49, 25) - delta * delta)
+    require(positive_gap / 2 < F(4, 9) * 128 * h, "wrong input eigenspace undetected")
+    require(max(abs(x - y) for x, y in zip(a, b)) > F(8, 9) * 128 * h,
+            "separation lost")
+    return {"invalid_precisions_rejected": len(invalid),
+            "false_inverse_answers_rejected": len(wrong), "semantic_discriminators": 4}
+
+
+def check_pair_minimax() -> dict:
+    """Independent one-dimensional two-instance decisions in rational units."""
+    cases = 0
+    for distance in range(1, 33):
+        for numerator in range(-32, 65):
+            answer = F(numerator, 2)
+            left, right = abs(answer), abs(answer - distance)
+            require(max(left, right) >= F(distance, 2), "deterministic minimax")
+            radius = F(distance, 2) - F(1, 4)
+            require(not (left < radius and right < radius), "overlapping success balls")
+            cases += 1
+    mixtures = 0
+    for distance in range(1, 9):
+        for weight in range(17):
+            probability = F(weight, 16)
+            e0, e1 = (1 - probability) * distance, probability * distance
+            require(max(e0, e1) >= F(distance, 2), "randomized expected minimax")
+            mixtures += 1
+    return {"deterministic_decisions": cases, "two_output_mixtures": mixtures}
+
+
+def package_hashes() -> dict:
+    package = Path(__file__).resolve().parent
+    names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py")
+    hashes = {}
+    for name in names:
+        path = package / name
+        require(path.is_file() and not path.is_symlink(), "missing regular package file")
+        require(path.stat().st_size <= 1024 * 1024, "package file exceeds 1 MiB")
+        hashes[name] = sha256(path.read_bytes()).hexdigest()
+    ast.parse((package / "verify.py").read_text())
+    return hashes
+
+
+def main() -> None:
+    report = {"status": "PASS_NEUMANN_ORACLE_ERROR_FLOOR",
+              "rounding": check_rounding(), "instances": check_precision_cases(),
+              "controls": check_controls(), "minimax": check_pair_minimax(),
+              "package_sha256": package_hashes()}
+    print(json.dumps(report, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()