From 48e4be7d845b5ac9e465c3a8bffe04b36a8b6aff Mon Sep 17 00:00:00 2001 From: ywz65 <154373401+ywz65@users.noreply.github.com> Date: Thu, 15 Oct 2026 09:24:17 -0700 Subject: [PATCH] Extend QQ16 obstruction to normalized Clifford coefficients --- .../qq16-clifford-ring-obstruction/PROOF.md | 149 +++ .../qq16-clifford-ring-obstruction/README.md | 98 ++ .../RESULT.json | 1061 +++++++++++++++++ .../SOURCES.json | 57 + .../qq16-clifford-ring-obstruction/TASK.json | 160 +++ .../VERIFY.json | 35 + .../qq16-clifford-ring-obstruction/ring.py | 82 ++ .../source/PR2443-README.md | 213 ++++ .../source/PR2546-README.md | 181 +++ .../test_verify.py | 78 ++ .../qq16-clifford-ring-obstruction/verify.py | 220 ++++ 11 files changed, 2334 insertions(+) create mode 100644 research/qq16-clifford-ring-obstruction/PROOF.md create mode 100644 research/qq16-clifford-ring-obstruction/README.md create mode 100644 research/qq16-clifford-ring-obstruction/RESULT.json create mode 100644 research/qq16-clifford-ring-obstruction/SOURCES.json create mode 100644 research/qq16-clifford-ring-obstruction/TASK.json create mode 100644 research/qq16-clifford-ring-obstruction/VERIFY.json create mode 100644 research/qq16-clifford-ring-obstruction/ring.py create mode 100644 research/qq16-clifford-ring-obstruction/source/PR2443-README.md create mode 100644 research/qq16-clifford-ring-obstruction/source/PR2546-README.md create mode 100644 research/qq16-clifford-ring-obstruction/test_verify.py create mode 100644 research/qq16-clifford-ring-obstruction/verify.py diff --git a/research/qq16-clifford-ring-obstruction/PROOF.md b/research/qq16-clifford-ring-obstruction/PROOF.md new file mode 100644 index 0000000000..b91245cd70 --- /dev/null +++ b/research/qq16-clifford-ring-obstruction/PROOF.md @@ -0,0 +1,149 @@ +# The retained QQ16 obstruction over normalized Clifford+T coefficients + +Let `D=Z[1/2]`, let `zeta=exp(pi*i/4)`, and set +`R=D[zeta]=Z[zeta,1/2]`. This note extends the **coefficient-ring boundary** +of Nick Petalas's [PR2546](https://github.com/CrocSwap/integer-mult-bounds/pull/2546), +pinned at `3aff4ccbfaa1005e5093e95535e4d99aa3813e54`. It reuses that work's +explicit witness. It does not supply a new unread-minor census or read lower bound. + +## Statement and fixed observations + +Use the unchanged conserved `F0/B_1_2` pair and exactly the two-cut observation +contract of starship-s's PR2443, with its unread set changed to +`H=[1,25,3,4,5,6,8,12]`. Grant these complete owner/payload arrays: + +1. `x1_A`, `x1_T`, `y1_A`, `y1_T` immediately after complete F0; +2. the 88 arrays `x1_(U\H)` at that same cut; +3. `y2_A` and `C=x2_U` immediately after B1, with no intervening modification. + +There are 224 granted arrays. Reading and retaining these observations may even +be free. There is no observation of `y2_U`, original selected inputs, or an +additional ordinary query. The selected sets A,T, ordinary set U and integer +query matrix R in the source are fixed. In this note the ring is also named R; +where a distinction is needed the query matrix is written `R_query`. + +**Theorem.** No fixed finite affine-linear circuit whose linear coefficients lie +in the ring `Z[zeta,1/2]` can recover all 224 original port arrays from these observations +for arbitrary original inputs. Arbitrary finite auxiliary workspace and affine +constants do not change the conclusion, when their initial values are the same +for the two inputs compared. Input-dependent advice or additional observations +are not part of this contract. + +This covers the explicit normalized gate alphabet H, S, T, X, Z, CNOT and SWAP, +their inverses, permutations, tensor products, direct sums, and scalar linear +ADDs/dyadic scalings. Here H is the normalized Hadamard, `S=diag(1,i)` and +`T=diag(1,zeta)`. Fixed phases generated by zeta are included; arbitrary global +phases are not asserted to belong to this ring. The theorem excludes an even +larger class of finite R-linear circuits, so no gate synthesis theorem is needed. + +## A proper ideal after adjoining the normalizations + +The cyclotomic relation is `zeta^4+1=0`; the polynomial is irreducible over Q +(substitute `x+1` and apply Eisenstein at 2). Consequently every ring element +has a unique expression `c0+c1*zeta+c2*zeta^2+c3*zeta^3`, with each `cj` dyadic. +Equivalently the ring is `D[x]/(x^4+1)`. + +Let `F25=F5[t]/(t^2-2)`. Two is not a square modulo five (the squares are +0,1,4), so this quotient is a field. There is a unital ring homomorphism + +```text +phi: D[zeta] -> F25, +phi(2^(-1))=3, phi(zeta)=4t=3/t. +``` + +Indeed `(4t)^2=2` and `(4t)^4=4=-1`, so the defining polynomial vanishes. +The integer map extends to D because two maps to a unit. In the unique basis, + +```text +phi(c0+c1*zeta+c2*zeta^2+c3*zeta^3) + = (c0+2*c2) + (4*c1+3*c3)*t (coefficients reduced modulo five). +``` + +In particular `phi(1)=1` and `phi(5)=0`. Thus `5R` is proper. We do not claim +that `5R` is the entire kernel of this particular specialization. + +The actual normalizing coefficients lie in the ring: + +```text +i=zeta^2, sqrt(2)=zeta-zeta^3, +1/sqrt(2)=(zeta-zeta^3)/2, zeta^(-1)=-zeta^3. +``` + +Their images are respectively `2,t,3t,2t`. In particular adjoining normalized +Hadamards has not made five invertible. The coefficient `1/sqrt(2)` has nonzero +odd basis coefficients, so it is outside the old Gaussian-dyadic subring D[i]. +This is a strict extension of the explicitly excluded class in PR2546. + +The specialization is **not assumed to preserve complex conjugation**. For +example, i maps to 2, while its complex conjugate -i maps to 3; every field +automorphism fixes these prime-field elements. Gate inverses are instead exact +ring identities before specialization: `H^2=I`, `S*S^(-1)=I`, +`T*T^(-1)=I`, and the named permutation gates are involutions. These identities +remain true under any ring homomorphism. No reduced-unitarity claim is used. + +## Source witness, with complete arbitrary-input boundary + +For this paragraph write the query matrix as `R_query`. The authenticated packet +gives `R_A R_A^T=R_T R_T^T=4I`. Put `P_A=R_A^T/4`, +`z=(1,2,1,1,1,1,3,-2)`, and `q=10e_1` (zero-indexed centre coordinate). +Direct multiplication gives `(R_query)_H z=q`. + +Choose every owner and payload entry of each port array constant, and initialize + +```text +x_U=iota_H z, x_A=-P_A q, x_T=0, +y_U=0, y_A= P_A q, y_T=0. +``` + +These are legitimate dyadic inputs, including nonzero selected dirt. The actual +cover maps are permutations of owner/payload addresses; hence they fix these +constant arrays. This is an input subspace of the original full-array contract, +not an assertion that arbitrary frames or arbitrary gates preserve constants. + +The full conserved F0 equations now give a zero first query and + +```text +x1_U=y1_U=iota_H z, +x1_A=x1_T=y1_A=y1_T=0. +``` + +The completed B1 future logger gives `y2_A=P_A q`, and its ordinary target +subtraction gives `C=x1_U-y1_U=0`. All 88 read coordinates vanish. In A order, + +```text +y2_A=(5/2,-5/2,0,5/2,0,0,-5/2,0). +``` + +Therefore every entry of every granted observation is in `5D`, hence in `5R`. +The original port `x_1` is the constant array one. These source witness equations +are credited to PR2546 and recomputed from the pinned packet; they are not new. + +Compare this input with the all-zero original input, using identical auxiliary +workspace and affine constants. The observation difference lies entrywise in +`5R`, and workspace differences are zero. Any R-linear gate, at any finite width, +maps vectors in this ideal to vectors in this ideal. This follows directly from +closure under finite sums and multiplication by R; induction proves it for the +whole circuit. Injecting/forgetting coordinates or permuting addresses also +preserves it. Constants cancel in the two executions, regardless of their values. +The required output difference at every coordinate of original `x_1` is one, +which cannot lie in `5R` because phi sends it to one. This contradiction proves +the theorem, without assuming that intermediate values remain constant arrays. + +## Positive and failure boundaries + +The old unread set `H0=[1,2,3,4,5,6,8,12]` still has a dyadic inverse. Its two +inverse orders are checked; this note does not obstruct that existing decoder. +The alternative H is invertible over Q with inverse entry `(0,1)=1/10`. Thus +the result is a coefficient restriction, not information loss over Q. Allowing +`1/5` invalidates the proper-ideal argument: `(1/5)*5=1`. + +The witness does not obstruct recovery of only the original selected inputs: +those inputs in this family are already determined dyadically by `y2_A`. +Nonlinear division, measurement/postselection and normalization, input-dependent +branching, additional observations, or a changed first pair require separate +analysis. Merely adjoining these explicit normalized Clifford+T coefficients +does not repair complete-input recovery at the fixed cut. + +No claim binds every available native frame or child operation to this alphabet. +Physical access, chronological retention, precision, native kernel costs, +all-size supplier admission and a full controller invoice remain open. diff --git a/research/qq16-clifford-ring-obstruction/README.md b/research/qq16-clifford-ring-obstruction/README.md new file mode 100644 index 0000000000..ad8b46baa4 --- /dev/null +++ b/research/qq16-clifford-ring-obstruction/README.md @@ -0,0 +1,98 @@ +# QQ16 obstruction with normalized Clifford+T coefficients + +The alternative unread set from [PR2546](https://github.com/CrocSwap/integer-mult-bounds/pull/2546) +still cannot support complete-input recovery when its decoder gains normalized +Hadamards and eighth-root phases. The new result extends that work's explicit +Gaussian-dyadic boundary to `Z[zeta_8,1/2]`; it reuses and credits its full-input +witness. No read minimum, minor census, native controller or supplier is claimed. + +## Result + +Keep the unchanged F0/B1 pair, all arbitrary original inputs, and exactly the +PR2443 two-cut observations with unread set `H=[1,25,3,4,5,6,8,12]`. +All 224 granted observation arrays in the inherited witness have every entry +divisible by five, but the required original port `x_1` is one. The proper ideal +persists in the larger ring: reduction to `F25=F5[t]/(t^2-2)` sends +`zeta_8 -> 4t`, `i -> 2`, `sqrt(2) -> t` and `1/sqrt(2) -> 3t`. + +[PROOF.md](PROOF.md) proves the ring homomorphism and ideal invariance under +every fixed finite linear circuit over that ring, including arbitrary finite +workspace with identical initial values in the two executions. Its explicit +gate subclass is H, S, T, X, Z, CNOT, SWAP, their inverses, tensor/direct sums, +permutations and dyadic linear operations. It does not assume the specialization +commutes with complex conjugation. Gate inverse identities are exact identities +before reduction. + +The original unread set `H0=[1,2,3,4,5,6,8,12]` remains a passing dyadic-inverse +control. The alternative has a rational inverse with entry `1/10`, so this is +not an information-loss result over Q. Allowing an odd-denominator gate such +as `1/5`, nonlinear division, postselection, additional observations or a changed +first pair lies outside the result. The displayed family does not obstruct +selected-only recovery. Binding a complete native alphabet, chronological access, +retention, precision and a favorable total invoice remain separate obligations. + +## Exact evidence + +The checker independently evaluates the literal constant-array F0/B1 equations +from the authenticated retained packet, without importing predecessor code. +[RESULT.json](RESULT.json) retains all 224 original input values +(112 X and 112 Y), all 224 observation values, both eight-by-eight +inverse matrices, the field specialization and seven gate-prefix vectors. +It checks 56 individual inverse basis columns and a complete mixed word return. +The normalized H prefix actually leaves the earlier Gaussian-dyadic subring. + +Six failure boundaries catch a wrong field relation, an odd denominator, +admission of inverse five, an omitted Hadamard normalization, a wrong phase +inverse and a changed unread witness. Separate export tests reject changed source +bytes, typed and semantic receipt changes and a missing receipt; an explicit +`--emit` mode prints a recomputation without writing package files. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -B scripts/research_package.py --package research/qq16-clifford-ring-obstruction +python3.12 -I -O -B research/qq16-clifford-ring-obstruction/verify.py +``` + +Expected primary output starts `PASS: source-bound 224 observations`. +[VERIFY.json](VERIFY.json) registers the primary checker and four export/control +groups. [SOURCES.json](SOURCES.json) pins main inputs by Git blob and SHA256 and +retains exact source READMEs for PR2546 at +`3aff4ccbfaa1005e5093e95535e4d99aa3813e54` and PR2443 at +`545c05e17243c962b112b91e7f84b4c1a41de7b8`. + +The standalone replay also works in a Git-free export with the listed source +files. Default replay writes no artifacts and keeps checks active under `-O`. +The source-bound finite checks support the written proof; they do not replace +its induction for arbitrary finite circuits. Python uses dynamic allocation and +arbitrary-size integers, a managed-runtime deviation from fixed allocation. +Replay dimensions are fixed at 112 ports, eight centre coordinates, four ring +basis coefficients and eight gate rows; source input sizes are bounded before +parsing. No floating-point arithmetic or external mathematical library is used. + +## Open next questions + +Does a concrete proposed native gate or frame leave this ring and actually +permit the odd denominator? First derive its exact coefficients at the real cut, +then check whether five remains a nonunit. The current result does not bind every +native primitive. Alternatively, use the already admissible H0 basis and price +its complete chronological reads, frame maps, retention and cleanup. Neither +route follows from scalar invertibility alone. [TASK.json](TASK.json) records +the changed task scope, overlap coverage and structured handoffs. + +## Credit + +Nick Petalas's PR2546 supplies the alternative unread set, modular full-input +witness and prior Gaussian-dyadic obstruction; its explicit normalized-Clifford +exclusion is the boundary resolved here. starship-s's PR2443 supplies the +arbitrary-input rational decoder and two-cut contract. Gareth Davidson's PR2432 +supplies the unread-column criterion and H0. Ali Romman and the retained QQ16 +contributors supply the packet, conserved maps and cover semantics. Earlier +compiler/supplier attribution remains in the unchanged +[QQ16 notice](../joint-query/NOTICE.md). + +Prepared by ywz65 with substantial OpenAI Codex assistance in mathematics, code, +checking and prose. New work is Apache-2.0. No human or proof-assistant +certification, native implementation or new kappa is claimed. diff --git a/research/qq16-clifford-ring-obstruction/RESULT.json b/research/qq16-clifford-ring-obstruction/RESULT.json new file mode 100644 index 0000000000..d071ac3af6 --- /dev/null +++ b/research/qq16-clifford-ring-obstruction/RESULT.json @@ -0,0 +1,1061 @@ +{ + "schema_version": 1, + "status": "PASS", + "ring": "Z[zeta8,1/2]", + "field": "F5[t]/(t^2-2)", + "specialization": { + "zeta8": [ + 0, + 4 + ], + "i": [ + 2, + 0 + ], + "sqrt2": [ + 0, + 1 + ], + "inverse_sqrt2": [ + 0, + 3 + ], + "inverse_zeta8": [ + 0, + 2 + ] + }, + "witness": { + "input_x": [ + "-5/2", + "1", + "0", + "1", + "1", + "1", + "1", + "5/2", + "3", + "0", + "0", + "0", + "-2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "2", + "0", + "-5/2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "5/2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + "input_y": [ + "5/2", + "0", + "0", + "0", + "0", + "0", + "0", + "-5/2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "5/2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-5/2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + "observation": [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "5/2", + "-5/2", + "0", + "5/2", + "0", + "0", + "-5/2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + "y2_A": [ + "5/2", + "-5/2", + "0", + "5/2", + "0", + "0", + "-5/2", + "0" + ], + "required_original_x_port1": "1" + }, + "inverses": { + "original": [ + [ + "-1/4", + "0", + "1/2", + "-1/4", + "-1/4", + "0", + "0", + "-1/4" + ], + [ + "5/4", + "1/2", + "-1/2", + "-1/4", + "-1/4", + "0", + "-1/2", + "1/4" + ], + [ + "-1/4", + "0", + "0", + "1/4", + "-1/4", + "0", + "1/2", + "1/4" + ], + [ + "-1/4", + "0", + "0", + "1/4", + "1/4", + "-1/2", + "0", + "-1/4" + ], + [ + "-1/4", + "0", + "0", + "1/4", + "1/4", + "1/2", + "0", + "-1/4" + ], + [ + "1/2", + "1/2", + "0", + "0", + "0", + "0", + "-1/2", + "1/2" + ], + [ + "-3/4", + "0", + "0", + "-1/4", + "1/4", + "0", + "1/2", + "-1/4" + ], + [ + "-1/4", + "-1/2", + "1/2", + "1/4", + "1/4", + "0", + "1/2", + "-1/4" + ] + ], + "alternative": [ + [ + "0", + "1/10", + "2/5", + "-3/10", + "-3/10", + "0", + "-1/10", + "-1/5" + ], + [ + "1/2", + "1/5", + "-1/5", + "-1/10", + "-1/10", + "0", + "-1/5", + "1/10" + ], + [ + "0", + "1/10", + "-1/10", + "1/5", + "-3/10", + "0", + "2/5", + "3/10" + ], + [ + "0", + "1/10", + "-1/10", + "1/5", + "1/5", + "-1/2", + "-1/10", + "-1/5" + ], + [ + "0", + "1/10", + "-1/10", + "1/5", + "1/5", + "1/2", + "-1/10", + "-1/5" + ], + [ + "-1/2", + "1/10", + "2/5", + "1/5", + "1/5", + "0", + "-1/10", + "3/10" + ], + [ + "0", + "3/10", + "-3/10", + "-2/5", + "1/10", + "0", + "1/5", + "-1/10" + ], + [ + "1/2", + "-1/5", + "1/5", + "1/10", + "1/10", + "0", + "1/5", + "-1/10" + ] + ] + }, + "gate_controls": { + "gates": [ + [ + "H", + 0, + null + ], + [ + "T", + 1, + null + ], + [ + "CNOT", + 0, + 2 + ], + [ + "S", + 2, + null + ], + [ + "X", + 1, + null + ], + [ + "Z", + 0, + null + ], + [ + "SWAP", + 0, + 2 + ] + ], + "inverse_columns": 56, + "prefixes": [ + [ + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "5/2", + "0", + "-5/2" + ], + [ + "0", + "5/4", + "0", + "-5/4" + ], + [ + "0", + "-5/4", + "0", + "5/4" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "-5/4", + "0", + "5/4" + ], + [ + "0", + "-5/4", + "0", + "5/4" + ] + ], + [ + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "5/2", + "0", + "-5/2" + ], + [ + "5/4", + "0", + "5/4", + "0" + ], + [ + "-5/4", + "0", + "-5/4", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "-5/4", + "0", + "-5/4", + "0" + ], + [ + "-5/4", + "0", + "-5/4", + "0" + ] + ], + [ + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "5/2", + "0", + "-5/2" + ], + [ + "5/4", + "0", + "5/4", + "0" + ], + [ + "-5/4", + "0", + "-5/4", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "-5/4", + "0", + "-5/4", + "0" + ], + [ + "-5/4", + "0", + "-5/4", + "0" + ] + ], + [ + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "5/2", + "0", + "-5/2" + ], + [ + "5/4", + "0", + "5/4", + "0" + ], + [ + "-5/4", + "0", + "-5/4", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "5/4", + "0", + "-5/4", + "0" + ], + [ + "5/4", + "0", + "-5/4", + "0" + ] + ], + [ + [ + "5/4", + "0", + "5/4", + "0" + ], + [ + "-5/4", + "0", + "-5/4", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "5/2", + "0", + "-5/2" + ], + [ + "5/4", + "0", + "-5/4", + "0" + ], + [ + "5/4", + "0", + "-5/4", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0" + ] + ], + [ + [ + "5/4", + "0", + "5/4", + "0" + ], + [ + "5/4", + "0", + "5/4", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "-5/2", + "0", + "5/2" + ], + [ + "5/4", + "0", + "-5/4", + "0" + ], + [ + "-5/4", + "0", + "5/4", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0" + ] + ], + [ + [ + "5/4", + "0", + "5/4", + "0" + ], + [ + "5/4", + "0", + "-5/4", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "5/4", + "0", + "5/4", + "0" + ], + [ + "-5/4", + "0", + "5/4", + "0" + ], + [ + "0", + "-5/2", + "0", + "5/2" + ], + [ + "0", + "0", + "0", + "0" + ] + ] + ] + }, + "failure_controls": [ + "wrong field relation", + "odd denominator rejected", + "inverse five admits unit", + "omitted H normalization", + "wrong phase inverse", + "changed unread witness" + ] +} diff --git a/research/qq16-clifford-ring-obstruction/SOURCES.json b/research/qq16-clifford-ring-obstruction/SOURCES.json new file mode 100644 index 0000000000..60c76305a8 --- /dev/null +++ b/research/qq16-clifford-ring-obstruction/SOURCES.json @@ -0,0 +1,57 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/joint-query/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/joint-query/evidence/CONSERVED-QQ16.md", + "usage": "input", + "git_blob": "4639583c1be02c2fb60ed8a8072c9969ef1569ce", + "sha256": "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb" + }, + { + "path": "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "usage": "input", + "git_blob": "a6805c58f23132f9420efebf90f5b7e863c2e179", + "sha256": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75" + } + ], + "retained_documents": [ + { + "path": "research/qq16-clifford-ring-obstruction/source/PR2546-README.md", + "source_path": "research/qq16-dyadic-unread-minors/README.md", + "source_commit": "3aff4ccbfaa1005e5093e95535e4d99aa3813e54", + "source_url": "https://github.com/CrocSwap/integer-mult-bounds/blob/3aff4ccbfaa1005e5093e95535e4d99aa3813e54/research/qq16-dyadic-unread-minors/README.md", + "usage": "retained contract, proof and attribution; no predecessor executable imported", + "git_blob": "caafa962ce3365d94f5ea156490f25352399cd1b", + "sha256": "732490db14d5bd317e414b99cb79a6abfab76c89256282cddeed3703e5c57e75" + }, + { + "path": "research/qq16-clifford-ring-obstruction/source/PR2443-README.md", + "source_path": "research/qq16-coordinate-cut-decoder/README.md", + "source_commit": "545c05e17243c962b112b91e7f84b4c1a41de7b8", + "source_url": "https://github.com/CrocSwap/integer-mult-bounds/blob/545c05e17243c962b112b91e7f84b4c1a41de7b8/research/qq16-coordinate-cut-decoder/README.md", + "usage": "retained contract, proof and attribution; no predecessor executable imported", + "git_blob": "1ae3d3eb976ed85f795da2c211b58577ed7e8a82", + "sha256": "91d68f5d01d89ee78802ee5f76e8b901199a686aaa62341090eb70c458fd070e" + } + ], + "packet_payload_sha256": "2efe83c59978aa9c0db2c3e4eccc14cbfdcd3c9ce499432601b5dd34083472ef" +} diff --git a/research/qq16-clifford-ring-obstruction/TASK.json b/research/qq16-clifford-ring-obstruction/TASK.json new file mode 100644 index 0000000000..a061382209 --- /dev/null +++ b/research/qq16-clifford-ring-obstruction/TASK.json @@ -0,0 +1,160 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "joint-query-controller", + "question": "Can one explicitly changed QQ16 interface recover the missing chart query and close a two-call controller within a favorable full budget?", + "starting_points": [ + "research/joint-query/README.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Add one explicitly priced ordinary-to-selected observation and derive the ordered two-call map and inverse.", + "Change the first local pair or retained state, then test the existing lost-observation witness and price all new operations." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the fixed-first-pair QQ16 witness before designing a controller. The checked #1969 local words do not evade that witness or supply global placement.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Apply the existing witness to one proposed extra observation or changed first pair. If it still loses the required record, stop. Otherwise derive one ordered two-call identity and charge the added read, chart maps and restoration before extending to more stages.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969" + ] + }, + "scope_status": "changed", + "actual_scope": "Extend PR2546 fixed full-input QQ16 unread-set obstruction from Gaussian-dyadic coefficients to Z[zeta8,1/2], including explicitly normalized Clifford+T gates.", + "scope_change_reason": "The drawn coverage-law and connector-alphabet starting cases were already covered by the local ceiling proof and existing scalar/interface handoffs. A bounded joint-query pivot addresses PR2546 explicitly excluded normalized Clifford coefficients, without another minor census or controller claim.", + "bottleneck_link": "Side result on decoder coefficient admission: adding normalized Hadamard and eighth-root phases cannot repair this exact complete-input recovery contract. Native cost and physical retention remain independent obligations.", + "budget_minutes": 60, + "stop_rule": "Stop after a proper-ideal proof with explicit F25 specialization, source-bound full-input witness, named gate/inverse controls and unchanged-basis positive control. Do not extend the minor census or infer native/supplier admission.", + "outcome": "negative-result", + "evidence": "PROOF.md proves the ring extension and ideal invariance at every finite width. RESULT.json records 224 observations, both source-minor inverses, seven named gate controls and six failure boundaries; verify.py rederives these from authenticated sources.", + "author": "ywz65 with OpenAI Codex", + "ai_assistance": "Substantial OpenAI Codex assistance with derivation, implementation, prose and exact checks. Independent AI-assisted peer review requested; no human or proof-assistant certification claimed.", + "open_questions": [ + { + "question": "Does a concrete additional native gate or frame leave Z[zeta8,1/2] and permit the odd denominator required at this fixed cut?", + "why_it_matters": "The present result closes the explicitly normalized Clifford+T extension but does not classify every native primitive.", + "first_step": "Pin the proposed gate at the actual input/output cut, derive its exact coefficients, and check whether five remains a nonunit before attempting a decoder.", + "blocked_by": "No complete native alphabet binding, retention implementation or full controller budget is supplied." + }, + { + "question": "Can an existing dyadic-unit unread basis yield a favorable complete native read/retention invoice?", + "why_it_matters": "The original H0 basis remains algebraically admissible.", + "first_step": "Use the credited dyadic inverse and bind legal chronological reads, endpoint maps and cleanup to an actual native host.", + "blocked_by": "Algebraic admissibility alone does not establish physical access, precision or supplier admission." + } + ], + "scope_key": "qq16/full-input/unread-1-25-3-4-5-6-8-12/normalized-clifford-ring", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2546#issuecomment-6196493106", + "selection": { + "seed": "2eba63bd19421f2b60de315da4df72f8", + "track": "recursive-interfaces", + "initial_cards": [ + "coverage-law-change", + "connector-alphabet-change", + "joint-query-controller" + ], + "baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; complex-local-word-ceiling baseline passed" + }, + "freshness": { + "checked_utc": "2026-10-15T16:23:24.210760+00:00", + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "source_heads": [ + { + "pr": 2546, + "head": "3aff4ccbfaa1005e5093e95535e4d99aa3813e54", + "state": "open" + }, + { + "pr": 2443, + "head": "545c05e17243c962b112b91e7f84b4c1a41de7b8", + "state": "open" + } + ], + "latest100_hits": [ + { + "number": 2599, + "title": "Prove sharp binary-stream faithfulness thresholds", + "head": "cfafdd633cf4e2e534704ec3ddd684cb0c32734f" + }, + { + "number": 2598, + "title": "Prove native payload dimension for owner-local centre repairs", + "head": "f6ec9e47781071fe665445afbdffd7312c039593" + }, + { + "number": 2580, + "title": "Kernel-check the HPE component-bound packed comparator", + "head": "a11c16a71336d9d0cd1cae414c50e8c93f808c1f" + }, + { + "number": 2551, + "title": "Distinguish P104 physical and backward-chart dual contracts", + "head": "249c4034da118da35f1e6009744b81461172bc61" + }, + { + "number": 2546, + "title": "Research: audit dyadic admission of QQ16 unread minors", + "head": "3aff4ccbfaa1005e5093e95535e4d99aa3813e54" + }, + { + "number": 2534, + "title": "Execute Compact around an actual selected complex child", + "head": "f961dcb12061c3959058aed883f48b55f365eb80" + }, + { + "number": 2532, + "title": "Audit (no \u03ba): #2297/#2041 k-group port decoders are not scalar decoders \u2014 6,608 parity-forced forbidden entries; k=5 needs a diagonal rank-112 map; 2-integral floor 554/334 exceeds every saving threshold", + "head": "bcb6f278503bd2a6b3ffb9bdcfcda9f36c18d2f4" + }, + { + "number": 2530, + "title": "Conditional \u03ba \u2248 0.0017137379215475043 from source-partner lifetimes and physical rehosting", + "head": "b4012098048e12500b2d33d2e84be281915a27ac" + }, + { + "number": 2516, + "title": "Attain the sharp nonreciprocal Clifford correction rank", + "head": "9d1c93bcb5ab77d92c316f144f6e2c3a92ae5d03" + } + ], + "targeted_comment_count": 2, + "discussion_coverage": "Complete cached1197-discussion snapshot 2026-10-15T12:29:05Z; no full new Discussion pagination. Targeted source comments and latest100 PRs refreshed; no claim of exhaustive novelty.", + "competing_claim": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2546#issuecomment-6196885408", + "scope": "Later independent ywz65 task claims the same coefficient-ring extension plus a source-bound P/X/D/PH/C native alphabet audit.", + "coordination": "Our earlier6196493106 investigation completed the ring theorem and independent peer review; native alphabet binding is invited as a complementary followup. The shared scalar extension is one result, not a second novelty claim." + } + }, + "validation": { + "CPython3.12.7": "Registered primary optimized replay and four export/control groups PASS", + "CPython3.14.5": "Direct optimized primary and four export/control groups PASS", + "independent_review": "Separate AI-assisted C review passed full224x224 modular observation maps and exact gates in Q(i,sqrt2), with no candidate imports; final head binding pending." + } +} diff --git a/research/qq16-clifford-ring-obstruction/VERIFY.json b/research/qq16-clifford-ring-obstruction/VERIFY.json new file mode 100644 index 0000000000..5a8a46f0da --- /dev/null +++ b/research/qq16-clifford-ring-obstruction/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/CONSERVED-QQ16.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact source pins, F25 homomorphism basis, fixed two-cut full-input witness, positive inverse, explicit gate inverses and six failure controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Four Git-free export groups: no writes, source corruption, typed/semantic receipt corruption, missing receipt and explicit emission." + } + ] +} diff --git a/research/qq16-clifford-ring-obstruction/ring.py b/research/qq16-clifford-ring-obstruction/ring.py new file mode 100644 index 0000000000..40f1833734 --- /dev/null +++ b/research/qq16-clifford-ring-obstruction/ring.py @@ -0,0 +1,82 @@ +"""Exact D[zeta_8] arithmetic and its F25 specialization; no floats.""" +from fractions import Fraction as Q + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def add(a, b): + return tuple(x + y for x, y in zip(a, b)) + + +def neg(a): + return tuple(-x for x in a) + + +def mul(a, b): + out = [Q(0)] * 4 + for i, x in enumerate(a): + for j, y in enumerate(b): + out[(i + j) % 4] += x * y * (-1 if i + j >= 4 else 1) + return tuple(out) + + +def scalar(value): + return (Q(value), Q(0), Q(0), Q(0)) + + +ZERO, ONE = scalar(0), scalar(1) +ZETA = (Q(0), Q(1), Q(0), Q(0)) +I = mul(ZETA, ZETA) +ZETA3 = mul(I, ZETA) +SQRT2 = add(ZETA, neg(ZETA3)) +HALFROOT = mul(scalar(Q(1, 2)), SQRT2) + + +def fmul(a, b, square=2): + return ((a[0]*b[0] + square*a[1]*b[1]) % 5, + (a[0]*b[1] + a[1]*b[0]) % 5) + + +def dyadic(value): + return value.denominator & (value.denominator - 1) == 0 + + +def reduce(value): + need(len(value) == 4 and all(dyadic(v) for v in value), + "dyadic coefficient required") + c = [v.numerator * pow(v.denominator, -1, 5) % 5 for v in value] + return ((c[0] + 2*c[2]) % 5, (4*c[1] + 3*c[3]) % 5) + + +def gate(values, operation, bit, other=None, inverse=False, normalizer=HALFROOT): + """Literal fixed three-bit gate, acting on eight coefficient rows.""" + need(len(values) == 8 and bit in range(3), "three-bit gate domain") + need(operation in ('H', 'S', 'T', 'X', 'Z', 'CNOT', 'SWAP'), "gate name") + values = values[:] + if operation == 'H': + for j in range(8): + if not j >> bit & 1: + k = j ^ (1 << bit) + a, b = values[j], values[k] + values[j] = mul(normalizer, add(a, b)) + values[k] = mul(normalizer, add(a, neg(b))) + elif operation in ('T', 'S', 'Z'): + phase = {'T': ZETA, 'S': I, 'Z': scalar(-1)}[operation] + if inverse: + phase = {'T': neg(ZETA3), 'S': neg(I), 'Z': scalar(-1)}[operation] + values = [mul(phase, v) if j >> bit & 1 else v for j, v in enumerate(values)] + else: + need(operation == 'X' or other in range(3) and other != bit, + "distinct controlled/permuted bits") + out = [ZERO] * 8 + for j, v in enumerate(values): + if operation == 'SWAP': + k = j ^ ((1 << bit) | (1 << other)) if ((j >> bit) ^ (j >> other)) & 1 else j + else: + k = j ^ (1 << bit) if operation == 'X' or j >> other & 1 else j + out[k] = v + values = out + return values diff --git a/research/qq16-clifford-ring-obstruction/source/PR2443-README.md b/research/qq16-clifford-ring-obstruction/source/PR2443-README.md new file mode 100644 index 0000000000..1ae3d3eb97 --- /dev/null +++ b/research/qq16-clifford-ring-obstruction/source/PR2443-README.md @@ -0,0 +1,213 @@ +# QQ16 coordinate decoding with two retained cuts + +**Scoped ordered proof; no supplier or new kappa.** For the unchanged conserved +`F0/B_1_2` pair, 88 ordinary coordinate arrays suffice to recover **all original +pair-0 inputs**, provided the selected fields and completed-X block listed below +are available at the two specified cuts. The inputs may be arbitrary, not just +members of the eight local-axis families tested by +[PR2432](https://github.com/CrocSwap/integer-mult-bounds/pull/2432). + +This answers a restricted version of PR2432's next question. It does **not** +show that the final controller exposes these cut values, that retaining them +is free, or that 88 reads are a favorable physical implementation. It supplies +an explicit decoder once those observations are granted. + +## Exact observation contract + +Write `(x1,y1)=F0(x,y)` and `(x2,y2)=B_1_2(x1,y1)`, with no intervening +modification. Use the retained disjoint selected sets + +```text +A = [0,7,20,27,36,46,57,111] +T = [21,37,47,76,81,87,92,110] +U = {0,...,111} \ (A union T) +J = [1,2,3,4,5,6,8,12] +S = U \ J +``` + +The decoder receives only: + +- `x1_A`, `x1_T`, `y1_A`, `y1_T`, retained immediately after complete F0; +- `y2_A` and the completed-X ordinary block `C=x2_U`, immediately after B1; +- `x1_S`, the 88 ordinary arrays read after F0. + +An array includes its complete owner and payload coordinates. Reads are +side-effect-free. No original selected input, initial dense ordinary query, +`y2_U`, or former-Y final endpoint is an observation. This is a two-cut +information contract, not a bound of 88 total stored arrays: the selected +records and the complete `C` block are additional granted observations. +Other bank pairs can have arbitrary initial values; they do not participate +in these first two events. No recovery claim for those other pairs is made. + +## Ordered proof + +All equations are over rational-valued owner/payload arrays. Let `D_(s,p)` be +the actual invertible cover map for port p in chart s. The scalar centre matrix +is R. For a port set V, write + +```text +B_(s,V) z = sum_(p in V) r_p D_(s,p) z_p +B_s = B_(s,U) +ell_(s,V) = B_(s,V), for V=A or T +P_(s,V) q = D_(s,V)^(-1) R_V^(-1) q, for V=A or T. +``` + +Here `D_(s,V)` is block diagonal in ports; its entries are operators, not +commuting scalar coefficients. The actual selected Grams are +`R_A R_A^T = R_T R_T^T = 4I`, so `R_V^(-1)=R_V^T/4`. +The source normalization is `K=R^T/4`; its routed restriction to U is `K_(s,U)`. +These are the conserved maps in the retained +[ordered contract](../joint-query/evidence/JOINT-QUERY-TRANSFER.md), sections +“A variant that preserves both selected pair sums” and +“A forward map with the same conserved inputs.” + +### Recover the missing post-F0 ordinary arrays + +The forward equations give + +```text +f = R_0 x +x1_U = x_U - K_(0,U) f +y1_U = y_U + x1_U +x1_A = P_(0,A) ell_(0,T) x_T +x1_T = P_(0,T) f. +``` + +The backward U target is an exact subtraction. Its future logger changes +only A, and its source output at A is that logger's output. Consequently, + +```text +C = x2_U = x1_U - y1_U = -y_U +q = ell_(2,A) (y2_A - y1_A) + = B_2 y1_U + ell_(2,T) y1_T +v = q - ell_(2,T) y1_T + B_2 C + = B_2 x1_U. +``` + +Every expression on the left is determined by the allowed observations. +Subtract the known coordinates: + +```text +w = v - B_(2,S) x1_S + = R_J D_(2,J) x1_J. +``` + +The actual rational `R_J` is invertible. The checker derives its inverse +from the pinned R, verifies both inverse orders, and records the matrices in +[RESULT.json](RESULT.json). Thus + +```text +x1_J = D_(2,J)^(-1) (R_J^(-1) w). +``` + +The order is essential: first apply the scalar inverse, then undo each +port's cover map. Moving the different port maps through `R_J^(-1)` is not +valid. This step recovers all of `x1_U`, with no hypothesis on how its +owner or payload values were generated. + +### Recover the original inputs + +Use the selected sections and the recovered ordinary block: + +```text +f = ell_(0,T) x1_T +t = P_(0,T) ell_(0,A) x1_A +x_U = x1_U + K_(0,U) f +x_T = t +x_A = P_(0,A) (f - B_0 x_U - ell_(0,T) t) +y_U = -C +y_V = x1_V + y1_V - x_V, V=A,T. +``` + +The first two formulas invert the two selected forward records. The third +inverts its ordinary update. The fourth and fifth recover the selected +components of `R_0 x=f`. Finally, the unchanged selected pair sums recover +the original Y values. Therefore this decoder composed with the stated +observation map is the identity on all 224 original port arrays. + +This is an ordered algebraic argument for arbitrary arrays under the inherited +local contract. The finite fixtures below check its source-specific premises +and implementation; they are not the proof of the arbitrary-array statement. + +## Evidence and reproduction + +From the repository root, with Python 3.12 and its standard library: + +```sh +python3.12 scripts/research_package.py --package research/qq16-coordinate-cut-decoder +``` + +The registered commands run the direct check and the optimized replay and +source-corruption controls. Direct entry point: + +```sh +python3.12 -I -B research/qq16-coordinate-cut-decoder/verify.py +``` + +Expected status: `PASS_QQ16_COORDINATE_CUT_DECODER`. + +The check binds the actual packet, two archive members, the first F0/B1 events, +selected Grams, `K=R^T/4`, the two-sided unread-minor inverse, and 224 registered +port-route/inverse pairs, including their payload-translation inverse equations. +It implements the conserved logical maps directly, rather than executing the +native words or importing a predecessor verifier. + +Finite execution covers each of the 224 input-port placements using nonconstant +owner bit-functions and one dense signed/dyadic fixture with every field dirty. +All five incorrect decoders have explicit nonzero residuals: wrong C sign, +missing future-T subtraction, missing old-A subtraction, missing forward K +correction, and reversed route/scalar inverse order. Each of the five external +source-file corruptions is rejected. Checks remain active under `-O`, and the +optimized replay must match the committed result without modifying package files. + +The finite functions are constant in payload. The universal proof uses the +inherited invertibility of the full cover maps, not an extrapolation from these +functions. Native kernels, the remaining 17 schedule events, a proof assistant, +and the selected full cold replay were not run. + +## Relation to earlier work and limits + +- Gareth Davidson's [PR2432](https://github.com/CrocSwap/integer-mult-bounds/pull/2432), + pinned at `cbede349fc764aa38379aa533befe3215916cfcd`, supplies the unread basis + and the eight-family threshold. This package adds arbitrary-input sufficiency + under the explicit two-cut contract. It does not reprove the threshold or + claim a new unrestricted read minimum. +- commdata2338's [PR2174](https://github.com/CrocSwap/integer-mult-bounds/pull/2174), + pinned at `f79470a7931f3943360c10d15b428e0e4e479c22`, uses two initial dense + queries and a post-B1 selected cut to recover pair-0 selected inputs. It + reconstructs a transient F0 record which this package explicitly retains. + The observation and retention contracts differ; neither cost nor controller + superiority follows from this comparison. +- commdata2338's PR2384 exact `Model.forward/backward` implementation, as + retained by PR2432, was consulted. Its owner-function representation informed + the finite checker; no predecessor executable is imported or vendored. +- Ali Romman / PR1969 supplies the conserved maps, native contract and cover + semantics. Adam Gall / PR2093, kyzer1023 / PR2354, PR2389 and its PR2419 audit + supply the hidden-family and coordinate-read lineage. The retained Rohan Arun, + Jeremy Kothe, DreamingOfClouds and supplier contributors retain their credit. + +No read, storage, chart-map, cleanup, hosting, precision, tape or recursive-child +cost is certified here. In particular, the `B_2 C` read must be legal at the +completed-X type; an algebraic formula alone does not establish that access. +The selected frontier and frozen predecessors are unchanged. + +Base and exact input pins are in [SOURCES.json](SOURCES.json); scope and overlap +are in [TASK.json](TASK.json). Coordination: +[Discussion 2424](https://github.com/CrocSwap/integer-mult-bounds/discussions/2424#discussioncomment-18946004). +New work is Apache-2.0, submitted by `starship-s` with substantial assistance from +Hermes Agent (`gpt-6-astra-900k`: derivation and proof) and Codex +(`gpt-6-astra`, max effort: implementation and review). No independent human or +proof-assistant verification is claimed. + +## Open next questions + +1. **Can an actual controller retain or reconstruct these two-cut records?** + This is necessary to turn the information lemma into a usable decoder. + First trace `x1_A/T`, `y1_A/T`, `y2_A` and `C` through the remaining schedule, + with their native endpoint types. The blocker is legal retention and access, + not the local inverse. +2. **Does a fully charged implementation have a favorable budget?** + First price the 88 reads, `B_2 C`, scalar minor inversion, per-port chart + maps, storage and cleanup together. No physical implementation or favorable + complete bill has been supplied; stop this route if even its optimistic bill + misses the declared supplier target. diff --git a/research/qq16-clifford-ring-obstruction/source/PR2546-README.md b/research/qq16-clifford-ring-obstruction/source/PR2546-README.md new file mode 100644 index 0000000000..caafa962ce --- /dev/null +++ b/research/qq16-clifford-ring-obstruction/source/PR2546-README.md @@ -0,0 +1,181 @@ +# Dyadic admission of QQ16 unread minors + +This is a scoped scalar-admission result submitted for review, not a supplier +or a new kappa. + +The unread basis used by [PR2443](https://github.com/CrocSwap/integer-mult-bounds/pull/2443), +`H0=[1,2,3,4,5,6,8,12]`, has determinant `-32` and a dyadic inverse. It passes the +check below. However, replacing just unread port 2 by port 25 gives a rationally +invertible minor with determinant `-80` and inverse entry `1/10`. That read set +cannot support a finite dyadic-linear decoder for all original inputs under the +same two-cut observations, even when access and retention are free. + +This does not contradict PR2443. Its specific basis is dyadic, its theorem is +rational, and it does not claim native execution. The new contribution is the +explicit alternative-set obstruction and a complete local census, useful before +optimizing which ports to leave unread. + +## Domain and result + +Use the actual integer `8 x 112` query matrix R and ordinary set U96 from the +retained [QQ16 packet](../joint-query/README.md). For an unread set H of size eight, +consider exact inversion of + +```text +w = R_H D_(2,H) x1_H, +x1_H = D_(2,H)^(-1) R_H^(-1) w. +``` + +The order is the one in PR2443. Each port's cover map must be undone after scalar +inversion. No commutation of the different port maps is assumed. + +Let `D=Z[1/2]`. An integer square matrix is invertible over D if and only if its +determinant is a unit of D, namely a signed power of two. Sufficiency follows +from the adjugate formula. Necessity follows by taking determinants of a left +inverse. Thus nonsingularity alone is insufficient for dyadic scalar admission. +The same odd-factor obstruction holds with Gaussian-dyadic coefficients. + +The exact census includes every unread set at exchange distance at most two +from H0. No random sampling is used. + +| Distance | Sets | Singular | Dyadic-unit determinant | Nonzero odd-factor determinant | +| --- | ---: | ---: | ---: | ---: | +| 0 | 1 | 0 | 1 | 0 | +| 1 | 704 | 185 | 485 | 34 | +| 2 | 107184 | 46180 | 58537 | 2467 | +| Total | 107889 | 46365 | 59023 | 2501 | + +The nonzero absolute determinants are `16,32,48,64,80,96`. The odd-factor values +are `48,80,96`. [RESULT.json](RESULT.json) contains every histogram, both complete +inverses and the counterexample. This is not a census of all eight-subsets of U96. +A unit determinant admits the scalar inverse, not a native read or a favorable bill. + +## A counterexample for the complete two-cut decoder + +The observation contract is exactly PR2443's. Retain `x1_A/T`, `y1_A/T` after +complete F0, read `x1_(U\H)` there, and retain `y2_A` and `C=x2_U` immediately +after B1. There is no intervening modification. No `y2_U` or additional original +input is observed. Here A and T are the retained selected sets. + +Use this order for the alternative unread ports and integer vector: + +```text +H = [1,25,3,4,5,6,8,12], +z = [1,2,1,1,1,1,3,-2]. +``` + +Exact multiplication gives `R_H z=10 e_1`, where centre coordinates are zero-indexed. +Set all owner and payload values constant, so every cover map acts as the identity. +Writing `P_A=R_A^T/4` and `q=10 e_1`, initialize + +```text +x_U = iota_H z, x_A = -P_A q, x_T = 0, +y_U = 0, y_A = P_A q, y_T = 0. +``` + +These are valid dyadic inputs, including the selected dirt. Since `R_A P_A=I`, +the first forward query is zero. The conserved F0 equations give + +```text +x1_U = y1_U = iota_H z, +x1_A = x1_T = y1_A = y1_T = 0. +``` + +At B1, its future logger gives `y2_A=P_A q` and its ordinary target subtraction +gives `C=0`. All 88 read coordinates vanish. Hence all allowed observations are +zero except `y2_A=(5/2) R_A^T e_1`. Every observed coordinate belongs to the ideal +`5D`, but the required original `x_1` equals 1. + +A finite D-linear circuit preserves `5D`. Therefore no such circuit can decode +all original inputs from these observations. The argument also covers finite +Gaussian-dyadic linear operations and owner permutations. The ideal `5D[i]` is +proper, as reduction modulo five with `i -> 2` maps 1 to 1 and five to zero. Extra dirty workspace or affine constants do not help a linear +implementation: compare the displayed input with the zero input using identical +workspace and subtract the two executions. The observation difference stays in +the ideal while the required output difference is 1. + +A frame change is covered only if its coefficients are separately shown to lie +in the proved ring. Normalized Clifford coefficients such as `1/sqrt(2)` are +outside `D[i]` and are not covered here. No binding of the complete native gate +alphabet to this ring is supplied, and no claim that all native operations are +Gaussian-dyadic is made. + +This is not an information-loss witness over Q. The rational inverse exists, +and its row 0, column 1 entry is `1/10`. Nor is it an obstruction to restoring +only the selected original inputs. In this displayed family those selected +inputs are already determined dyadically by `y2_A`. The claim concerns complete +input recovery, as in PR2443, under the fixed observations and coefficient ring. +Nonlinear exact integer division, odd-denominator gates, new observations or a +changed first pair are outside the result. + +## Reproduce + +Python 3.12 or later, standard library only: + +```sh +python3.12 -I -B scripts/research_package.py --package research/qq16-dyadic-unread-minors +python3.12 -I -O -B research/qq16-dyadic-unread-minors/verify.py +``` + +The registered replay checks source pins and runs: + +- `verify.py`, using the one-/two-column determinant lemma, exact Fraction + elimination, two inverse orders and the constant-owner two-cut witness; +- `oracle.py`, importing no primary verifier or pending PR code, using direct + fraction-free elimination on all 107889 matrices and adjugate cofactors for + both inverses; +- `test_verify.py`, checking optimized replay, a Git-free source export and + rejection of source corruption, receipt type corruption, a missing receipt + and an altered histogram. + +The six mathematical controls include a singular minor, a wrong inverse sign, +an odd denominator, treating every nonzero determinant as a dyadic unit, a +changed modular vector and a duplicate unread port. Default replay writes no +artifacts. `verify.py --emit` explicitly emits a new complete receipt to stdout. + +[SOURCES.json](SOURCES.json) pins retained main inputs at +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. Pending PRs are attribution and +contract context, not runtime dependencies. Native replay, chronological +retention, child hosting, precision, tape, all-size admission and the complete +supplier invoice are not established. The separate retained QQ16 local replay +was run as a baseline, not as verification of a new native decoder. + +## Engineering limits + +All loops have fixed finite domains: matrix dimension at most eight, 112 ports, +and 107889 streamed candidates. Python uses dynamic allocation and arbitrary-size +integers. This is a managed-runtime deviation from fixed steady-state allocation. +The exact hash-bound source, fixed matrix sizes and streamed census bound live +state; no list of all candidates is retained. Parser sizes are checked before +hashing/decompression. Functions stay below 60 physical lines. Direct and +optimized replays, warning-enabled tests and a second determinant algorithm are +the available interpreted-code checks. A future broader domain must add explicit +input bounds and recheck resource limits rather than reuse this bounded receipt. + +## Open next questions + +Can a dyadic-unit unread basis reduce a complete native decoder's cost? First +for a dyadic-linear implementation, filter candidate read sets by the determinant +gate, then compare actual endpoint frames and the full read, chart-map, retention +and cleanup invoice. The blocker +is physical access and sustainable retention, not nonsingularity. The original +PR2443 basis already passes the dyadic check. No broader search is justified by +this finite census alone. [TASK.json](TASK.json) records the structured handoff. + +## Credit + +Gareth Davidson's PR2432 supplies the unread-column criterion and H0, pinned at +`cbede349fc764aa38379aa533befe3215916cfcd`. starship-s's PR2443 supplies the +arbitrary-input rational decoder and explicit two-cut contract, pinned at +`545c05e17243c962b112b91e7f84b4c1a41de7b8`. thakrarsagar's PR2470, +`1b2eee3bf1ec67e68c0b0fa7f47c7b2a66febe56`, is the separate retention census. +None is adopted as a supplier or represented as independently reviewed here. + +Ali Romman and the retained QQ16 contributors supply the matrix, selected +sections, conserved maps and cover semantics. Adam Gall, commdata2338, +kyzer1023 and the coordinate-read predecessors retain their information-bound +credit. Rohan Arun, Jeremy Kothe, DreamingOfClouds and the earlier supplier and +compiler lineage retain their attribution through the unchanged +[QQ16 notice](../joint-query/NOTICE.md). No predecessor executable is imported or +vendored. New work is Apache-2.0. No independent human or proof-assistant review +is claimed. diff --git a/research/qq16-clifford-ring-obstruction/test_verify.py b/research/qq16-clifford-ring-obstruction/test_verify.py new file mode 100644 index 0000000000..545937c82f --- /dev/null +++ b/research/qq16-clifford-ring-obstruction/test_verify.py @@ -0,0 +1,78 @@ +"""Entry-point controls in an isolated Git-free export.""" +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +PKG = Path(__file__).resolve().parent +ROOT = PKG.parents[1] +REL = PKG.relative_to(ROOT) + + +def run(root, *args): + return subprocess.run([sys.executable, '-I', '-O', '-B', str(root / REL / 'verify.py'), *args], + cwd=root, capture_output=True, text=True, timeout=45) + + +class ExportTests(unittest.TestCase): + def setUp(self): + self.temp = tempfile.TemporaryDirectory() + self.root = Path(self.temp.name) + shutil.copytree(PKG, self.root / REL, ignore=shutil.ignore_patterns('__pycache__')) + manifest = json.loads((PKG / 'SOURCES.json').read_text()) + for row in manifest['files']: + path = self.root / row['path'] + path.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / row['path'], path) + self.pkg = self.root / REL + + def tearDown(self): + self.temp.cleanup() + + def test_export_and_no_writes(self): + def snapshot(): + return {str(p.relative_to(self.root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in self.root.rglob('*') if p.is_file()} + before = snapshot() + completed = run(self.root) + self.assertEqual(completed.returncode, 0, completed.stderr) + self.assertEqual(before, snapshot()) + + def test_source_corruption(self): + path = self.root / 'research/joint-query/certificate.json.gz' + path.write_bytes(path.read_bytes() + b'corrupt') + completed = run(self.root) + self.assertNotEqual(completed.returncode, 0) + self.assertIn('source SHA256', completed.stderr) + + def test_typed_receipt_and_semantics(self): + path = self.pkg / 'RESULT.json' + original = path.read_bytes() + for mutation in ('type', 'witness', 'gate'): + value = json.loads(original) + if mutation == 'type': + value['schema_version'] = True + elif mutation == 'witness': + value['witness']['required_original_x_port1'] = '0' + else: + value['gate_controls']['prefixes'][0][1][1] = '0' + path.write_text(json.dumps(value)) + completed = run(self.root) + self.assertNotEqual(completed.returncode, 0, mutation) + self.assertIn('exact typed receipt', completed.stderr) + + def test_missing_receipt_and_explicit_emit(self): + (self.pkg / 'RESULT.json').unlink() + self.assertNotEqual(run(self.root).returncode, 0) + emitted = run(self.root, '--emit') + self.assertEqual(emitted.returncode, 0, emitted.stderr) + self.assertEqual(json.loads(emitted.stdout), json.loads((PKG / 'RESULT.json').read_text())) + self.assertFalse((self.pkg / 'RESULT.json').exists()) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/qq16-clifford-ring-obstruction/verify.py b/research/qq16-clifford-ring-obstruction/verify.py new file mode 100644 index 0000000000..816928cb7d --- /dev/null +++ b/research/qq16-clifford-ring-obstruction/verify.py @@ -0,0 +1,220 @@ +#!/usr/bin/env python3 +"""Source-bound full-input witness and Clifford+T ring controls.""" +import argparse +from fractions import Fraction as Q +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path + +PKG = Path(__file__).resolve().parent +ROOT = PKG.parents[1] +spec = importlib.util.spec_from_file_location('exact_ring', PKG / 'ring.py') +ring = importlib.util.module_from_spec(spec) +spec.loader.exec_module(ring) +need = ring.need +H = [1, 25, 3, 4, 5, 6, 8, 12] +H0 = [1, 2, 3, 4, 5, 6, 8, 12] +Z = [1, 2, 1, 1, 1, 1, 3, -2] + + +def read_json(path, limit=2000000): + need(path.stat().st_size <= limit, 'bounded JSON input') + return json.loads(path.read_text(encoding='utf-8')) + + +def sources(): + manifest = read_json(PKG / 'SOURCES.json') + rows = manifest['files'] + manifest['retained_documents'] + for row in rows: + path = ROOT / row['path'] + need(path.stat().st_size <= 4000000, 'bounded source file') + data = path.read_bytes() + need(hashlib.sha256(data).hexdigest() == row['sha256'], 'source SHA256: ' + row['path']) + blob = hashlib.sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() + need(blob == row['git_blob'], 'source Git blob: ' + row['path']) + raw = (ROOT / 'research/joint-query/certificate.json.gz').read_bytes() + payload = gzip.decompress(raw) # authenticated fixed source, bounded compressed size + need(hashlib.sha256(payload).hexdigest() == manifest['packet_payload_sha256'], 'packet payload') + packet = json.loads(payload) + R = [[Q(row.get(str(j), '0')) for j in range(112)] for row in packet['R_rows']] + A, T, U = (packet[k] for k in ('A_ports', 'T_ports', 'U_ports')) + need(len(R) == 8 and len(A) == len(T) == 8 and len(U) == 96, 'packet dimensions') + need(len(set(A + T + U)) == 112, 'port partition') + need(all(sum(R[i][j]*R[k][j] for j in ports) == 4*int(i == k) + for ports in (A, T) for i in range(8) for k in range(8)), 'selected sections') + return R, A, T, U + + +def inverse(matrix): + n = len(matrix) + a = [list(row) + [Q(i == j) for j in range(n)] for i, row in enumerate(matrix)] + for col in range(n): + pivot = next((i for i in range(col, n) if a[i][col]), None) + need(pivot is not None, 'nonsingular matrix') + a[col], a[pivot] = a[pivot], a[col] + scale = a[col][col] + a[col] = [v / scale for v in a[col]] + for i in range(n): + if i != col: + scale = a[i][col] + a[i] = [x - scale*y for x, y in zip(a[i], a[col])] + return [row[n:] for row in a] + + +def inverse_checks(R): + result = {} + for label, ports in [('original', H0), ('alternative', H)]: + a = [[row[j] for j in ports] for row in R] + b = inverse(a) + for left, right in ((a, b), (b, a)): + need(all(sum(left[i][k]*right[k][j] for k in range(8)) == int(i == j) + for i in range(8) for j in range(8)), 'both inverse orders') + if label == 'original': + need(all(ring.dyadic(v) for row in b for v in row), 'original dyadic positive control') + else: + need(b[0][1] == Q(1, 10), 'odd denominator boundary') + result[label] = [[str(v) for v in row] for row in b] + return result + + +def cut(R, A, T, U, z=Z): + def query(values, ports): + return [sum(row[j]*values[j] for j in ports) for row in R] + def section(v, j): + return sum(R[i][j]*v[i] for i in range(8)) / 4 + x, y = [Q(0)]*112, [Q(0)]*112 + for j, value in zip(H, z): + x[j] = Q(value) + q = query(x, U) + need(q == [0, 10, 0, 0, 0, 0, 0, 0], 'exact unread witness') + for j in A: + x[j], y[j] = -section(q, j), section(q, j) + f, c = query(x, range(112)), query(x, T) + x1, y1 = x[:], y[:] + for j in U: + x1[j] = x[j] - section(f, j) + y1[j] = y[j] + x1[j] + for j in A + T: + x1[j] = section(c if j in A else f, j) + y1[j] = x[j] + y[j] - x1[j] + u = y1[:] + future = query(y1, range(112)) + for j in A: + u[j] = section(future, j) + a, b = query(x1, T), query(u, range(112)) + x2, y2 = x1[:], y1[:] + for j in A: + x2[j], y2[j] = x1[j] + y1[j] - u[j], u[j] + for j in U: + x2[j], y2[j] = x1[j] - y1[j], y1[j] + section(a, j) + for j in T: + x2[j] = section([b[k] + 12*a[k] for k in range(8)], j) + y2[j] = u[j] - section([b[k] + 11*a[k] for k in range(8)], j) + obs = [x1[j] for j in A + T] + [y1[j] for j in A + T] + obs += [y2[j] for j in A] + [x2[j] for j in U] + [x1[j] for j in U if j not in H] + need(len(obs) == 224 and all(ring.reduce(ring.scalar(v)) == (0, 0) for v in obs), 'lost modulo five') + need(x[1] == 1, 'required original output unit') + need([y2[j] for j in A] == [Q(5, 2), Q(-5, 2), 0, Q(5, 2), 0, 0, Q(-5, 2), 0], + 'complete retained logger witness') + return {'input_x': list(map(str, x)), 'input_y': list(map(str, y)), + 'observation': list(map(str, obs)), 'y2_A': [str(y2[j]) for j in A], + 'required_original_x_port1': str(x[1])} + + +def ring_checks(): + r = ring + need(r.mul(r.SQRT2, r.SQRT2) == r.scalar(2), 'square root relation') + need(r.mul(r.HALFROOT, r.SQRT2) == r.ONE, 'normalization inverse') + basis = [tuple(Q(i == j) for i in range(4)) for j in range(4)] + need(all(r.reduce(r.mul(a, b)) == r.fmul(r.reduce(a), r.reduce(b)) + for a in basis for b in basis), 'sixteen basis products') + need(all((a*a - 2*b*b) % 5 for a in range(5) for b in range(5) if a or b), 'F25 norm') + need(r.reduce(r.ONE) == (1, 0) and r.reduce(r.scalar(5)) == (0, 0), 'proper ideal') + need(r.reduce(r.I) != r.reduce(r.neg(r.I)), 'conjugation is not assumed compatible') + need(r.fmul(r.reduce(r.ZETA), r.reduce(r.ZETA), square=3) != r.reduce(r.I), 'wrong field relation detected') + try: + r.reduce(r.scalar(Q(1, 5))) + except ValueError: + pass + else: + raise ValueError('odd denominator admitted') + need(Q(1, 5) * 5 == 1, 'admitting inverse five breaks obstruction') + return {name: list(r.reduce(value)) for name, value in + [('zeta8', r.ZETA), ('i', r.I), ('sqrt2', r.SQRT2), + ('inverse_sqrt2', r.HALFROOT), ('inverse_zeta8', r.neg(r.ZETA3))]} + + +def gate_checks(y2): + r = ring + gates = [('H', 0, None), ('T', 1, None), ('CNOT', 0, 2), + ('S', 2, None), ('X', 1, None), ('Z', 0, None), ('SWAP', 0, 2)] + for op, bit, other in gates: + for j in range(8): + basis = [r.ZERO]*8 + basis[j] = r.ONE + v = r.gate(basis, op, bit, other) + need(r.gate(v, op, bit, other, inverse=True) == basis, 'literal inverse columns') + need(all(r.reduce(r.mul(x, r.scalar(5))) == (0, 0) for x in v), 'reduced gate coefficients') + start = [r.scalar(Q(v)) for v in y2] + current, prefixes = start[:], [] + for op, bit, other in gates: + current = r.gate(current, op, bit, other) + need(all(r.reduce(v) == (0, 0) for v in current), 'gate prefix preserves ideal') + prefixes.append([[str(c) for c in v] for v in current]) + need(any(Q(v[1]) or Q(v[3]) for row in prefixes for v in row), 'non-Gaussian coefficients exercised') + for op, bit, other in reversed(gates): + current = r.gate(current, op, bit, other, inverse=True) + need(current == start, 'whole word return') + basis = [r.ONE] + [r.ZERO]*7 + wrong = r.gate(r.gate(basis, 'H', 0, normalizer=r.ONE), 'H', 0, normalizer=r.ONE) + need(wrong != basis, 'omitted normalization detected') + need(r.mul(r.ZETA, r.ZETA3) != r.ONE, 'wrong phase inverse detected') + return {'gates': [list(g) for g in gates], 'inverse_columns': 56, 'prefixes': prefixes} + + +def compute(): + R, A, T, U = sources() + witness = cut(R, A, T, U) + changed = Z[:] + changed[0] += 1 + try: + cut(R, A, T, U, changed) + except ValueError: + pass + else: + raise ValueError('changed witness accepted') + return {'schema_version': 1, 'status': 'PASS', 'ring': 'Z[zeta8,1/2]', + 'field': 'F5[t]/(t^2-2)', 'specialization': ring_checks(), + 'witness': witness, 'inverses': inverse_checks(R), + 'gate_controls': gate_checks(witness['y2_A']), + 'failure_controls': ['wrong field relation', 'odd denominator rejected', + 'inverse five admits unit', 'omitted H normalization', + 'wrong phase inverse', 'changed unread witness']} + + +def strict_equal(left, right): + if type(left) is not type(right): + return False + if isinstance(left, dict): + return left.keys() == right.keys() and all(strict_equal(left[k], right[k]) for k in left) + if isinstance(left, list): + return len(left) == len(right) and all(strict_equal(x, y) for x, y in zip(left, right)) + return left == right + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit', action='store_true', help='emit recomputed JSON to stdout') + args = parser.parse_args() + result = compute() + if args.emit: + print(json.dumps(result, indent=2)) + else: + need(strict_equal(result, read_json(PKG / 'RESULT.json')), 'exact typed receipt') + print('PASS: source-bound 224 observations; F25 ring map; 56 inverse columns; six failure controls') + + +if __name__ == '__main__': + main()