From fd4b1d3e3d1efd0b344f1de72fd4b62f5df8e703 Mon Sep 17 00:00:00 2001 From: Hiroki KUMAZAKI Date: Mon, 26 Oct 2026 14:37:44 +0900 Subject: [PATCH] Independently audit native equality-cut signs and caller contracts --- .../PROOF.md | 390 ++++++++++++++++++ .../README.md | 121 ++++++ .../RESULT.json | 182 ++++++++ .../SOURCES.json | 36 ++ .../TASK.json | 80 ++++ .../VERIFICATION.md | 56 +++ .../VERIFY.json | 22 + .../contracts.py | 333 +++++++++++++++ .../stabilizers.py | 232 +++++++++++ .../verify.py | 58 +++ 10 files changed, 1510 insertions(+) create mode 100644 research/native-equality-independent-audit/PROOF.md create mode 100644 research/native-equality-independent-audit/README.md create mode 100644 research/native-equality-independent-audit/RESULT.json create mode 100644 research/native-equality-independent-audit/SOURCES.json create mode 100644 research/native-equality-independent-audit/TASK.json create mode 100644 research/native-equality-independent-audit/VERIFICATION.md create mode 100644 research/native-equality-independent-audit/VERIFY.json create mode 100644 research/native-equality-independent-audit/contracts.py create mode 100644 research/native-equality-independent-audit/stabilizers.py create mode 100644 research/native-equality-independent-audit/verify.py diff --git a/research/native-equality-independent-audit/PROOF.md b/research/native-equality-independent-audit/PROOF.md new file mode 100644 index 0000000000..58052bdd2f --- /dev/null +++ b/research/native-equality-independent-audit/PROOF.md @@ -0,0 +1,390 @@ +# Independent audit of the native equality-cut tariff and its caller contract + +Prepared for Hiroki KUMAZAKI (@kumagi), with substantial OpenAI Codex +assistance in derivation, checking, and writing. New work is Apache-2.0. + +**Finding:** the signed Clifford tariff and the complete-word, initial-cache, +and approximation implications in Sections 3–5 of Ali Romman's +[PR #5588 proof](https://github.com/aliromman/integer-mult-bounds/blob/97db3fb45cd93a350e300781d75440d14e6a1f73/research/native-equality-cut/PROOF.md) +hold under their stated hypotheses. No mathematical defect was found in +that scope. The derivation below uses a trace expansion to verify the +signed intersection, then treats all register banks as typed rectangular +maps. It does not infer correctness of a particular physical caller or +admit a new multiplication bound. + +The reviewed source head is +`97db3fb45cd93a350e300781d75440d14e6a1f73`. The unchanged proof and README +are authenticated inputs in [SOURCES.json](SOURCES.json); the repository +base is `df0137efd35e11b4445734bf612bdd4c7ebc330c`. + +## 1. Quantified statement and the equality projector + +Let \(n\ge1\), \(D=2^n\), and \(f\ge1\) be integers. A field is +\(V_f=(\mathbb C^D)^{\otimes f}\). For an integer +\(1\le k\le\lfloor f/2\rfloor\), let \(E_k\) be the orthogonal +projector onto basis strings with equal addresses in each of the pairs +\((1,2),(3,4),\ldots,(2k-1,2k)\). Set + +\[ + a_k=\operatorname{rank}E_k=D^{f-k}. +\] + +For a bank of \(m\) fields the cut projector is +\(E_k^{[m]}=\bigoplus_{j=1}^m E_k\). For a map \(A\) from one bank +to another, define + +\[ + c_k(A)=\operatorname{rank}\bigl((I-E_{\rm out})A E_{\rm in}\bigr). + \tag{1} +\] + +Input and output projectors in (1) are those of the actual banks, which +may have different numbers of fields. All ranks are over \(\mathbb C\). + +For an \(n\)-qubit unitary Clifford operator \(U\), let \(Z\) denote +the diagonal binary Pauli label space and set + +\[ + r(U)=n-\dim_{\mathbb F_2}(Z\cap UZU^*). + \tag{2} +\] + +Here the intersection in (2) is of Pauli labels, ignoring signs. If +\(U Z_j U^*\) has binary \(X\)-label \(x_j\), then +\(r(U)=\operatorname{rank}_{\mathbb F_2}[x_1\ \cdots\ x_n]\): the +kernel consists exactly of diagonal images. The first result to audit is + +\[ + c_k(U^{\otimes f})=a_k(1-2^{-kr(U)}), \tag{3} +\] + +with every nonzero singular value of this cut block equal to one. +When \(r=0\) the cut block is zero. At width \(f=1\) there is no +admissible positive \(k\), so this family supplies no inequality. + +## 2. Signed intersection from a trace calculation + +First consider one pair. For \(v\in\mathbb F_2^n\), write +\(Z_v e_x=(-1)^{v\cdot x}e_x\). Its equality projector is + +\[ + E=\frac1D\sum_v Z_v\otimes Z_v. + \tag{4} +\] + +Indeed its diagonal entry at \((x,y)\) is +\(D^{-1}\sum_v(-1)^{v\cdot(x+y)}\), which is one exactly when +\(x=y\). Put \(W_w=UZ_wU^*\), \(R=U\otimes U\), and + +\[ + F=RER^*=\frac1D\sum_w W_w\otimes W_w. +\] + +Each \(W_w\) is a Hermitian Pauli, and the map \(w\mapsto W_w\) +is injective and multiplicative, including its signs. For each \(v,w\) +the one-column Paulis commute or anticommute. Their two tensor copies +therefore commute: the commutation factor is \((\pm1)^2=1\). +Consequently \(E\) and \(F\) commute and \(EF\) is the orthogonal +projector onto their intersection. + +Expand its trace directly: + +\[ + \operatorname{Tr}(EF) + =\frac1{D^2}\sum_{v,w} + \operatorname{Tr}(Z_v W_w)^2. \tag{5} +\] + +This is the square of the trace, not an assumed absolute-value square. +Pauli trace orthogonality makes it zero unless \(W_w=\pm Z_v\). +In that case the trace is \(\pm D\), so its contribution to (5) is +exactly one. Hermiticity rules out \(W_w=\pm iZ_v\). For precisely +\(2^{n-r(U)}\) choices of \(w\), its image has a diagonal label; +there is one \(v\) for each. Thus + +\[ + \operatorname{rank}(EF)=\operatorname{Tr}(EF) + =2^{n-r(U)}=D\,2^{-r(U)}. \tag{6} +\] + +This calculation explicitly handles negative diagonal images and +images containing \(Y\) factors. Discarding Clifford signs before +forming the tensor-pair stabilizers would not by itself justify (6). + +For comparison with the source's stabilizer-group proof, let +\(S_E=\{Z_v\otimes Z_v\}\) and \(S_F=\{W_w\otimes W_w\}\). +Each is a group of order \(2^n\), and their intersection has order +\(2^{n-r}\), by the same diagonal-image test. There is no negative +identity in their generated joint group. Otherwise, because the groups +commute, some \(Z_v\otimes Z_v=-(W_w\otimes W_w)\) would hold. +Equality of their Pauli labels first forces \(W_w=\pm Z_v\); its +tensor square then gives equality with a **positive** sign, a +contradiction. Hence the joint group has \(2^{n+r}\) elements and +contains no sign conflict. This verifies the specific premise needed +by the source's alternative stabilizer dimension count. + +## 3. From the intersection to the exact tariff + +Let \(C=(I-E)RE\). Its range before projecting by \(I-E\) is +\(\operatorname{ran}F\), and \(R\) maps \(\operatorname{ran}E\) +unitarily onto that space. More explicitly, + +\[ + CC^*=(I-E)F(I-E)=(I-E)F, +\] + +which is a projector because \(E\) and \(F\) commute. Thus the +nonzero singular values of \(C\) are all one, and + +\[ + \operatorname{rank}C + =\operatorname{rank}F-\operatorname{rank}(EF) + =D(1-2^{-r}). +\] + +For \(k\) pairs and \(f-2k\) remaining columns, the cut and its +conjugate are tensor products of these pair projectors and an identity. +They still commute. Their intersection has rank + +\[ + (D2^{-r})^k D^{f-2k}=a_k2^{-kr}, +\] + +whereas each cut has rank \(a_k\). The same projector calculation +proves (3) and its singular-value statement for every allowed +\(n,f,k\). Both terms are integers: in particular +\(a_k2^{-kr}=2^{n(f-k)-kr}\), with exponent at least +\(n(f-2k)\ge0\). + +Multiplying \(U\) by a global scalar phase does not alter its +conjugation action or any rank or singular value here. Also +\(r(U^{-1})=r(U)\), since conjugation by \(U\) identifies +\(Z\cap U^{-1}ZU\) with \(UZU^{-1}\cap Z\). Thus inverse calls +have the same tariff. Nonzero scalar multiples of a cut block have +the same rank, but their nonzero singular values are scaled by the +absolute value of that scalar; only the rank is needed for paid query +updates. + +Two literal boundary examples distinguish the premises from their +unsigned rank consequences. On one qubit, take + +\[ + C=\frac12\begin{pmatrix}1+i&1-i\\1-i&1+i\end{pmatrix}, + \qquad CZC^*=-Y. +\] + +For \(C\otimes C\), the intersection of the equality subspace with +its image is the line spanned by +\((|00\rangle-|11\rangle)/\sqrt2\). Replacing the second factor by +\(\overline C\) changes that line to +\((|00\rangle+|11\rangle)/\sqrt2\). Both intersection ranks are +one, so a rank-only comparison misses this orientation error. The +source requires identical tensor factors; it does not identify these +two projectors. The exact projector numerators are checked by +`stabilizers.signed_matrix_controls`. + +For a different boundary, left-compose \(C\otimes C\) with CNOT +whose control is the first tensor column and whose target is the +second. This CNOT is a unitary monomial map of the complete field, but +it does not preserve the equality cut. In the equality input basis +\((|00\rangle,|11\rangle)\), the resulting cut block has Gram +matrix \(I_2/2\), also checked by `signed_matrix_controls`. Its +nonzero singular values are \(1/\sqrt2\), not one. This is not a +counterexample to the theorem: such inter-column routing is already +excluded from its ordinary alphabet. It shows why unitary endpoint +frames must also preserve the cut. + +## 4. Rectangular composition and all dirty directions + +For composable maps \(B:H_0\to H_1\) and \(A:H_1\to H_2\), with +the respective bank projectors, insert +\(I=E_1+(I-E_1)\) to obtain + +\[ + (AB)_{-+}=A_{--}B_{-+}+A_{-+}B_{++},\qquad + c_k(AB)\le c_k(A)+c_k(B). \tag{7} +\] + +Rank subadditivity and the two elementary product-rank inequalities +prove (7). No inverse, square shape, unitary assumption, fixed choice +of paid input, or absence of feedback is used. + +A rectangular ordinary map satisfies +\(E_{\rm out}A=A E_{\rm in}\), so both of its cross blocks vanish. +A one-column monomial map uses the same address permutation in every +tensor column; it preserves equality and inequality in each pair, and +its diagonal weights do not change support. Its tensor lift therefore +commutes with \(E_k\), as does any linear combination of such lifts. +Scalar mixing between fields, register permutations, COPY, CLEAR, +zero-field insertion, and field selection intertwine the bank cuts. +They consequently have zero charge in (7). + +An application of \(U^{\otimes f}\) on one field has the rank (3) +in its sole potentially nonzero bank cut block. For an update +\(y\leftarrow y+cU^{\otimes f}x\), that block is +\(c(I-E_k)U^{\otimes f}E_k\). It has the same rank for \(c\ne0\), +and rank zero for \(c=0\). This remains the rank calculation if the +alphabet permits a self update: the identity part contributes no cross +block. Overcharging a zero update is harmless to the upper bound. +If a primitive returns several fields, each output must be included +in a valid rank budget; the single-output tariff is not a multi-output +credit. + +Represent the input as the direct sum of **every independent original +and dirty helper field**. Owned fields that actually start at zero +are inserted by a separate rectangular map. A chronological word is a +product of its complete state maps, so induction in (7) gives an upper +bound by the sum of all its paid cut ranks. COPY may increase bank +size, CLEAR may destroy information, and later paid arguments may +depend on all earlier responses. These facts do not change the matrix +identity (7). + +Required output selection is a cut-intertwining map and cannot increase +the endpoint cut rank. This does not authorize ignoring required dirty +returns: they remain in the specified endpoint and are required for +correctness. To obtain a necessary condition one may project that +complete endpoint onto the disjoint target-job blocks. Independent +targets \(T_j^{\otimes f}\), each on its own independent input and +output field, then have additive cut ranks. With \(P_r\) paid calls +and \(T_r\) such target jobs of Fourier rank \(r\), the result is + +\[ + a_k\sum_r T_r(1-2^{-kr}) + \le a_k\sum_r P_r(1-2^{-kr}). \tag{8} +\] + +Repeated credit for the same input/output block would not satisfy this +independence premise. Since \(a_k>0\), it may be canceled in (8). +If fixed profiles are realizable at arbitrarily large widths, each +fixed positive \(k\) is covered by some such \(f\ge2k\). The same +inequality then holds for every \(k\), even if the program, feedback, +coefficients, and storage vary with \(f\). + +## 5. A cached boundary has one joint initial rank + +Let \(J:H_{\rm original}\to H_{\rm available}\) map all independent +inputs to the complete rows available at a chosen caller boundary. +It must specify the actual row versions and their dependence on those +inputs, including independent dirty helper fields. If \(W\) is the +subsequent word and \(S\) selects the required outputs, (7) gives + +\[ + c_k(SWJ)\le c_k(J)+\sum_{\text{subsequent paid calls}}c_k(\text{call}). + \tag{9} +\] + +An exact target endpoint \(T\) therefore requires +\(c_k(T)\) to be at most the right side. In the ordinary initial +state, \(J\) consists of identities and zero insertions and has +\(c_k(J)=0\), recovering (8). At a cached boundary, the entire +cross matrix of \(J\) must be ranked jointly. + +For example, let \(R\) be any one-field map with cut block \(C\). +The availability map \(J=(I,R,R)^\mathsf T\) on one independent +original has cut block \((0,C,C)^\mathsf T\), of rank +\(\operatorname{rank}C\), not twice that rank. Two copies of the +same response do not become two independent inputs. Conversely, rows +depending on separate independent originals can have disjoint domain +blocks and contribute additive rank. A nominal cache count cannot +distinguish these cases. + +Omitting a nonordinary cache is also unsound: a free copy of an already +available \(Rx\) realizes that target with no new paid call, but it +uses the initial cross rank in \(J\). Equation (9) is a relative +boundary statement. It does not make producing those initial cached +rows free in a full physical invoice. A full-word accounting can start +before their production and charge those calls there instead. + +## 6. Endpoint codes and approximation constants + +Let \(L\) and \(R\) be invertible ordinary output and input codes, +respectively, intertwining the same bank cuts. Their restrictions to +the plus and minus subspaces are invertible, and + +\[ + (LAR)_{-+}=L_{--}A_{-+}R_{++}. +\] + +Thus these codes preserve cut rank exactly. This proves the exact +rank obstruction also for nonunitary invertible ordinary endpoint +codes, including invertible monomial frames. It does not preserve +singular values unless the relevant restrictions are unitary. + +For the source's approximation statement, use independent unitary +target jobs and unitary cut-preserving endpoint frames. Their target +cut block \(B\) is a partial isometry with + +\[ + q=\operatorname{rank}B=a_k\sum_r T_r(1-2^{-kr}) +\] + +unit nonzero singular values. Let the program cut block be \(A\), +with rank at most an integer paid budget \(b\). On the \(q\)-dimensional +initial singular subspace of \(B\), the kernel of \(A\) has +dimension at least \(q-b\). If \(q>b\), choose an orthonormal set +of \(q-b\) vectors there. For each such vector \(v\), +\((A-B)v=-Bv\) has norm one. Hence + +\[ + \|A-B\|_{\rm op}\ge1,\qquad + \|A-B\|_{\rm HS}^2\ge q-b. \tag{10} +\] + +Projecting the full endpoint error onto its cut block cannot increase +either norm. In the zero-initial-rank case, take +\(b=a_k\sum_rP_r(1-2^{-kr})\); (10) is precisely the source's +unit operator-error floor and squared Hilbert–Schmidt floor +\(a_k\delta_k\). The same reasoning with caches uses +\(b=c_k(J)+a_k\sum_rP_r(1-2^{-kr})\), when a positive deficit +remains. These are bounds for words assembled from the exact ideal +paid maps. Approximation errors inside a query are not extra +unpriced linear operations in this model. + +The unitary-frame restriction is necessary for the stated constants. +Multiplying the whole output by \(\varepsilon I\), with +\(0<\varepsilon<1\), is an invertible ordinary code and preserves +every cut rank. But it scales the error between a zero endpoint and +a unitary target to operator norm \(\varepsilon\), and its squared +Hilbert–Schmidt error by \(\varepsilon^2\). Thus the exact rank +obstruction survives while the numerical lower bounds with constant +one do not. The source explicitly states this limitation. + +## 7. Audit disposition and boundaries + +| Source assertion at the pinned head | Disposition in this review | Retained premise | +|---|---|---| +| Section 3: signed stabilizer intersection and no negative identity | Established by (5)–(6) and the explicit joint-group check | Unitary Clifford conjugation; the same operator on both tensor columns | +| Section 3, equation (4): exact tariff and unit singular values | Established in Section 3 for every admissible \(n,f,k\), including rank zero | Disjoint equality pairs and unchanged field capacity | +| Section 4: chronological paid-rank upper bound | Established by rectangular identity (7) | Every free map preserves the stated cut; every nonordinary call is charged | +| Section 4: independent targets and dirty inputs/returns | Established as the necessary condition (8) | Separate input/output job blocks and a complete specified endpoint | +| Section 4: invertible ordinary endpoint codes | Exact-rank invariance established in Section 6 | Both cut blocks are preserved and the codes are invertible | +| Section 4, equation (5): approximation floors | Established by the explicit kernel subspace in (10) | Independent unitary target blocks, unitary cut-preserving endpoint frames, exact paid gates | +| Section 5, equation (6): retained observations | Established by (9) and the duplicate-cache example | The complete actual availability matrix \(J\), not nominal rows | +| Sections 6–7: profile decision algorithm and semisimple row-return discussion | Outside this audit | No acceptance of those separate claims is inferred | +| A particular P104/G20 caller, physical execution, or multiplication theorem | Outside this audit | Actual source bindings, availability ledger, paid invoice, compiler, precision, and outer assumptions remain separate | + +An operation acting on only one member of an equality pair need not +preserve the cut. Nor need arbitrary inter-column routing or a nonlinear +operation. Such changes are outside the declared free alphabet. With +different field capacities, (7) can still be formulated using correctly +typed projectors, but the common factor \(a_k\) in (8) cannot simply +be canceled across unlike fields. + +The package's executable receipts provide finite exact corroboration +and controls for these implications. This note makes no claim about +their case counts; the counts and executed commands belong to the +receipt and verification documentation. The general result rests on +the quantified arguments above, not extrapolation from a finite +Clifford sample. This is a separate agent-assisted review, not +independent human acceptance or proof-kernel verification. + +Ali Romman retains credit for the equality-cut invariant, Clifford +tariff, full-word extension, explicit cached-boundary contract, and +source theorem in PR #5588. The classical product-rank inequality, +Pauli/stabilizer theory, trace orthogonality, and rank-deficit +approximation principle are not new results. The source's credited +fused-block/dirty-host work, an664 and its reviewers, Adam Gall, Ross +Richardson, Chris R/Clear1nsight, and the P104/native/controller/compiler +lineage retain their attribution. This contribution checks the stated +proof obligation through a separate trace calculation and explicit +caller-domain accounting; it does not change the selected frontier. diff --git a/research/native-equality-independent-audit/README.md b/research/native-equality-independent-audit/README.md new file mode 100644 index 0000000000..b3f696b7c6 --- /dev/null +++ b/research/native-equality-independent-audit/README.md @@ -0,0 +1,121 @@ +# Independent review of the native equality-cut tariff + +The signed Clifford tariff and caller implications in **PR #5588 PROOF.md +§§3–5 hold under their stated hypotheses**. No mathematical defect was found +in this scope. [PROOF.md](PROOF.md) independently derives the intersection +by a trace calculation and proves the complete-word, cached-history and +approximation statements. This takes the +[explicit independent-review request](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19183713). + +For `a_k = 2^(n(f-k))`, a Fourier-rank-r Clifford call has crossing rank +`a_k (1-2^(-kr))` across the cut equating k disjoint pairs of columns. +Rectangular rank subadditivity then bounds any chronological linear word, +including changed paid inputs, feedback, COPY, CLEAR and independent dirty +helpers. A cached boundary contributes **one joint crossing rank of its +complete availability map J**. The exact rank bound permits invertible +ordinary endpoint codes; the stated unit error floor needs unitary, +cut-preserving endpoint frames. + +This validates one proposed supplier-screening theorem. It does not produce +a supplier, extract J from P104, or discharge any selected implementation +premise. No κ change or native admission is claimed. + +## What the independent checks add + +The checkers import no implementation from PR #5588. They use standard-library +rational and Gaussian-integer arithmetic and independently check: + +- All **366 signed ordered commuting Pauli image frames** for one/two axes, + covering 18 image subgroups. The 54 literal projector checks verify + symmetry, idempotence, trace and rational rank. These are image-frame + enumerations, not an enumeration of all Clifford unitaries. Separate + two-pair checks give crossing ranks 3 and 6 at widths 4 and 5. +- A complex Clifford with `C Z C* = -Y`. Its same-factor tensor has a + Bell-minus intersection; conjugating the second factor changes it to + Bell-plus without changing its rank. This catches a sign/orientation + distinction that rank-only tests miss. +- One **18-operation complete word**, with four paid overwrites, feedback + into the third query, an arbitrary dirty field, and a zero temporary. + All 19 prefixes obey the cut bound; the complete endpoint is + `(2x + Ty, Tx + y, d, 0)`. Omitting dirty subtraction, the final CLEAR, + or the first crossing charge is detected. Five two-bank paid updates + and five self updates also cover zero, negative and fractional coefficients, + including singular self updates. +- `J = [I; T; T]`: joint crossing rank 1, while summing separate cache ranks + gives 2. Selecting a cached response realizes T with no additional call, + demonstrating why omitting J gives a false obstruction. +- Invertible ordinary codes preserve rank. Scaling a unitary target by 1/8 + preserves positive crossing rank but lowers its zero-program operator + error to 1/8. A non-columnwise unitary monomial endpoint instead gives + cut Gram `I/2`, invalidating the partial-isometry step. Both distinguish + restrictions already present in the source contract. + +[RESULT.json](RESULT.json) is a deterministic receipt. Finite controls support +the written all-size argument; they do not replace it. This is an agent-assisted +independent derivation and implementation, not human or proof-kernel acceptance. + +## Source and scope + +Reviewed source: [Ali Romman's PR #5588](https://github.com/CrocSwap/integer-mult-bounds/pull/5588), +head `97db3fb45cd93a350e300781d75440d14e6a1f73`. +The unchanged proof and README are pinned in [SOURCES.json](SOURCES.json) +at canonical main `df0137efd35e11b4445734bf612bdd4c7ebc330c`. +The selected baseline at this checkpoint is P104 PR #5599, +κ=`62009/20000000`; its five inherited premises remain. + +Excluded: source §6's profile algorithm, §7's semisimple output-packing +question, extraction of an actual retained-observation ledger, full supplier +replay, compiler/precision/storage/routing costs, and the complete rounded +multiplication theorem. The source verifier and selected cold replay were not +run. The common factor assumes equal field capacities. Free maps must preserve +the cut and its complement; arbitrary inter-column maps are not included. + +The picker ran once with seed `81093d593dbc22d5b1e5cb3cc7d46405`. +[TASK.json](TASK.json) retains the `uniform-transfer-audit` card and records +the handoff-first scope change from its historical #4100 target to this explicit +current native-lift review. The first overlap snapshot covered 7,676 local +notes, 370 open PRs and 4,998 Discussion records with complete reported +pagination and no warnings. Exact-thread and targeted all-status searches +found no competing audit; PR #5617's stronger stage cuts are distinct. +Searches do not cover unpublished work or every historical code file. +The canonical claim is in +[Discussion #5582](https://github.com/CrocSwap/integer-mult-bounds/discussions/5582#discussioncomment-19188980). + +## Reproduce + +Python 3.12, standard library only; the registered replay is bounded at 120 s. + +```sh +python3.12 -B scripts/research_package.py --package research/native-equality-independent-audit --check-only +python3.12 -B scripts/research_package.py --package research/native-equality-independent-audit +python3.12 -I -O -B research/native-equality-independent-audit/verify.py +``` + +[VERIFICATION.md](VERIFICATION.md) records executed commands and transport +checks. Direct replay needs only the package and its three declared input +files; Git and network are unnecessary. It reads exact pinned source bytes +and compares the recomputed receipt. Normal execution never regenerates it. + +## Open next questions + +At one unclaimed physical caller boundary, extract the complete actual J, +including row versions and independent dirty inputs, and certify its joint +cut rank. The blocker is a source-bound availability ledger, not this rank +inequality. For a concrete caller with inter-column operations or unequal +field sizes, first specify typed projectors and charge every crossing map; +the present normalized tariff cannot be imported unchanged. See the +structured relevance, first steps and blockers in [TASK.json](TASK.json). + +## Credit + +Ali Romman retains credit for the equality-cut invariant, Clifford tariff, +complete-word theorem and explicit boundary/approximation limitations in +PR #5588. Its fused-block and dirty-host predecessors, an664 and reviewers, +Adam Gall, Ross Richardson, Chris R/Clear1nsight, and the P104/native/helper/ +compiler lineage retain their credit. Pauli/stabilizer theory, trace +orthogonality and product-rank inequalities are classical. + +New derivation, code and review prepared for Hiroki KUMAZAKI, with substantial +OpenAI Codex assistance. Delegated agents separately scoped overlap, +reviewed the proof and signs, and implemented chronological/cache controls. +No predecessor code is copied or imported. Apache-2.0. diff --git a/research/native-equality-independent-audit/RESULT.json b/research/native-equality-independent-audit/RESULT.json new file mode 100644 index 0000000000..9780904553 --- /dev/null +++ b/research/native-equality-independent-audit/RESULT.json @@ -0,0 +1,182 @@ +{ + "authenticated_inputs": 3, + "contracts": { + "cached_history": { + "additional_paid_calls": 0, + "available_rows": [ + "x", + "T*x", + "T*x" + ], + "exact_target_cut_rank": 1, + "joint_cut_rank": 1, + "rejected_control": "omit initial availability map J", + "sum_individual_cut_ranks": 2 + }, + "changed_alphabet": { + "crossing_rank": 1, + "inter_column_permutation": [ + 0, + 1, + 3, + 2 + ], + "rejected_control": "grant inter-column CNOT as a zero-rank free map", + "repeated_one_column_positive_controls": 2 + }, + "chronological": { + "endpoint": [ + "2*x + T*y", + "T*x + y", + "d", + "0" + ], + "endpoint_cut_rank": 2, + "feedback_paid_input_index": 3, + "field_dimension": 4, + "missing_first_charge": { + "mutant_prefix_budget": 0, + "observed_prefix_rank": 1 + }, + "operations": 18, + "original_and_dirty_input_columns": 12, + "owned_zero_registers": 1, + "paid_overwrites": 4, + "prefix_bounds": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2, + 2, + 2, + 2, + 2, + 3, + 3, + 3, + 3, + 4, + 4, + 4 + ], + "prefix_cut_ranks": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2, + 2, + 1, + 1, + 1, + 2, + 2, + 2, + 2, + 3, + 3, + 2 + ], + "rejected_controls": [ + "omit dirty-response subtraction", + "omit final CLEAR", + "omit first paid crossing charge" + ] + }, + "endpoint_codes": { + "coded_target_cut_rank": 2, + "left_and_right_code_ranks": [ + 8, + 8 + ], + "rejected_control": "retain unit error floor after nonunitary scaling", + "scaled_target_cut_rank": 1, + "zero_program_operator_error": "1/8", + "zero_program_paid_calls": 0 + }, + "paid_updates": { + "cases": [ + { + "coefficient": "0", + "self_update_cut_rank": 0, + "self_update_full_rank": 4, + "two_bank_cut_rank": 0 + }, + { + "coefficient": "1", + "self_update_cut_rank": 1, + "self_update_full_rank": 2, + "two_bank_cut_rank": 1 + }, + { + "coefficient": "-1", + "self_update_cut_rank": 1, + "self_update_full_rank": 2, + "two_bank_cut_rank": 1 + }, + { + "coefficient": "1/2", + "self_update_cut_rank": 1, + "self_update_full_rank": 4, + "two_bank_cut_rank": 1 + }, + { + "coefficient": "-3/2", + "self_update_cut_rank": 1, + "self_update_full_rank": 4, + "two_bank_cut_rank": 1 + } + ], + "self_update_cases": 5, + "two_bank_cases": 5, + "two_bank_independent_input_columns_per_case": 8 + } + }, + "new_kappa_or_supplier_admission": false, + "reviewed_source_head": "97db3fb45cd93a350e300781d75440d14e6a1f73", + "scope": "PR5588 PROOF.md sections3\u20135; written all-size proof plus finite exact controls", + "source_verifier_imported": false, + "stabilizers": { + "controls": { + "k2_f4_cut_rank": 3, + "k2_f5_cut_rank": 6, + "mismatched_factor_control": 1, + "rejected_frame_controls": 3 + }, + "n1": { + "fourier_rank_counts": { + "0": 2, + "1": 4 + }, + "frames_with_imaginary_Pauli_entries": 2, + "image_subgroups": 3, + "literal_projectors": 9, + "signed_ordered_frames": 6 + }, + "n2": { + "fourier_rank_counts": { + "0": 24, + "1": 144, + "2": 192 + }, + "frames_with_imaginary_Pauli_entries": 216, + "image_subgroups": 15, + "literal_projectors": 45, + "signed_ordered_frames": 360 + }, + "signed_matrix_controls": { + "conjugated_factor_intersection": "Bell plus", + "exact_Gaussian_integer_controls": 3, + "noncolumnwise_unitary_endpoint_cut_gram": "I/2", + "same_factor_intersection": "Bell minus" + } + }, + "status": "PASS_NATIVE_EQUALITY_INDEPENDENT_AUDIT" +} diff --git a/research/native-equality-independent-audit/SOURCES.json b/research/native-equality-independent-audit/SOURCES.json new file mode 100644 index 0000000000..37012c4bf6 --- /dev/null +++ b/research/native-equality-independent-audit/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "files": [ + { + "path": "LICENSE", + "usage": "input", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/native-equality-cut/PROOF.md", + "usage": "input", + "git_blob": "bd4964f17868e4f016d47db887bae6906e8e9f2b", + "sha256": "8f0043ff2084b3ff503cd357a186bda4ffa3cd4f1e50df4d7d9b63d23064e38d" + }, + { + "path": "research/native-equality-cut/README.md", + "usage": "input", + "git_blob": "83fcc474f5b79a7d1118090d4687d55974708d5a", + "sha256": "2fab505ce913ef8edf474a355b3e7d8c40552e37f9e3a9f03e380b4d4332f9c2" + } + ] +} diff --git a/research/native-equality-independent-audit/TASK.json b/research/native-equality-independent-audit/TASK.json new file mode 100644 index 0000000000..711920358e --- /dev/null +++ b/research/native-equality-independent-audit/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Independent audit of PR5588 PROOF.md sections3\u20135: signed Clifford equality-cut tariff for all n,f,k; rectangular chronological composition, joint cached J, and exact/approximate endpoint conditions.", + "scope_change_reason": "Handoff-first choice: the current explicit PR5588 review request is an uncovered native-lift implication. The picker suggested uniform-transfer-audit in historical4100; no reroll was made. This checks the scoped theorem used to screen changed native callers, not the complete4100 construction or the selected P104 caller.", + "bottleneck_link": "Supplier searches with changed paid inputs need a valid whole-word obstruction. Independent sign and caller-contract review reduces the risk of rejecting a feasible supplier or overlooking uncharged cached information; it does not discharge the selected all-column/physical transfer assumptions.", + "budget_minutes": 60, + "stop_rule": "Stop after the quantified \u00a7\u00a73\u20135 proof audit and bounded independent exact controls; no new supplier search, full native replay, profile algorithm audit, or selected-result edit.", + "outcome": "completed", + "evidence": "PROOF.md establishes the scoped implication; RESULT.json records366 signed ordered frames,54 literal projectors, Bell-sign and endpoint-frame controls, and one18-operation dirty-feedback word with19 prefix checks plus cache/code controls.", + "author": "Hiroki KUMAZAKI", + "ai_assistance": "Substantial OpenAI Codex assistance in derivation, implementation, verification and prose. Delegated agents separately scouted overlap, derived/reviewed the proof, implemented chronological/cache controls, and reviewed signs and contract boundaries. This is not independent human or proof-kernel acceptance.", + "open_questions": [ + { + "question": "What is the exact joint cut rank of J at a named retained-observation boundary in a current native supplier?", + "why_it_matters": "This audit validates the relative inequality but does not bind its initial credit to an actual physical caller. Nominal cache counts can overstate that credit.", + "first_step": "Choose an unclaimed exact boundary, pin every available row version and independent source, build its complete availability matrix, and compute a certified joint cut rank.", + "blocked_by": "A source-bound availability ledger and explicit permitted free alphabet for that caller; no such extraction was performed here." + }, + { + "question": "Do stronger cuts handle a proposed caller with paid inter-column routing or unequal field capacities?", + "why_it_matters": "The present common equality-cut factor and unitary-frame argument cannot be used unchanged for those operations.", + "first_step": "Name the concrete proposed operation and typed field spaces, compute its cross blocks, and include their ranks in the chronological bound before assessing an invoice.", + "blocked_by": "A concrete changed caller and full physical charge; arbitrary new alphabets are outside this review." + } + ] +} diff --git a/research/native-equality-independent-audit/VERIFICATION.md b/research/native-equality-independent-audit/VERIFICATION.md new file mode 100644 index 0000000000..43f7925ec8 --- /dev/null +++ b/research/native-equality-independent-audit/VERIFICATION.md @@ -0,0 +1,56 @@ +# Verification record + +Environment: Linux x86_64, Python 3.12.13, standard library only. +Base: canonical main `df0137efd35e11b4445734bf612bdd4c7ebc330c`. +Reviewed PR5588 head: `97db3fb45cd93a350e300781d75440d14e6a1f73`. +Its proof and README are byte-identical at the base; `SOURCES.json` +authenticates their exact Git blobs and SHA256 hashes. + +The following completed successfully on 2026-10-26: + +```sh +python3.12 -B scripts/research_selected_baseline.py +python3.12 -B scripts/research_package.py --package research/native-equality-independent-audit --check-only +python3.12 -B scripts/research_package.py --package research/native-equality-independent-audit +python3.12 -I -O -B research/native-equality-independent-audit/verify.py +``` + +The selected-baseline command checks source bindings and metadata only. +No selected native replay or supplier admission was run. The registered +normal replay and direct isolated optimized replay produce the same +scientific receipt, `RESULT.json`. Every check uses explicit exceptions +and remains active with assertions disabled. + +The arithmetic modules are independent implementations. No source verifier +is imported. `stabilizers.py` uses Pauli labels with explicit phases modulo4, +integer projector numerators, rational elimination and Gaussian-integer +complex controls. `contracts.py` uses literal rational matrices throughout. +The written proof, not the finite enumerations, establishes all-size claims. + +Committed-byte/source-history and deterministic export checks also passed: + +```sh +python3.12 -B scripts/check_research_commit.py --package research/native-equality-independent-audit --check-source-history +python3.12 -B scripts/export_research_package.py export --package research/native-equality-independent-audit --output /tmp/imb-20261026-equality.tar +python3.12 -B scripts/export_research_package.py check /tmp/imb-20261026-equality.tar +``` + +The export contains 13 scientific/package/input files, including the three +declared inputs. It was extracted with Python's tar data filter into a fresh +`/tmp` directory outside the checkout. Direct `-I -O -B` replay from `/tmp`, +using an absolute Python executable with `PATH=/nonexistent` and empty +`PYTHONPATH`, reproduced the complete receipt without Git. In that disposable +copy, changing the receipt and changing the pinned proof input independently +caused the expected explicit failures. The source checkout stayed unchanged. +After recording these results, the final committed bytes were exported and +checked again, with a second fresh Git-free optimized replay. + +Pre-submission canonical-main refresh retained the same base. The fresh overlap +snapshot at 05:37:18 UTC covered 7,676 HEAD notes plus the two new package notes, +374 open PRs and 5,002 Discussion records, with complete reported pagination +and no warnings. No new overlapping audit appeared. The reviewed source head +and its proof/README bytes were rechecked separately. These checks establish +transport, source bindings and reported search coverage; they are not +mathematical acceptance or a guarantee about unpublished work. + +Hosted CI status is reported in the PR, not frozen into this note. diff --git a/research/native-equality-independent-audit/VERIFY.json b/research/native-equality-independent-audit/VERIFY.json new file mode 100644 index 0000000000..85461a59f9 --- /dev/null +++ b/research/native-equality-independent-audit/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "LICENSE", + "research/native-equality-cut/PROOF.md", + "research/native-equality-cut/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Independent signed-Pauli projector matrices, tensor-pair ranks, exact Gaussian-integer Bell/frame controls, full chronological dirty-feedback endpoint and all prefixes, joint cache rank and code/error controls; source pins and deterministic receipt." + } + ] +} diff --git a/research/native-equality-independent-audit/contracts.py b/research/native-equality-independent-audit/contracts.py new file mode 100644 index 0000000000..3adc926f83 --- /dev/null +++ b/research/native-equality-independent-audit/contracts.py @@ -0,0 +1,333 @@ +"""Independent exact checks of the complete-word contract in PR5588 §§4–5. + +Hiroki KUMAZAKI, with substantial OpenAI Codex assistance. Apache-2.0. + +This module uses its own dense Fraction arithmetic and imports no predecessor +implementation. Its finite examples support, but do not prove, the quantified +rank inequality. The chosen native operation is H tensor H, whose entries are +rational although the entries of the one-column normalized Hadamard are not. +""" + +from fractions import Fraction as F + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def zeros(rows, cols): + return [[F(0) for _ in range(cols)] for _ in range(rows)] + + +def eye(size): + result = zeros(size, size) + for i in range(size): + result[i][i] = F(1) + return result + + +def shape(matrix): + need(bool(matrix) and bool(matrix[0]), "empty matrix") + width = len(matrix[0]) + need(all(len(row) == width for row in matrix), "ragged matrix") + return len(matrix), width + + +def multiply(left, right): + rows, inner = shape(left) + inner_right, cols = shape(right) + need(inner == inner_right, "matrix product shape") + result = zeros(rows, cols) + for i in range(rows): + for k, value in enumerate(left[i]): + if value: + for j, other in enumerate(right[k]): + if other: + result[i][j] += value * other + return result + + +def transpose(matrix): + shape(matrix) + return [list(row) for row in zip(*matrix)] + + +def scale(matrix, scalar): + return [[F(scalar) * value for value in row] for row in matrix] + + +def rank(matrix): + rows, cols = shape(matrix) + work = [[F(value) for value in row] for row in matrix] + pivot_row = 0 + for col in range(cols): + pivot = next((i for i in range(pivot_row, rows) + if work[i][col]), None) + if pivot is None: + continue + work[pivot_row], work[pivot] = work[pivot], work[pivot_row] + divisor = work[pivot_row][col] + work[pivot_row] = [value / divisor for value in work[pivot_row]] + for i in range(pivot_row + 1, rows): + factor = work[i][col] + if factor: + work[i] = [value - factor * base for value, base + in zip(work[i], work[pivot_row])] + pivot_row += 1 + if pivot_row == rows: + break + return pivot_row + + +def tensor(left, right): + return [[a * b for a in row_left for b in row_right] + for row_left in left for row_right in right] + + +def equality_cut(registers): + # Two binary columns, ordered 00, 01, 10, 11 in every register. + return [i % 4 in (0, 3) for i in range(4 * registers)] + + +def cut_rank(matrix, output_cut, input_cut): + rows, cols = shape(matrix) + need((rows, cols) == (len(output_cut), len(input_cut)), "cut shape") + block = [[matrix[i][j] for j in range(cols) if input_cut[j]] + for i in range(rows) if not output_cut[i]] + return rank(block) + + +def install_block(matrix, output_register, input_register, block): + need(shape(block) == (4, 4), "field block shape") + for i in range(4): + for j in range(4): + matrix[4 * output_register + i][4 * input_register + j] = block[i][j] + + +def register_gate(kind, dst, src=None, coefficient=1, native=None): + """Four registers: x, y, independent dirty d, owned temporary t.""" + result = eye(16) + need(0 <= dst < 4, "destination") + if kind in ("copy", "add"): + need(src is not None and 0 <= src < 4 and src != dst, "source") + if kind in ("copy", "clear", "native"): + for row in range(4 * dst, 4 * dst + 4): + result[row] = [F(0)] * 16 + if kind == "copy": + install_block(result, dst, src, eye(4)) + elif kind == "add": + install_block(result, dst, src, scale(eye(4), coefficient)) + elif kind == "native": + install_block(result, dst, dst, native) + else: + need(kind == "clear", "unknown gate") + return result + + +def chronological(native): + # Implement y += T x, then x += T y, using an arbitrary dirty d. + # In each shear the temporary first queries source+d; a second query + # removes T d. Thus the third paid input depends on the first response. + operations = [] + for dst, src in ((1, 0), (0, 1)): + operations.extend([ + ("copy", 3, src, 1), + ("add", 3, 2, 1), + ("native", 3, None, 1), + ("add", dst, 3, 1), + ("clear", 3, None, 1), + ("copy", 3, 2, 1), + ("native", 3, None, 1), + ("add", dst, 3, -1), + ("clear", 3, None, 1), + ]) + initial = zeros(16, 12) + for i in range(12): + initial[i][i] = F(1) + state = initial + in_cut, out_cut = equality_cut(3), equality_cut(4) + initial_rank = cut_rank(initial, out_cut, in_cut) + need(initial_rank == 0, "ordinary independent initial state") + charged = 0 + prefix_ranks = [initial_rank] + prefix_bounds = [initial_rank] + gate_ranks = [] + paid_inputs = [] + dirty_omitted = initial + dirty_control_removed = False + for index, (kind, dst, src, coefficient) in enumerate(operations): + gate = register_gate(kind, dst, src, coefficient, native) + gate_rank = cut_rank(gate, out_cut, out_cut) + gate_ranks.append(gate_rank) + need(gate_rank == (1 if kind == "native" else 0), "gate crossing rank") + if kind == "native": + paid_inputs.append([row[:] for row in state[12:16]]) + before_rank = cut_rank(state, out_cut, in_cut) + state = multiply(gate, state) + after_rank = cut_rank(state, out_cut, in_cut) + need(after_rank <= before_rank + gate_rank, "one-step subadditivity") + charged += gate_rank + need(after_rank <= initial_rank + charged, "complete prefix bound") + prefix_ranks.append(after_rank) + prefix_bounds.append(initial_rank + charged) + # Omit exactly the first dirty-response subtraction, leaving all + # later gates unchanged; endpoint comparison must catch its leakage. + if index == 7: + dirty_control_removed = True + else: + dirty_omitted = multiply(gate, dirty_omitted) + expected = zeros(16, 12) + for dst, src, block in ((0, 0, scale(eye(4), 2)), (0, 1, native), + (1, 0, native), (1, 1, eye(4)), + (2, 2, eye(4))): + install_block(expected, dst, src, block) + need(state == expected, "literal complete endpoint") + need(dirty_control_removed and dirty_omitted != expected, + "missing dirty uncompute was undetected") + need(any(dirty_omitted[i][j] for i in range(8) for j in range(8, 12)), + "dirty mutation must leak an independent dirty coordinate") + # The third query input is y_original + T*x_original + d_original. + expected_feedback = [native[i] + eye(4)[i] + eye(4)[i] for i in range(4)] + need(paid_inputs[2] == expected_feedback, "paid response feedback") + need(prefix_ranks[3] == 1, "first paid overwrite must cross the cut") + mutant_prefix_budget = initial_rank + sum(gate_ranks[:2]) + need(mutant_prefix_budget == 0 and prefix_ranks[3] > mutant_prefix_budget, + "omitting the first paid charge must fail the prefix bound") + need(cut_rank(state, out_cut, in_cut) == 2, "complete two-shear rank") + # CLEAR is substantive: omitting the final one retains T*d in t. + before_last = initial + for kind, dst, src, coefficient in operations[:-1]: + before_last = multiply(register_gate(kind, dst, src, coefficient, native), + before_last) + need(before_last != expected and before_last[12:16] != zeros(4, 12), + "missing final CLEAR was undetected") + return { + "field_dimension": 4, "original_and_dirty_input_columns": 12, + "owned_zero_registers": 1, "operations": len(operations), + "paid_overwrites": len(paid_inputs), "feedback_paid_input_index": 3, + "prefix_cut_ranks": prefix_ranks, "prefix_bounds": prefix_bounds, + "endpoint": ["2*x + T*y", "T*x + y", "d", "0"], + "endpoint_cut_rank": 2, + "missing_first_charge": {"observed_prefix_rank": prefix_ranks[3], + "mutant_prefix_budget": mutant_prefix_budget}, + "rejected_controls": ["omit dirty-response subtraction", + "omit final CLEAR", "omit first paid crossing charge"], + } + + +def paid_update_controls(native): + """Check overwrite-independent additive queries, including singular updates.""" + coefficients = (F(0), F(1), F(-1), F(1, 2), F(-3, 2)) + results = [] + for coefficient in coefficients: + gate = eye(8) + install_block(gate, 1, 0, scale(native, coefficient)) + # Literal all-column semantics: the original destination is retained, + # while only the source contributes through the paid operator. + expected = [[F(i == j) + (coefficient * native[i - 4][j] + if i >= 4 and j < 4 else F(0)) + for j in range(8)] for i in range(8)] + need(gate == expected, "two-bank additive query endpoint") + cross = cut_rank(gate, equality_cut(2), equality_cut(2)) + need(cross == int(bool(coefficient)), "scaled additive query cut rank") + need(rank(gate) == 8, "additive query retains both independent banks") + # Same-register updates may be singular. The identity has no crossing + # block, so their crossing rank is still that of c*T. + self_update = [[F(i == j) + coefficient * native[i][j] + for j in range(4)] for i in range(4)] + self_cross = cut_rank(self_update, equality_cut(1), equality_cut(1)) + need(self_cross == int(bool(coefficient)), "self-update cut rank") + full_rank = rank(self_update) + need(full_rank == (2 if coefficient in (F(1), F(-1)) else 4), + "self-update invertibility boundary") + results.append({"coefficient": str(coefficient), + "two_bank_cut_rank": cross, + "self_update_cut_rank": self_cross, + "self_update_full_rank": full_rank}) + return {"two_bank_cases": len(coefficients), + "self_update_cases": len(coefficients), + "two_bank_independent_input_columns_per_case": 8, + "cases": results} + + +def cached_history(native): + # Available fields are x, T*x, T*x, all from the same independent x. + joined = eye(4) + [row[:] for row in native] + [row[:] for row in native] + cuts_in, cuts_out = equality_cut(1), equality_cut(3) + joint = cut_rank(joined, cuts_out, cuts_in) + separate = [cut_rank(block, cuts_in, cuts_in) for block in (eye(4), native, native)] + need(joint == 1 and sum(separate) == 2, "dependent cached rows") + select = zeros(4, 12) + install_block(select, 0, 1, eye(4)) + need(cut_rank(select, cuts_in, cuts_out) == 0, "ordinary cache selection") + endpoint = multiply(select, joined) + need(endpoint == native, "cache alone supplies the exact native target") + target_rank = cut_rank(endpoint, cuts_in, cuts_in) + need(target_rank <= joint and target_rank > 0, + "omitting initial crossing rank must give a false obstruction") + return {"available_rows": ["x", "T*x", "T*x"], + "joint_cut_rank": joint, "sum_individual_cut_ranks": sum(separate), + "additional_paid_calls": 0, "exact_target_cut_rank": target_rank, + "rejected_control": "omit initial availability map J"} + + +def endpoint_codes(native): + # Independently invertible register codes commute with the equality cut. + left = tensor([[F(1), F(1)], [F(0), F(2)]], eye(4)) + right = tensor([[F(1), F(0)], [F(1, 2), F(1)]], eye(4)) + target = tensor(eye(2), native) + cut = equality_cut(2) + need(rank(left) == 8 and rank(right) == 8, "invertible ordinary codes") + need(cut_rank(left, cut, cut) == cut_rank(right, cut, cut) == 0, + "ordinary codes cross the cut") + need(cut_rank(target, cut, cut) == 2, "uncoded independent targets") + need(cut_rank(multiply(multiply(left, target), right), cut, cut) == 2, + "ordinary codes change cut rank") + small = scale(native, F(1, 8)) + need(multiply(transpose(small), small) == scale(eye(4), F(1, 64)), + "exact scaled-target singular values") + need(cut_rank(small, equality_cut(1), equality_cut(1)) == 1, + "nonunitary scalar code changes rank") + return {"coded_target_cut_rank": 2, "left_and_right_code_ranks": [8, 8], + "scaled_target_cut_rank": 1, "zero_program_paid_calls": 0, + "zero_program_operator_error": "1/8", + "rejected_control": "retain unit error floor after nonunitary scaling"} + + +def changed_alphabet(): + # CNOT between the two tensor columns is monomial on the four-coordinate + # field, but is not an allowed repeated one-column map M tensor M. + permutation = [0, 1, 3, 2] + cnot = zeros(4, 4) + for source, destination in enumerate(permutation): + cnot[destination][source] = F(1) + cut = equality_cut(1) + need(multiply(transpose(cnot), cnot) == eye(4), "CNOT permutation") + need(cut_rank(cnot, cut, cut) == 1, "inter-column map crossing") + swap = tensor([[F(0), F(1)], [F(1), F(0)]], + [[F(0), F(1)], [F(1), F(0)]]) + diagonal = tensor([[F(1), F(0)], [F(0), F(2)]], + [[F(1), F(0)], [F(0), F(2)]]) + need(cut_rank(swap, cut, cut) == cut_rank(diagonal, cut, cut) == 0, + "one-column monomial positive controls") + return {"inter_column_permutation": permutation, "crossing_rank": 1, + "repeated_one_column_positive_controls": 2, + "rejected_control": "grant inter-column CNOT as a zero-rank free map"} + + +def run(): + native = [[F((-1) ** ((i & j).bit_count()), 2) for j in range(4)] + for i in range(4)] + need(multiply(native, native) == eye(4), "Hadamard tensor square") + need(multiply(transpose(native), native) == eye(4), "native unitarity") + return {"chronological": chronological(native), + "paid_updates": paid_update_controls(native), + "cached_history": cached_history(native), + "endpoint_codes": endpoint_codes(native), + "changed_alphabet": changed_alphabet()} + + +if __name__ == "__main__": + import json + print(json.dumps(run(), sort_keys=True, indent=2)) diff --git a/research/native-equality-independent-audit/stabilizers.py b/research/native-equality-independent-audit/stabilizers.py new file mode 100644 index 0000000000..0f7566911d --- /dev/null +++ b/research/native-equality-independent-audit/stabilizers.py @@ -0,0 +1,232 @@ +"""Independent exact signed-Pauli audit. Hiroki KUMAZAKI / OpenAI Codex. + +Apache-2.0. No source verifier imports. Matrices are unnormalized integer +projector numerators; complex Pauli phases are represented modulo four. +""" +from collections import Counter +from fractions import Fraction +from itertools import product + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def multiply(a, b): + p, x, z = a + q, y, w = b + return ((p + q + 2 * (z & y).bit_count()) % 4, x ^ y, z ^ w) + + +def commute(a, b): + return ((a[1] & b[2]).bit_count() + (a[2] & b[1]).bit_count()) % 2 == 0 + + +def subgroup(frame): + result = [(0, 0, 0)] + for generator in frame: + result += [multiply(old, generator) for old in result] + return result + + +def valid_frame(frame, n): + if len(frame) != n: + return False + if any(multiply(p, p) != (0, 0, 0) for p in frame): + return False + if any(not commute(p, q) for p in frame for q in frame): + return False + return len({(x, z) for _, x, z in subgroup(frame)}) == 2**n + + +def gf2rank(values): + pivots = {} + for v in values: + while v: + bit = v.bit_length() - 1 + if bit in pivots: + v ^= pivots[bit] + else: + pivots[bit] = v + break + return len(pivots) + + +def matrix_rank(matrix): + a = [[Fraction(v) for v in row] for row in matrix] + rank = 0 + for col in range(len(a[0])): + pivot = next((i for i in range(rank, len(a)) if a[i][col]), None) + if pivot is None: + continue + a[rank], a[pivot] = a[pivot], a[rank] + for i in range(rank + 1, len(a)): + if a[i][col]: + ratio = a[i][col] / a[rank][col] + for j in range(col, len(a[0])): + a[i][j] -= ratio * a[rank][j] + rank += 1 + return rank + + +def doubled_projector_numerator(group, n): + d = 2**n + result = [[0] * (d*d) for _ in range(d*d)] + for p, x, z in group: + for a, b in product(range(d), repeat=2): + sign = (-1) ** ((p + (z & a).bit_count() + (z & b).bit_count()) % 2) + result[(a ^ x)*d + (b ^ x)][a*d + b] += sign + return result + + +def check_projector(a, scale, expected_rank): + size = len(a) + require(all(a[i][j] == a[j][i] for i in range(size) for j in range(size)), 'Hermitian numerator') + require(all(sum(a[i][k]*a[k][j] for k in range(size)) == scale*a[i][j] + for i in range(size) for j in range(size)), 'projector idempotence') + require(sum(a[i][i] for i in range(size)) == scale*expected_rank, 'projector trace') + require(matrix_rank(a) == expected_rank, 'independent rational rank') + + +def census(n): + d = 2**n + labels = [((x & z).bit_count() % 4, x, z) + for x, z in product(range(d), repeat=2) if x or z] + seen = set() + signed_frames = 0 + rank_counts = Counter() + nontrivial_phase_frames = 0 + checked_projectors = 0 + for base in product(labels, repeat=n): + if not valid_frame(base, n): + continue + r = gf2rank([p[1] for p in base]) + common_labels = frozenset((p[1], p[2]) for p in subgroup(base)) + base_numerator = doubled_projector_numerator(subgroup(base), n) + # Every choice of generator signs is a different character, and every + # one must give the same doubled projector. No sign is discarded first. + for signs in product((0, 2), repeat=n): + frame = [((p + sign) % 4, x, z) for (p, x, z), sign in zip(base, signs)] + group = subgroup(frame) + require(valid_frame(frame, n), 'signed frame is valid') + require((2, 0, 0) not in group, 'single-copy group has no negative identity') + diagonal = [p for p in group if p[1] == 0] + require(len(diagonal) == 2**(n-r), 'signed diagonal intersection size') + require(all(p[0] % 2 == 0 for p in diagonal), 'diagonal Hermitian phases are real') + numerator = doubled_projector_numerator(group, n) + require(numerator == base_numerator, 'sign cancellation in literal tensor matrices') + signed_frames += 1 + rank_counts[str(r)] += 1 + nontrivial_phase_frames += int(any(p[0] % 2 for p in group)) + # The same image subgroup may have several ordered bases. Check its + # literal matrix once, while all ordered signed frames were checked above. + if common_labels in seen: + continue + seen.add(common_labels) + a = base_numerator + eq = [i*d+i for i in range(d)] + neq = [i for i in range(d*d) if i not in eq] + require(all(a[i][j] == 0 for i in eq for j in neq), 'equality projector commutation') + check_projector(a, d, d) + intersection = [[a[i][j] for j in eq] for i in eq] + outside = [[a[i][j] for j in neq] for i in neq] + check_projector(intersection, d, 2**(n-r)) + check_projector(outside, d, d-2**(n-r)) + checked_projectors += 3 + expected_frames = {1: 6, 2: 360}[n] + expected_groups = {1: 3, 2: 15}[n] + require(signed_frames == expected_frames, 'exhaustive signed frame cardinality') + require(len(seen) == expected_groups, 'exhaustive image subgroup cardinality') + return {'signed_ordered_frames': signed_frames, 'image_subgroups': len(seen), + 'fourier_rank_counts': dict(sorted(rank_counts.items())), + 'frames_with_imaginary_Pauli_entries': nontrivial_phase_frames, + 'literal_projectors': checked_projectors} + + +def tensor(a, b): + return [[x*y for x in ar for y in br] for ar in a for br in b] + + +def signed_matrix_controls(): + # Gaussian integers (real, imaginary); all denominators stay explicit. + def mul(a, b): + return (a[0]*b[0]-a[1]*b[1], a[0]*b[1]+a[1]*b[0]) + + def conjugate(a): + return (a[0], -a[1]) + + def mm(a, b): + return [[tuple(sum(mul(a[i][k], b[k][j])[component] + for k in range(len(b))) for component in (0, 1)) + for j in range(len(b[0]))] for i in range(len(a))] + + def adjoint(a): + return [[conjugate(a[j][i]) for j in range(len(a))] + for i in range(len(a[0]))] + + def kt(a, b): + return [[mul(x, y) for x in ar for y in br] for ar in a for br in b] + + # C = exp(-i*pi*X/4) up to a scalar phase; C Z C* = -Y. + # c is 2C and u is 4(C tensor C). + c = [[(1,1), (1,-1)], [(1,-1), (1,1)]] + require(mm(adjoint(c), c) == [[(4,0),(0,0)],[(0,0),(4,0)]], 'literal Clifford unitarity') + z = [[(1,0),(0,0)],[(0,0),(-1,0)]] + require(mm(mm(c, z), adjoint(c)) == [[(0,0),(0,4)],[(0,-4),(0,0)]], 'literal signed Y image') + u = kt(c, c) + other = kt(c, [[conjugate(v) for v in row] for row in c]) + eq = (0,3) + def intersection_num(v): + cols = [[row[j] for j in eq] for row in v] + f = mm(cols, adjoint(cols)) # 16F + return [[f[i][j] for j in eq] for i in eq] + same = intersection_num(u) + conjugated = intersection_num(other) + require(same == [[(8,0),(-8,0)],[(-8,0),(8,0)]], 'same-factor Bell-minus intersection') + require(conjugated == [[(8,0),(8,0)],[(8,0),(8,0)]], 'conjugated-factor Bell-plus intersection') + # A unitary monomial on the complete two-column field need not preserve E. + # Left CNOT exchanges output rows 2 and 3. Its cut Gram is I/2. + routed = [u[i] for i in (0,1,3,2)] + block = [[routed[i][j] for j in eq] for i in (1,2)] + require(mm(adjoint(block), block) == [[(8,0),(0,0)],[(0,0),(8,0)]], + 'non-cut-preserving endpoint invalidates the partial-isometry step') + return {'same_factor_intersection': 'Bell minus', + 'conjugated_factor_intersection': 'Bell plus', + 'noncolumnwise_unitary_endpoint_cut_gram': 'I/2', + 'exact_Gaussian_integer_controls': 3} + + +def controls(): + # Same symplectic label but a sign change in only the second tensor factor: + # F=(I-Z tensor Z)/2 has no intersection with E=(I+Z tensor Z)/2. + wrong = [[0]*4 for _ in range(4)] + wrong[1][1] = wrong[2][2] = 2 + require(matrix_rank(wrong) == 2 and wrong[0][0] + wrong[3][3] == 0, + 'mismatched tensor factors invalidate r=0 tariff') + require(not valid_frame([(0,1,0),(0,0,1)], 2), 'reject anticommuting images') + require(not valid_frame([(0,1,0),(0,1,0)], 2), 'reject dependent images') + require(not valid_frame([(1,1,0)], 1), 'reject anti-Hermitian image') + # Two paired blocks and one unrestricted column: test the product factors + # using the literal r=1 projector F=(I+X tensor X)/2. + pair = doubled_projector_numerator([(0,0,0),(0,1,0)], 1) + four = tensor(pair, pair) + # Pairwise row index ordering is (a,b,c,d), E imposes a=b and c=d. + eq = [i for i in range(16) if ((i>>3)&1)==((i>>2)&1) and ((i>>1)&1)==(i&1)] + neq = [i for i in range(16) if i not in eq] + cross_gram = [[four[i][j] for j in neq] for i in neq] + check_projector(cross_gram, 4, 3) + five = tensor(cross_gram, [[1,0],[0,1]]) + check_projector(five, 4, 6) + return {'rejected_frame_controls': 3, 'mismatched_factor_control': 1, + 'k2_f4_cut_rank': 3, 'k2_f5_cut_rank': 6} + + +def run(): + return {'n1': census(1), 'n2': census(2), 'controls': controls(), + 'signed_matrix_controls': signed_matrix_controls()} + + +if __name__ == '__main__': + import json + print(json.dumps(run(), indent=2, sort_keys=True)) diff --git a/research/native-equality-independent-audit/verify.py b/research/native-equality-independent-audit/verify.py new file mode 100644 index 0000000000..9811d49d09 --- /dev/null +++ b/research/native-equality-independent-audit/verify.py @@ -0,0 +1,58 @@ +#!/usr/bin/env python3 +"""Bounded independent equality-cut audit; Hiroki KUMAZAKI / OpenAI Codex. + +Apache-2.0. Reads pinned proof inputs, imports only this package's separately +written checkers, and compares a deterministic receipt. No Git or network. +""" +import hashlib +import importlib.util +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def load(name): + # Compile source directly so a stale sibling bytecode cache cannot replace + # the checks even in a direct standalone replay outside the generic runner. + path = PACKAGE / (name + '.py') + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + exec(compile(path.read_bytes(), str(path), 'exec'), module.__dict__) + return module + + +def calculate(): + sources = json.loads((PACKAGE / 'SOURCES.json').read_text()) + inputs = [row for row in sources['files'] if row['usage'] == 'input'] + require(len(inputs) == 3, 'expected proof, README and license inputs') + for row in inputs: + digest = hashlib.sha256((ROOT / row['path']).read_bytes()).hexdigest() + require(digest == row['sha256'], 'source digest mismatch: ' + row['path']) + return { + 'status': 'PASS_NATIVE_EQUALITY_INDEPENDENT_AUDIT', + 'reviewed_source_head': '97db3fb45cd93a350e300781d75440d14e6a1f73', + 'authenticated_inputs': len(inputs), + 'stabilizers': load('stabilizers').run(), + 'contracts': load('contracts').run(), + 'scope': 'PR5588 PROOF.md sections3–5; written all-size proof plus finite exact controls', + 'source_verifier_imported': False, + 'new_kappa_or_supplier_admission': False, + } + + +def main(): + result = calculate() + expected = json.loads((PACKAGE / 'RESULT.json').read_text()) + require(result == expected, 'computed evidence differs from committed RESULT.json') + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main()