Independently audit QQ16 cut recovery with payload-sensitive operators

research/qq16-cut-operator-audit/PREDECESSORS.json

@@ -0,0 +1,26 @@
+[
+  {
+    "pr": 2443,
+    "head": "545c05e17243c962b112b91e7f84b4c1a41de7b8",
+    "path": "research/qq16-coordinate-cut-decoder/README.md",
+    "sha256": "91d68f5d01d89ee78802ee5f76e8b901199a686aaa62341090eb70c458fd070e",
+    "git_blob": "1ae3d3eb976ed85f795da2c211b58577ed7e8a82",
+    "usage": "Reviewed source context; not imported at runtime"
+  },
+  {
+    "pr": 2443,
+    "head": "545c05e17243c962b112b91e7f84b4c1a41de7b8",
+    "path": "research/qq16-coordinate-cut-decoder/verify.py",
+    "sha256": "7decbde0922eb8b1473e1cf4ad0b65eee69f040c40ad0bea3b415e82bd129dc7",
+    "git_blob": "e4bcea403a0db78115eba60ab8ec78294cea0c5c",
+    "usage": "Reviewed source context; not imported at runtime"
+  },
+  {
+    "pr": 2432,
+    "head": "cbede349fc764aa38379aa533befe3215916cfcd",
+    "path": "research/qq16-eight-axis-readsets/README.md",
+    "sha256": "4dfcd20ded63c965bd6616a1226ea551d440723a320c447cd696b4960424aee1",
+    "git_blob": "b2100ddb6c28360605c88fc9fbd69488c8de7dc2",
+    "usage": "Reviewed source context; not imported at runtime"
+  }
+]

research/qq16-cut-operator-audit/PROOF.md

