Prove the mixed native F0 witness uniformly in precision

research/qq16-f0-all-precision/PROOF.md

@@ -0,0 +1,131 @@
+# Uniform precision for the credited F0 witness
+
+## 1. Model and theorem
+
+Use the literal 26,099-event F0 word and exact native conventions authenticated
+by `SOURCES.json`. The model is PR3067's mixed arithmetic. Each scalar ADD
+component rounds nearest-even to a normalized binary significand of p bits.
+The exponent is unbounded. Completed native operators, native interiors,
+endpoint/residual adapters, SCALEs and private CLEARs are exact. Source and
+destination fields are distinct at every ADD. Private inputs are zero here.
+
+For every integer `p >= 8`, let `D_p=2^(p+12)` and enter physical fields
+`L112=ONE`, `L224=D_p ONE`, with every other field zero. The ideal exact word
+returns the entry. The mixed rounded word has only the five errors stated in
+the README. All helpers return exactly and all private fields are zero.
+
+The exact word, the witness and this endpoint pattern are credited to
+PR3036/PR3067/PR3017. The new assertion is their validity simultaneously for
+all these p. Its proof uses the following rational predicate rather than
+inferring a universal statement from finite runs.
+
+## 2. A nearest-even lemma on a precision ray
+
+Let a and b be real dyadic rationals. Write `x_p=a*2^(p+12)+b`. Fix an integer
+`p0 >= 2`.
+
+If `a=0` and b's reduced numerator needs at most p0 bits, b is exactly
+representable at every `p >= p0`, so `RN_p(x_p)=b`.
+
+Otherwise put `A=a*2^(p0+12)`, `z=A+b`, and
+`e=floor(log2(abs(z)))`. Assume:
+
+1. A and z have the same nonzero sign.
+2. `2^e <= abs(A) <= 2^(e+1)`.
+3. If `abs(A)=2^(e+1)`, then `a*b<0`.
+4. With `q=2^(e-p0+1)`, the number `A/q` is an even integer.
+
+Then, for every integer `p >= p0`,
+
+```text
+RN_p(x_p) = a*2^(p+12) + q*nearest_even_integer(b/q).       (1)
+```
+
+To prove this, put `t=2^(p-p0)`. Dividing `x_p` by t gives `A+b/t`, a convex
+combination of z and A. Conditions 1 through 3 keep its sign fixed and its
+absolute value in `[2^e,2^(e+1))` for every finite t. The possible upper endpoint
+is only approached from below. Thus x_p's binary exponent is exactly
+`e+p-p0`. Its p-bit grid spacing is the constant q, independent of p.
+
+Condition 4 makes `t*A/q` an even integer. Adding that even integer commutes
+with rounding `b/q` to the nearest integer, including tie parity. Multiplying
+by q proves (1). If rounding reaches the upper binade boundary, that boundary
+is itself representable and has the required even parity. Negative values
+follow by sign symmetry. The classifier fails closed if any predicate is not
+established. It makes no claim outside those predicates.
+
+All comparisons and nearest-integer decisions in this lemma use integer or
+Fraction arithmetic. No floating logarithm or finite precision calculation
+establishes a predicate. The separate test oracle enumerates neighboring
+normalized binary numbers and does not call the classifier.
+
+## 3. Induction through the actual program
+
+Maintain two exact Gaussian-dyadic vectors per field, u and v. Their meaning
+is `D_p*u+v` for every `p >= 8`.
+
+At entry u is ONE only in L224 and v is ONE only in L112. Every completed
+native event is a fixed complex-linear operator, so applying the same exact
+operator separately to u and v preserves this meaning. The event dispatcher
+includes the actual child recipes, native lines, source/target endpoint
+monomials and residual adapters. Phase events are control markers. No cover
+sweep occurs in F0. Uniform-owner input and the inherited local tensor
+convention are unchanged from the predecessor.
+
+At a scalar ADD, the exact coefficient product is computed on both tracks.
+For every real and imaginary component, the lemma certifies that this product
+is already exactly representable for all p on the ray. The model's separate
+coefficient multiplication therefore introduces no additional rounding here.
+The destination sum is then treated by the lemma. Equation (1) leaves u
+unchanged and supplies one exact new v. SCALE coefficients are nonzero signed
+powers of two and remain exact in the stated model. Each CLEAR targets only
+an owned private field and sets both tracks to zero.
+
+The source-bound replay checks the lemma's predicates at every scalar product
+and every ADD result. It checks every component whenever u is nonzero; for
+zero u, every distinct constant coefficient suffices. The fixed word has
+40,556 such vector obligations. All pass with p0=8. Thus ordinary finite
+induction on 26,099 events establishes both symbolic tracks for every p>=8.
+
+Exactly two ADDs change the constant track. At event 3887,
+`L112 -= L224/2`, and event 4060, `L139 -= L224/2`, each rounded component is
+
+```text
+exact       -2^(p+11)+1/2
+rounded     -2^(p+11)
+error       -1/2.
+```
+
+The decisions are not ties. The symbolic replay compares all 712 returned
+vectors with the claimed tracks, not just a final digest or the five named
+fields. The ideal run independently follows both tracks without ADD rounding
+and returns the entry. The rounded run returns the unchanged leading track
+and the constant-track errors
+
+```text
+L112: -ONE; L114,L137,L190,L211: -ONE/2; all other fields: zero error.
+```
+
+This closes the finite certificate of the induction's source-specific
+premises. The written lemma supplies its universal quantifier. It is not a
+formal-kernel verification of that lemma, the primitive evaluator or a complete
+multiplication theorem. The direct unchanged predecessor executor agrees at
+p=8,127,256 as a separate implementation control, not the universal proof.
+
+## 4. Consequences and limits
+
+ONE has Euclidean norm `sqrt(512)`. The largest error therefore equals the
+input data norm, giving relative error one. Every exact linear map and binary
+nearest-even rounding commutes with multiplication by a signed power of two.
+Scaling the entire input by `1/32` gives data norm `1/sqrt(2) <= 1` while
+preserving relative error one. Arbitrary non-power-of-two scalings are not
+asserted to commute with rounding.
+
+The dirty input changes with p. Consequently the theorem rules out a
+precision-only uniform data-relative accuracy claim over arbitrary dirty
+magnitudes for this exact mixed model. It does not rule out increasing
+precision for one fixed dirty input, an admitted dirty-range bound, exact-grid
+arithmetic, changed operations or retained information. It is not an
+injectivity theorem or a fully rounded native-program collision. No inference
+about finite exponents, tensor powers, paid precision, recursive costs or the
+F17 consumer follows without their separate contracts.