@@ -0,0 +1,99 @@
+# What the exact operator check establishes
+
+This is an audit of PR2443's retained-cut decoder, whose result and original
+derivation remain credited there. We use exactly its granted observations.
+
+## Faithful expression representation
+
+Let G be the finite subgroup generated by the actual binary orthogonal owner
+maps. For `g in G` and `a in F2^73`, the affine view acts on arbitrary arrays as
+
+```
+M(g,a) f(d,z_1,...,z_lambda)
+  = f(d g,z_1+d a,...,z_lambda+d a),    lambda >= 1.
+M(g,a) M(h,b) = M(g h,a+g b).
+```
+
+An expression is a finite rational sum of symbols `(input array, g, a)`.
+The checker multiplies matrices over F2 and shifts by this semidirect law,
+collecting exactly equal symbols. A zero expression is therefore a universal
+operator identity, for arbitrary arrays and every positive tensor power.
+
+Conversely distinct `(g,a)` evaluate at `d=I` and every `z_i=0` at distinct
+array addresses `(g,a,...,a)`. For a nonzero expression, select one nonzero
+coefficient and set only that input array's value at that address to one.
+All other input values are zero. The output residual at `(I,0,...,0)` is
+exactly that coefficient. This gives an independently inspectable concrete
+counterexample from each `negative_controls` entry in RESULT.json. No regular
+cover enumeration or numerical rank estimate is needed.
+
+The logical chart in the inherited QQ16 formulas is `D=M(rho,0)`. Physical
+alignment is `A=M(rho,delta)`, and the native boundary gauges relate them by
+`A T = T_common D`. They cannot be substituted for one another in a logical
+decoder. This audit inherits that bridge identity; it does not re-prove it.
+
+## Factorization avoids a finite input sampling assumption
+
+Write `H` for the map from arbitrary post-F0 `(x1,y1)` to the granted cut
+observations. The source formulas used in H are only
+
+```
+y2_A = y1_A + P_(2,A) [B_2 y1_U + ell_(2,T) y1_T]
+C = x2_U = x1_U - y1_U.
+```
+
+Together with the 32 selected post-F0 arrays and the 88 read ordinary arrays,
+these are exactly 224 output arrays. Let `Hinv` be the audit's decoder on this
+post-F0 state. From the selected logger difference it computes
+
+```
+v = ell_(2,A) (y2_A-y1_A) - ell_(2,T) y1_T + B_2 C
+  = B_2 x1_U.
+rhs = v - B_(2,S) x1_S = R_J D_(2,J) x1_J.
+x1_J = D_(2,J)^(-1) R_J^(-1) rhs.
+y1_U = x1_U - C.
+```
+
+The scalar inverse is applied before each distinct port inverse. The selected
+post-F0 state was retained directly. The checker verifies `Hinv H=I` on 224
+independent formal input arrays. Independently granting all 224 output arrays,
+it verifies `H Hinv=I`. Thus no hidden consistency relation on the saved records
+is used by either direction.
+
+It separately reconstructs the conserved forward F0 and its inverse from the
+main source contract. Both `Finv F=I` and `F Finv=I` hold on 224 independent
+formal arrays. Consequently the full observation transform is `H F`, with
+two-sided inverse `Finv Hinv`. This establishes the audited arbitrary-input
+identity under the inherited QQ16 local contract. It is not a proof of native
+availability of H's records.
+
+## Payload-sensitive negative control
+
+In the decoder only, replace every logical stage-2 map and its inverse by the
+actual corresponding native alignment and inverse. Keep the observed data
+produced by H unchanged. The resulting output has a nonzero residual in the
+full affine algebra; its explicit input-array/address/coefficient witness is
+recorded under `native_alignment_for_logical_chart`.
+
+Now project every symbol `(v,g,a)` to `(v,g,0)`, combining coefficients again.
+This projection is exactly restriction to payload-constant input arrays. The
+entire faulty result becomes the identity after that projection. The checker
+tests all 224 rows of this statement. Therefore the mutation is invisible to
+all payload-constant fixtures, not merely to a chosen finite fixture set.
+
+This does not identify a bug in PR2443. Its code uses owner-only logical routes;
+its proof invokes the proper inherited contract. The control provides a precise
+failure mode for future physical lowering and a stronger regression target.
+
+## Source coverage and proof boundary
+
+R is independently reconstructed by propagating the source scalar prefix to
+its centre boundary. Stage-1 and stage-2 owner routes and payload translations
+are reconstructed from the retained phase geometry and compared with all 224
+registered entry/inverse pairs. The first two selected-template events are
+bound to pair zero, with F0 followed directly by B1. The packet's selected
+partition, K, selected and ordinary Grams, and unread minor are checked exactly.
+
+The proof applies to the granted two-cut logical interface. The audit does not
+execute the whole backward native word, prove legal reads at mixed frames,
+retain records through later calls, count native costs, or admit a supplier.

research/qq16-cut-operator-audit/README.md