research/qq16-f0-all-precision/README.md

@@ -0,0 +1,149 @@
+# The mixed native F0 rounding witness at every precision
+
+The same five-field error reported by Ross Richardson in
+[PR3067](https://github.com/CrocSwap/integer-mult-bounds/pull/3067) occurs for
+every integer precision `p >= 8`, under that package's mixed arithmetic model.
+PR3067 checked four finite precisions and explicitly left the all-precision
+statement open. The witness itself, its physical binding and its error pattern
+are predecessor results. This package supplies the uniform implication by
+symbolic execution, not another finite precision sweep.
+
+The scope is exactly one literal `F_0` word, one tensor factor with nine active
+axes and 512 payload coordinates, and owner-uniform inputs. Real and imaginary
+scalar ADD results round to a p-bit binary significand, nearest with ties to
+even and unbounded exponents. Completed native maps, their interiors, endpoint
+and residual adapters, SCALEs and owned CLEARs remain exact. Every scalar
+coefficient product on this family is certified exactly representable for all
+`p >= 8`.
+
+## Result
+
+Set physical `L112 = ONE`, `L224 = 2^(p+12) ONE`, and all other fields zero.
+The exact execution returns this entry. The mixed rounded execution differs
+from it only as follows.
+
+```text
+L112                  -ONE
+L114,L137,L190,L211    -ONE/2
+all 480 helpers       exactly their entry values
+all eight private C   zero
+```
+
+Only scalar events 3887 and 4060 round. Each contributes `-ONE/2`. The maximum
+output-error norm equals the input data norm `sqrt(512)`, so its relative error
+is one. Signed power-of-two scaling preserves the theorem. Scaling by `1/32`
+gives input data norm at most one with the same relative error. The dirty
+magnitude still grows with p. This is not a fixed-input failure at every
+precision or a theorem about bounded dirty state.
+
+[PROOF.md](PROOF.md) gives the affine-rounding lemma and induction. Every
+component has the symbolic form `a*2^(p+12)+b` with exact Gaussian-dyadic
+coefficients. Two endpoint binade checks and an even grid-index condition prove
+one rounding decision for the entire precision ray. The literal word passes
+all these checks with threshold eight. No optimality of that threshold is
+claimed.
+
+This is an accuracy-contract obstruction with exact completed native maps.
+The concurrent [PR3305](https://github.com/CrocSwap/integer-mult-bounds/pull/3305)
+clean-helper original-input collision uses a fully rounded model and is
+separate. Neither its theorem nor its implementation is used here.
+
+## Reproduce
+
+From the repository root, standard-library Python 3.12:
+
+```sh
+python3.12 -I -Werror -B scripts/research_package.py \
+  --package research/qq16-f0-all-precision
+```
+
+Direct commands, also usable from a source export without Git:
+
+```sh
+python3 -I -Werror -B research/qq16-f0-all-precision/verify.py
+python3 -I -O -Werror -B research/qq16-f0-all-precision/test_verify.py -v
+```
+
+`RESULT.json` is the exact canonical receipt. The verifier compares every one
+of the 712 symbolic output vectors with the stated ideal and rounded endpoints.
+Its 40,556 vector rounding/product obligations comprise 38,326 constant-vector
+checks and 2,230 mixed-or-leading-vector checks. All nonconstant checks inspect
+all 1,024 real/imaginary components. These are proof obligations for the ray,
+not sampled precisions.
+
+Eight behavioral groups include 3,762 separate exact-neighbor rounding checks,
+explicit ties and sign changes, rejected unstable binades and tie parity,
+non-dyadic inputs, source corruption and live-input reclassification. The
+unchanged predecessor executor separately agrees at `p=8,127,256`. Exact ADD
+and wrong-gate controls change the endpoint. The two dispatchers share the
+credited exact native evaluator; this is not an independent Clifford audit.
+
+The registered replay passed on CPython 3.12.15, Linux x86_64, including all
+eight groups under optimization. Strict Ruff E,F,I,B,UP,RUF and formatting
+checks passed. These are local results; hosted checks are tracked separately.
+
+All six runtime source files are canonical-main blobs at
+`463113d675af7410ac91d53a4fed51ec6494eb9a`. `SOURCES.json` records their exact
+hashes. The frozen archive's consumed member hashes are additionally checked
+by the unchanged PR3067 loader. Replay needs no unrelated pending-PR object.
+The source export must preserve the declared repository-relative paths. No
+input is regenerated or modified.
+
+## Limits and research decision
+
+This is a scoped written proof with an executable finite certificate of its
+symbolic premises. No independent human or proof-kernel review is claimed.
+Native-internal rounding, bounded exponents, overflow, a fixed caller entry
+lattice, multi-layer/full-cover execution, F0/B1 controller closure, source
+access, paid movement, backing/storage, recursive tariffs, dirty cleanup for a
+different contract and the F17 consumer are not proved or priced here. No
+selected cold replay, Lean or Docker run is required or claimed. There is no
+supplier admission, selected-frontier change or new kappa.
+
+The family decision is narrow and stop. This theorem removes a finite-case
+limitation from one concrete negative accuracy result. It does not justify
+another decoder or construction search. Unknown physical costs remain unknown.
+
+## Open next questions
+
+Can an admitted caller bound the dirty-to-data ratio and choose a sufficient
+paid precision for the actual rounded native interiors? Pin its entry grid,
+range and endpoint contract, then account for every occupied intermediate and
+its consumer. The lack of a complete paid caller blocks supplier admission.
+Exact-grid arithmetic and bounded dirty state remain legitimate escapes.
+
+Can the sufficient threshold eight be reduced for this same mixed-model
+family? The first step is to inspect which affine predicate fails below eight.
+No research decision currently requires a sharper threshold, so another search
+is not proposed here.
+
+## Credit and engineering notes
+
+Arham Tahir supplied PR3036's scalar witness at
+`3717c1e684553c57bc73300410df65438a9ef095`. Ross Richardson supplied PR3067's
+physical witness and finite implementation at
+`e1e28b4070ae52efa5a9d0aa826bc588be7206f2`. Tekalign supplied PR3017's exact
+native evaluator at `0f493f4c264fbc70ee14364b68af260d858c143c`. Nick Petalas's PR2965 supplies the conditional
+producer-output bridge, not an implementation of its premise. Credit Ali Romman,
+Sagar Thakrar, DLamdata, ywz65, starship-s, Douglas Colkitt and the retained
+QQ16/supplier/native lineage as recorded in the unchanged predecessor notices.
+New symbolic proof, checker and controls by Nick Petalas. Substantial AI
+assistance was used in derivation, implementation and checks. Apache-2.0.
+
+Build the Lever determined the rerunnable symbolic certificate rather than a
+prose extrapolation. Prove It Works determined full endpoint comparisons,
+direct native controls and exact publication checks.
+
+The Power of Ten managed-runtime deviation applies to `verify.py` and its
+controls. Python integers, Fractions and tuples allocate dynamically. State is
+bounded by two arrays of 712 vectors with 1,024 components each, the fixed
+26,099-event word, and a 65,536-entry rounding cache. Each authenticated input
+read is capped at 32 MB. Tests use finite ranges and temporary directories with
+scoped cleanup. The imported immutable evaluator retains its bounded 9-axis
+loops and 256-entry monomial cache. Direct predecessor controls also use its
+bounded 32,768-entry integer-rounding cache. Its existing runtime-source compilation is
+restricted to authenticated bytes, not arbitrary expressions. The new code
+uses no recursion; functions stay below 60 lines and validation remains active
+under optimization. Strict Ruff and warning-as-error checks accompany replay.
+This is not an allocation-free tape implementation. A physical implementation
+must replace these managed objects with its own bounded storage and costs.

research/qq16-f0-all-precision/RESULT.json

@@ -0,0 +1,51 @@
+{
+  "dirty_amplitude": "2^(p+12)",
+  "endpoint_affine_sha256": "3633691c9ec19a7ce6bf0aa491a4d08fe9b5b1ad3d2a6eb1637e709afd2f100e",
+  "error_fields": {
+    "112": "-1",
+    "114": "-1/2",
+    "137": "-1/2",
+    "190": "-1/2",
+    "211": "-1/2"
+  },
+  "event_sha256": "4c1ee518a6513c115741a3834c49490c6e8e68f5e2357af8dac782c3d40958e7",
+  "events": 26099,
+  "faults": [
+    {
+      "delta": {
+        "imag": {
+          "0": 512
+        },
+        "real": {
+          "-1/2": 512
+        }
+      },
+      "event": 3887
+    },
+    {
+      "delta": {
+        "imag": {
+          "0": 512
+        },
+        "real": {
+          "-1/2": 512
+        }
+      },
+      "event": 4060
+    }
+  ],
+  "helper_return": "all 480 physical helper fields equal their entry values",
+  "ideal_affine_sha256": "d25b71dad20ba3cc84d4e78224ba02a6a42c76f547f4367fa2cf5e9f72cc00d2",
+  "minimum_precision": 8,
+  "native_internals": "exact, not rounded",
+  "new_kappa": false,
+  "observations": {
+    "constant_vectors": 38326,
+    "mixed_or_leading_vectors": 2230
+  },
+  "private_return": "all eight private fields zero",
+  "quantifier": "every integer p >= minimum_precision",
+  "relative_error": "1",
+  "schema_version": 1,
+  "status": "PASS_QQ16_F0_ALL_PRECISION"
+}

research/qq16-f0-all-precision/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "research/community-frontier1042-audit/selected-replay.tar.gz",
+      "usage": "input",
+      "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b",
+      "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754"
+    },
+    {
+      "path": "research/joint-query/certificate.json.gz",
+      "usage": "input",
+      "git_blob": "c6e876d8b48d768214deee265ade428f8983b566",
+      "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7"
+    },
+    {
+      "path": "research/qq16-f0-physical-rounding/README.md",
+      "usage": "input",
+      "git_blob": "07424e01146187a3cd290b7193b0b6575c9b241f",
+      "sha256": "7e50f1f979f7eec37b026a55a7f2fbfb92a6aadec5458b43062becadd49cd537"
+    },
+    {
+      "path": "research/qq16-f0-physical-rounding/SOURCES.json",
+      "usage": "input",
+      "git_blob": "ba8f0232b4d985f7f6d737ab7f604e95d0da8a0d",
+      "sha256": "b74eff7f957860bd87dc45c4cfaf9e5c02709c623344cf7c055016193df6db0b"
+    },
+    {
+      "path": "research/qq16-f0-physical-rounding/vendor/pr3017/native.py",
+      "usage": "input",
+      "git_blob": "e1976b3a55a40206808405b99a4c443093378bef",
+      "sha256": "999eb1230798b25821de7771ecfa86381e137124059b30ccef167169d176ee8e"
+    },
+    {
+      "path": "research/qq16-f0-physical-rounding/verify.py",
+      "usage": "input",
+      "git_blob": "3d6e9713bf4487bcee6c77b4d0cbb822227f6356",
+      "sha256": "2951da6c9541b524dee0cab32ec3f7409e4ea2c4cca4105c3de3bbcc8fc73c0d"
+    }
+  ]
+}