@@ -0,0 +1,104 @@
+# QQ16 retained-cut decoder: independent exact operator audit
+
+**The ordered recovery in PR2443 passes an independent symbolic audit.** The
+checker verifies both inverse orders on all 224 formal input arrays and all
+224 independently specified observation arrays, using actual 73-dimensional
+owner maps. No producer executable is imported. No new supplier or kappa is
+claimed.
+
+The additional failure control separates logical and physical charts: replacing
+the logical owner-only map `D=(rho,0)` in the decoder with the native alignment
+`A=(rho,delta)` produces a nonzero exact arbitrary-payload residual. The same
+fault passes after every payload shift is forgotten. Thus payload-constant
+fixtures alone cannot distinguish this incorrect implementation. This is a
+deliberately injected fault, **not a defect found in PR2443**, which correctly
+uses the logical maps.
+
+## Audited contract and evidence
+
+The audited predecessor is [PR2443](https://github.com/CrocSwap/integer-mult-bounds/pull/2443)
+at `545c05e17243c962b112b91e7f84b4c1a41de7b8`. Read source hashes are in
+[PREDECESSORS.json](PREDECESSORS.json). Its unread ports are
+`J=[1,2,3,4,5,6,8,12]`; the other 88 ordinary ports are read. With
+`(x1,y1)=F0(x,y)` and `(x2,y2)=B_1_2(x1,y1)`, exactly these observations are
+granted, without intervening changes:
+
+- `x1_A/T` and `y1_A/T`: 32 complete arrays at the F0 cut;
+- `y2_A` and `C=x2_U`: 104 complete arrays at the B1 cut;
+- `x1_(U\J)`: 88 complete arrays at the F0 cut.
+
+This is 224 arrays in total, not 88 total records. Each array includes arbitrary
+owner and payload contents. The retained first two events operate on pair zero;
+the other three pairs are not decoded.
+
+The [proof and audit interpretation](PROOF.md) explain the factorization into
+F0 and the cut observation map. The checker reconstructs R from the immutable
+predecessor's scalar prefix, rebuilds stage-1/stage-2 routes and translations
+from its phase geometry, and compares all 224 entry/inverse pairs with the
+emitted QQ16 packet. It checks the selected Grams, K, unread minor and both
+minor inverse orders. Formal expressions retain independent array identifiers
+and exact affine owner/payload operators, with rational coefficients.
+
+[RESULT.json](RESULT.json) records four complete inverse identities and seven
+rejected faults, including a concrete point-supported input for each residual.
+The six other controls omit the old A baseline, omit the future T term, reverse
+the C sign, apply port inverses before the scalar inverse, discard the B1 A
+cut, or discard initial Y dirt. Source-file corruption controls and optimized
+replay are registered separately. No floating-point acceptance is used.
+
+## Reproduce
+
+Python 3.10+ and the standard library suffice for the direct checker. The
+repository's registered environment is Python 3.12:
+
+```sh
+python3 -I -B research/qq16-cut-operator-audit/verify.py
+python3.12 -I -B scripts/research_package.py --package research/qq16-cut-operator-audit
+```
+
+Expected direct status: `PASS_QQ16_CUT_OPERATOR_AUDIT`. Replay is read-only and
+compares the entire recomputed receipt with the committed file. Receipt creation
+is explicit via `--write-result` and refuses to overwrite an existing file.
+The source archive and frozen packages remain unchanged. Sources and Git
+provenance are in [SOURCES.json](SOURCES.json); scope is in [TASK.json](TASK.json).
+
+## Limits
+
+This checks the mathematical decoder from PR2443's displayed formulas, not the
+execution of its Python implementation. It imports no implementation from that
+PR. The inherited QQ16 logical local contract, physical/logical conjugation,
+and legal native kernels are not re-proved. The extra native-alignment mutation
+is a diagnostic on the logical decoder; it does not execute a physical decoder.
+
+Neither the remaining 17 schedule events nor final endpoint availability is
+checked. Retaining the two cuts, native read permissions, storage, cleanup,
+hosting, addresses, precision, all-size transfer, and the complete invoice
+remain open. Four operator identities are not a formal verification of the
+full multiplication theorem. No full selected cold replay was needed or run.
+
+## Open next questions
+
+1. Can a physical implementation realize the decoder with the correct
+   input/output gauges? First trace each read in the pinned formula through
+   the bridge relation `A T = T_common D`. The missing work is the mixed
+   endpoint types and retention, not the scalar inverse.
+2. Can the two retained cuts be reconstructed at final controller endpoints?
+   First propagate the 224 observation arrays through the complete remaining
+   schedule. A favorable scalar identity alone supplies no legal record.
+
+Both questions and their blockers are recorded in [TASK.json](TASK.json).
+
+## Credit
+
+`starship-s` / PR2443 supplies the audited arbitrary-input cut decoder and its
+observation contract; Gareth Davidson / PR2432 supplies its unread basis and
+coordinate-read lineage. commdata2338 / PR2174 supplies the earlier two-query
+cut recovery. Ali Romman / PR1969 supplies the QQ16 local maps and native
+contract; Adam Gall / PR2093, kyzer1023 / PR2354, PR2389 and PR2419 supply
+the hidden-family and read-set work. The retained Rohan Arun, Jeremy Kothe,
+DreamingOfClouds and other source contributors keep their attribution in
+[the source notice](../joint-query/NOTICE.md).
+
+The independent reviewer code, exact operator audit, and diagnostic control
+were prepared by ywz65 with substantial OpenAI Codex assistance. No independent
+human or proof-assistant review is claimed. New work is Apache-2.0.