diff --git a/research/pauli-history-arbitrary-targets/PROOF.md b/research/pauli-history-arbitrary-targets/PROOF.md new file mode 100644 index 0000000000..8346c9bd5c --- /dev/null +++ b/research/pauli-history-arbitrary-targets/PROOF.md @@ -0,0 +1,242 @@ +# Exact paid-history minimum for arbitrary targets in the full-Pauli model + +This contribution was produced by Nick Petalas. Apache-2.0. + +## 0. Model and source + +The model is the one in JoyboyBrian's +[PR #5482](https://github.com/CrocSwap/integer-mult-bounds/pull/5482) +(`research/pauli-twisted-history-threshold/PROOF.md`, pinned in +SOURCES.json). Let K=Q(i), X=[[0,1],[1,0]], Z=diag(1,-1), and fix a positive +width f. Put V=(K^2)^tensor f, P=X^tensor f, C=Z^tensor f and +R=span_K{I,P,C,PC}. A field is a row (A_1,...,A_N) in End_K(V)^N, meaning +sum_v A_v w_v for N independent whole-field inputs w_v. Ordinary operations +are left multiplication by elements of R, K-linear row combinations, COPY +and CLEAR. Each paid call returns one additional row. The initial history +is I0=R^N. After returns t_1,...,t_m every available field lies in + + M = I0 + R t_1 + ... + R t_m, (0) + +because ordinary operations preserve this left R-module and each return +adjoins one row. #5482 proves (0) and the predecessor facts used below: +P^2=C^2=I, PC=(-1)^f CP, and dim R=4. We cite these. We do not recheck them. + +The new question is the predecessor's own open boundary: it "does not +classify arbitrary Pauli-nonordinary matrices." Here the requested outputs +are H_j e_(v_j) for q distinct owners v_j and **arbitrary** H_j in End_K(V), +up to ordinary background. Equivalently H_j e_(v_j) lies in M. + +The **history minimum** m*(H_1,...,H_q) is the least m for which returns +t_1,...,t_m exist with every H_j e_(v_j) in M. Every #5482 program satisfies +(0), so m* is a lower bound on its paid returns. The returns achieving m* +below are explicit rows. Whether one native paid operator applied to one +current field can produce them is a separate question, which this package +does not decide (Section 5). + +## 1. Structure of R + +**Even f.** P and C commute, so R is commutative, with four orthogonal +idempotents + + E_(e,h) = (I + eP)(I + hC)/4, e,h in {+1,-1}, + +summing to I. They satisfy E_chi r = chi(r) E_chi for the character chi of R +with chi(P)=e and chi(C)=h. So E_chi R = K E_chi. Each E_chi has trace +2^(f-2), because P, C and PC are traceless for f>=1. + +**Odd f.** PC=-CP. Put e11=(I+P)/2, e22=(I-P)/2, e12=(I+P)C/2 and +e21=(I-P)C/2. Since C(I-P)=(I+P)C, these satisfy the matrix-unit relations +e_ab e_cd = delta_bc e_ad. Thus R is isomorphic to M_2(K). Every left +R-module is semisimple and isomorphic to S^d for the two-dimensional simple +module S. As a left module R is isomorphic to S^2. On V, R acts as +S^(2^(f-1)), so every nonzero element of R has rank at least 2^(f-1). + +## 2. Theorem 1: the exact minimum for arbitrary targets + +For a target H define its **nonordinary invariant**: + +* even f: the profile Pi(H) = {chi : E_chi H is not in K E_chi}; +* odd f: the excess s(H) = (dim_K(R + R H) - 4)/2, an integer in {0,1,2}. + +**Theorem 1.** For distinct owners and arbitrary H_j, + + even f: m* = max_chi #{ j : chi in Pi(H_j) }, + odd f: m* = ceil( (s(H_1) + ... + s(H_q)) / 2 ). + +*Lower bound, even f.* Left multiplication by E_chi is R-linear because R +is commutative. Apply it to (0): + + E_chi M = (+)_v K E_chi e_v + sum_k K E_chi t_k, + +so dim(E_chi M / E_chi I0) <= m. The vectors E_chi H_j e_(v_j) lie in +E_chi M. Modulo E_chi I0, the j-th one is nonzero exactly when chi is in +Pi(H_j). Distinct owners occupy distinct coordinates, so these vectors are +independent. Hence m >= #{j : chi in Pi(H_j)} for every chi. + +*Lower bound, odd f.* M is a left R-module and each R t_k is a quotient of +R, so dim(M / I0) <= 4m. The module W = I0 + sum_j R H_j e_(v_j) lies in M. +By distinct coordinates, dim(W / I0) = sum_j dim((R + R H_j)/R) = +2 sum_j s(H_j). So 4m >= 2 sum_j s(H_j). + +*Attainment, even f.* For each chi list the owners with chi in Pi(H_j) as +j_(chi,1), j_(chi,2), .... For k = 1,...,mu, with mu the stated maximum, put + + t_k = sum_chi E_chi H_(j_(chi,k)) e_(v_(j_(chi,k))) + +over the characters whose list has a k-th entry. Orthogonality gives +E_chi t_k = E_chi H_j e_(v_j) for the k-th owner j of chi. Then + + H_j e_(v_j) = sum_chi E_chi H_j e_(v_j). + +Each term is either E_chi t_k for some k or, when chi is not in Pi(H_j), an +element c E_chi e_(v_j) of I0. So every target lies in M. + +*Attainment, odd f.* The quotient W / I0 is isomorphic to S^d with +d = sum_j s(H_j). The space e11 (W / I0) has dimension d. Choose lifts +y_1,...,y_d in e11 W, independent modulo I0. For each pair put +t = y_a + e21 y_b. Then e11 t = y_a and e12 t = e11 y_b = y_b, so R t contains +both. An unpaired y is used alone. These ceil(d/2) rows generate W modulo I0. + +**Consequences.** At even width the per-owner count q is forced exactly when +one character is nonordinary for every owner. At odd width it is forced +exactly when at most one owner has excess one and none has excess zero. +Neither holds for arbitrary nonordinary targets. The tensor-power +corollaries below give explicit families where they fail. + +The #5482 family (aI+bX)^tensor f, with ab(a^2-b^2) != 0, has excess 2 at +odd f>=3 by its equation (2). At even f its profile contains (+1,+1) by its +Section 3. So Theorem 1 gives m* = q there, consistent with that result. + +## 3. Corollary 2: every tensor square + +Let f=2 and H=M tensor M for M in M_2(K). For a 2x2 matrix B, let psi_B be +the row vector with psi_B[(x,y)] = B[x,y]. A direct expansion gives + + psi_B^T (M tensor N) = psi_(M^T B N)^T. + +The rows psi_I, psi_X, psi_Z and psi_J, with J=XZ, are left eigenvectors of +(P,C) for the characters (+1,+1), (+1,-1), (-1,+1) and (-1,-1). Each E_chi +has rank one, so E_chi H is in K E_chi exactly when psi_B^T H is a multiple +of psi_B^T. Hence + + Pi(M tensor M) = { B in {I,X,Z} : M^T B M is not in K B }, (1) + +and the singlet character never occurs, since M^T J M = det(M) J. + +**Lemma.** If M^T B M is in K B for two distinct B in {I,X,Z}, then M is in +K{I,X,Z,XZ}. + +*Proof.* Write M=[[a,b],[c,d]]. Then + + M^T M = [[a^2+c^2, ab+cd], [ab+cd, b^2+d^2]], + M^T X M = [[2ac, ad+bc], [ad+bc, 2bd]], + M^T Z M = [[a^2-c^2, ab-cd], [ab-cd, b^2-d^2]]. + +*{I,Z}:* ab+cd = ab-cd = 0, a^2+c^2 = b^2+d^2 and a^2-c^2 = d^2-b^2. +Then ab=cd=0, b^2=c^2 and a^2=d^2. If b=0 then c=0 and M=a diag(1,+-1). +Otherwise a=d=0 and M=b[[0,1],[+-1,0]], which lies in K{X,XZ}. + +*{I,X}:* ac=bd=0, ab+cd=0 and a^2+c^2=b^2+d^2. If a=0 then cd=0. If also +c=0, then b^2+d^2=0 and bd=0 force M=0; otherwise d=0 and c^2=b^2. If a!=0, +then c=0, b=0 and a^2=d^2. Every case lies in K{I,X,Z,XZ}. + +*{X,Z}:* ac=bd=0, ab=cd and a^2-c^2+b^2-d^2=0. If a=0 then cd=0. With c=0, +b^2=d^2 and bd=0 force M=0; with d=0, b^2=c^2. If a!=0, then c=0, b=0 and +a^2=d^2. Again M lies in K{I,X,Z,XZ}. QED. + +Conversely, a Pauli matrix sigma satisfies sigma^T B sigma = +-B for every +Pauli B, so a projectively Pauli M has empty profile. + +**Corollary 2.** If no M_j lies in K{I,X,Z,XZ}, then every profile has two +or three of the characters I, X and Z, and + + m*( M_1^tensor 2, ..., M_q^tensor 2 ) >= ceil(2q/3). + +*Proof.* The profiles have total size at least 2q over three characters. +The bound is attained. 2I+X, 2I+Y and 2I+Z have profiles {I,X}, {X,Z} and +{I,Z}. Take owners of these three types in numbers a, b and c with +a+b+c=q, as equal as possible. The largest character count is +q - min(a,b,c) = ceil(2q/3). For q=3 this gives two returns for three +owners, whereas the per-owner count is three. + +## 4. Corollary 3: every rank-one target at width at least three + +Let M = u w^T with u,w nonzero. Put U = u^tensor f, so H = U (w^tensor f)^T +and every element of R H has rank at most one. + +**Tensor-power lemma.** If v_1,...,v_n in K^2 are pairwise nonproportional +and f >= n-1, then v_1^tensor f,...,v_n^tensor f are linearly independent. +*Proof.* Suppose sum_i c_i v_i^tensor f = 0. Pair it with g_1 tensor ... tensor g_f, +where the g_t are linear forms. Choose forms vanishing at each v_k with +k != i, and pad with forms nonzero at v_i. The result is c_i times a +nonzero number, so c_i = 0. + +Call u a **Pauli eigenvector** if u is an eigenvector of X, Z or XZ. If u is +not one, then u, Xu, Zu and XZu are pairwise nonproportional. For instance, +Xu proportional to Zu would make u an eigenvector of ZX, which is +proportional to XZ. By the lemma, RU = span{U, PU, CU, PCU} has dimension 4 +for f>=3. If u is a Pauli eigenvector sigma u = lambda u, then sigma^tensor f +fixes the line of U. Then RU = span{U, tau U} for a second Pauli tau, of +dimension 2 by the lemma. + +**Odd f>=3.** Nonzero elements of R have rank at least 2^(f-1) >= 4 > 1, so +R intersect RH = {0} and dim(R+RH) = 4 + dim RU. Therefore + + s(u w^T tensor power) = 1 if u is a Pauli eigenvector, else 2. + +So q rank-one owners whose u_j are Pauli eigenvectors need exactly +ceil(q/2) returns in the history minimum. For example, two owners with +targets E11^tensor f need one. + +**Even f>=4.** E_chi has rank 2^(f-2) >= 4, and E_chi H = (E_chi U) w^T has +rank at most one. Hence E_chi H lies in K E_chi only when E_chi U = 0, and +Pi(H) = {chi : E_chi U != 0}. If u is not a Pauli eigenvector, then +E_chi U = (1/4) sum_r chi(r) r U is a nonzero combination of four +independent vectors, so all four characters occur. Otherwise exactly two +occur: + +| u | profile | +|---|---| +| X-eigenvector (1,+-1) | {(+1,+1), (+1,-1)} | +| Z-eigenvector e_1 or e_2 | {(+1,+1), (-1,+1)} | +| XZ-eigenvector (1,+-i), f = 0 mod 4 | {(+1,+1), (-1,-1)} | +| XZ-eigenvector (1,+-i), f = 2 mod 4 | {(+1,-1), (-1,+1)} | + +*Proof for the table.* For an X-eigenvector PU = U, which kills e=-1. +(I+hC)U is nonzero because U and CU are independent. The Z case is +symmetric. For u=(1,+-i), PC U = lambda^f U with lambda^f = (-1)^(f/2), so +only characters with eh = (-1)^(f/2) can survive. For such a character a +direct expansion gives (I+eP)(I+hC)U = 2U + (h + e(+-i)^f) CU, which is +nonzero. + +So when f = 0 mod 4, all Pauli-eigenvector rank-one profiles share (+1,+1), +and q such owners need q returns. When f = 2 mod 4, the three types give +the same ceil(2q/3) sharing as Corollary 2. + +## 5. Scope and limitations + +* m* is the exact minimum of the one-row-per-return history count of + #5482. The lower bound applies to every #5482 program. Attainment uses + explicit returned rows, and Theorem 1 does not show that a native paid + operator applied to one current field produces them. #5482's own upper + bound has the same kind of hypothesis: each requested H_j must be an + available paid primitive. +* Corollaries 2 and 3 cover every tensor square and every rank-one tensor + power at f>=3. Invertible non-Pauli M at f>=3 is **not** classified here. + The verifier finds full invariants (excess 2, or all four characters) for + the tested invertible cases at f=3,4,5. Those are finite observations, not + a proof. +* No paid-call bound for a physical caller, no recursive profile and no κ + change follow. Nonlinear programs, approximation, multiple outputs per + call and changed geometry are excluded, as in #5482. + +## Credit + +JoyboyBrian's PR #5482 supplies the model, the history-module inclusion (0), +the algebra facts it proves, and the q-call theorem for (aI+bX)^tensor f. +That package credits Chris R / Clear1nsight, the PR5425/PR5446 history +authors and Ali Romman's PR5450, and those credits carry over. Theorem 1, +the module decomposition, the width-two classification, the rank-one +classification and the sharing constructions are new here. The algebra +used is classical: matrix units, semisimple modules and tensor-power +independence. diff --git a/research/pauli-history-arbitrary-targets/README.md b/research/pauli-history-arbitrary-targets/README.md new file mode 100644 index 0000000000..433cd5e526 --- /dev/null +++ b/research/pauli-history-arbitrary-targets/README.md @@ -0,0 +1,106 @@ +# Exact full-Pauli paid-history minimum for arbitrary targets + +This contribution was produced by Nick Petalas. Apache-2.0. + +JoyboyBrian's [PR #5482](https://github.com/CrocSwap/integer-mult-bounds/pull/5482) +proves that, in its phase-complete Pauli history model, q owners with +targets `(aI+bX)^tensor f` need q paid returns at every width f>=2. It +states that it "does not classify arbitrary Pauli-nonordinary matrices." +This package answers that question for the model's history count. + +**Theorem 1 (scoped proof).** For arbitrary targets H_j on distinct owners, +the least number of returned rows is exactly + +* even f: the largest number of owners whose target is nonordinary in one + common character of the commutative algebra `R=span{I,P,C,PC}`; +* odd f: `ceil(sum_j s_j / 2)`, where `R` is isomorphic to `M_2(K)` and + `s_j = (dim(R+R H_j)-4)/2` is in {0,1,2}. + +The lower bound holds for every program in the #5482 model. Explicit +returned rows attain it. + +So the per-owner count q is not a floor for general nonordinary targets: + +* **Every tensor square (f=2).** The profile of `M tensor M` is the set of + forms B in {I,X,Z} with `M^T B M` not proportional to B. For M not a + scalar multiple of a Pauli, it has two or three members. The minimum is + at least `ceil(2q/3)`, and this is sharp. Owners with targets + `(2I+X)^tensor 2`, `(2I+Y)^tensor 2` and `(2I+Z)^tensor 2` need **two** + returns, not three. +* **Every rank-one tensor power (f>=3).** For `M=u w^T`, the odd-width excess + is 1 if u is an eigenvector of X, Z or XZ, and 2 otherwise. Two such + owners, for example `E11^tensor 3` twice, share **one** return. At even + widths the profile has four characters, or two for Pauli eigenvectors; + [PROOF.md](PROOF.md) tabulates them by f mod 4. These profiles force q + when f = 0 mod 4 and allow `ceil(2q/3)` when f = 2 mod 4. + +At even width the count q is forced exactly when one character is shared +by every owner. At odd width it is forced exactly when at most one owner +has excess 1 and none has excess 0. The #5482 family satisfies both +conditions, consistent with that result. + +No κ, physical paid-call count or selected-frontier change is claimed. + +## Reproduce + +From the repository root, with CPython 3.12 (standard library only): + +```sh +python3.12 -B scripts/research_package.py --package research/pauli-history-arbitrary-targets +python3.12 -W error -B research/pauli-history-arbitrary-targets/verify.py +python3.12 -O -W error -B research/pauli-history-arbitrary-targets/verify.py +``` + +Each verifier run takes about two seconds and prints a JSON receipt with +`PASS_PAULI_HISTORY_ARBITRARY_TARGETS` and SHA-256 hashes of the package +files. It checks the cited proof's hash and uses exact Q(i) arithmetic: + +* The algebra identities at widths 1 to 5. +* Eleven target instances at widths 2 to 5. For each, the formula value, + explicit attaining returns, exact membership of every target in the + history module, and failure after dropping one return. +* All 625 width-two matrices with entries in {0,±1,±i}. The character + profile equals the form profile (1), the singlet never occurs, and + non-Pauli profiles have two or three characters. Size counts are + 17, 192 and 416 for sizes 0, 2 and 3. +* 48 vectors u at widths 3 to 9: dim RU is 2 exactly for the 30 Pauli + eigenvectors. +* The even-width rank-one profile table at widths 4, 6 and 8. +* Five rejection controls. + +The finite checks corroborate the written all-width proof. They do not +replace it. + +## Limitations + +The minimum counts returned rows in the #5482 history model. Its lower bound +applies to every program in that model. The attaining rows are explicit, but +this package does not show that a native operator applied to one current +field produces them. Invertible non-Pauli tensor powers at widths at least +three are not classified. The verifier observes full invariants there only +for finitely many tested matrices. + +## Open next questions + +1. **Invertible targets at f>=3.** Does every invertible `M` outside + `K{I,X,Z,XZ}` have excess 2 at odd f>=3 and all four characters at even + f>=4? If so, the q-call count of #5482 extends to all invertible + nonordinary tensor powers. First step: the condition `r M^tensor f in R` + is a linear relation among the eight tensor powers of `σM` and `σ`; + handle the low widths 3 to 6, where the tensor-power lemma alone is too + weak. +2. **Operator realizability of sharing.** Can two paid calls, each a fixed + linear operator applied to one current field, deliver the three width-two + X/Y/Z-type targets? A positive answer turns the history sharing into a + program. A negative answer gives a stronger operator-call floor than + Theorem 1. +3. **Physical caller.** A cached physical boundary must still bind its actual + observation module and complete paid bill before either count is charged. + +## Credit + +JoyboyBrian (PR #5482) supplies the model, the history-module inclusion and +the q-call theorem for `(aI+bX)^tensor f`. That package's credits carry +over: Chris R / Clear1nsight, the PR5425/PR5446 history authors and Ali +Romman's PR5450. Theorem 1, the two classifications and the sharing +constructions are new here. The algebra is classical. diff --git a/research/pauli-history-arbitrary-targets/SOURCES.json b/research/pauli-history-arbitrary-targets/SOURCES.json new file mode 100644 index 0000000000..04a0c89e28 --- /dev/null +++ b/research/pauli-history-arbitrary-targets/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/pauli-twisted-history-threshold/PROOF.md", + "usage": "input", + "git_blob": "c09c2bd7ee4b98846a5793a9cffb4e20e4f7b018", + "sha256": "f3f3972133a614cf9406cee6cfb78e62f51fad4fd57a1ed367467c75af1c2001" + } + ] +} diff --git a/research/pauli-history-arbitrary-targets/TASK.json b/research/pauli-history-arbitrary-targets/TASK.json new file mode 100644 index 0000000000..f9a91474ba --- /dev/null +++ b/research/pauli-history-arbitrary-targets/TASK.json @@ -0,0 +1,91 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Determine the exact paid-history minimum for arbitrary requested targets in the PR #5482 phase-complete Pauli model, and classify every tensor square and every rank-one tensor power at width at least three.", + "scope_change_reason": "The audit card is narrowed to the explicit open boundary of JoyboyBrian PR #5482, which does not classify arbitrary Pauli-nonordinary targets. This is a new scoped history-model theorem, not an audit of a #4100 obligation or a recheck of the predecessor.", + "bottleneck_link": "History-dimension floors price helper returns at cached boundaries; the exact minimum shows when per-owner charging is forced and when owners can share a return.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact arbitrary-target formula with its width-two and rank-one classifications; leave invertible targets at widths three and above open.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py exact Q(i) finite corroboration with generated hash-bound stdout receipt", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does every invertible M outside K{I,X,Z,XZ} have excess 2 at odd widths f>=3 and all four characters at even widths f>=4?", + "why_it_matters": "A positive answer extends the q-call count of PR #5482 to all invertible nonordinary tensor powers.", + "first_step": "Write r M^tensor f in R as a linear relation among the eight tensor powers of sigma M and sigma, and treat widths 3 to 6 separately.", + "blocked_by": "The tensor-power independence lemma needs f>=7 for eight vectors; the tested invertible cases are finite observations only." + }, + { + "question": "Can two paid calls, each a fixed linear operator applied to one current field, deliver the three width-two X/Y/Z-type targets?", + "why_it_matters": "It decides whether history sharing is realizable as a program or whether operator calls obey a stronger floor.", + "first_step": "Write the returns in the Bell basis and solve the bilinear system for two operators and two ordinary fields.", + "blocked_by": "Theorem 1 constructs returned rows, not operators acting on a single field." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19225349", + "question_source": "PR #5482" +} diff --git a/research/pauli-history-arbitrary-targets/VERIFY.json b/research/pauli-history-arbitrary-targets/VERIFY.json new file mode 100644 index 0000000000..d266fa581e --- /dev/null +++ b/research/pauli-history-arbitrary-targets/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/pauli-twisted-history-threshold/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Algebra identities, eleven attained instances with drop-one controls, width-two census of 625 matrices, rank-one dimension census at widths 3-9, even-width rank-one profiles and rejection controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete finite check with optimization; every check uses explicit exceptions." + } + ] +} diff --git a/research/pauli-history-arbitrary-targets/verify.py b/research/pauli-history-arbitrary-targets/verify.py new file mode 100644 index 0000000000..a280373bf0 --- /dev/null +++ b/research/pauli-history-arbitrary-targets/verify.py @@ -0,0 +1,534 @@ +"""Exact finite corroboration of the arbitrary-target Pauli history minimum. + +Standard library only. Arithmetic is exact over K = Q(i). Every check raises +an exception on failure and stays active under -O. The written all-width +proof is PROOF.md; this program checks its finite instances and controls. +""" +from fractions import Fraction +from hashlib import sha256 +from itertools import product +from pathlib import Path +import json +import sys + +PACKAGE = Path(__file__).resolve().parent +SOURCE = "research/pauli-twisted-history-threshold/PROOF.md" +MAX_WIDTH_MATRIX = 5 # full End(V) computations: 32 x 32 matrices +MAX_WIDTH_VECTOR = 9 # tensor-power vector computations: 512 entries +MAX_OWNERS = 6 + + +class Check(Exception): + pass + + +def require(condition, label): + if not condition: + raise Check(label) + + +# ---------------------------------------------------------------- Q(i) +ZERO = (Fraction(0), Fraction(0)) +ONE = (Fraction(1), Fraction(0)) +IU = (Fraction(0), Fraction(1)) + + +def q(re, im=0): + return (Fraction(re), Fraction(im)) + + +def add(a, b): + return (a[0] + b[0], a[1] + b[1]) + + +def sub(a, b): + return (a[0] - b[0], a[1] - b[1]) + + +def mul(a, b): + return (a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0]) + + +def inv(a): + n = a[0] * a[0] + a[1] * a[1] + require(n != 0, "inverse of zero") + return (a[0] / n, -a[1] / n) + + +def nz(a): + return a[0] != 0 or a[1] != 0 + + +# ------------------------------------------------------------ matrices +def eye(n): + return [[ONE if i == j else ZERO for j in range(n)] for i in range(n)] + + +def matmul(a, b): + n, k, m = len(a), len(b), len(b[0]) + out = [[ZERO] * m for _ in range(n)] + for i in range(n): + row = out[i] + for t in range(k): + x = a[i][t] + if not nz(x): + continue + bt = b[t] + for j in range(m): + if nz(bt[j]): + row[j] = add(row[j], mul(x, bt[j])) + return out + + +def kron(a, b): + return [[mul(a[i][j], b[k][l]) for j in range(len(a[0])) for l in range(len(b[0]))] + for i in range(len(a)) for k in range(len(b))] + + +def tensor_power(m, f): + require(1 <= f <= MAX_WIDTH_MATRIX, "matrix width capacity") + out = [[ONE]] + for _ in range(f): + out = kron(out, m) + return out + + +def madd(a, b): + return [[add(x, y) for x, y in zip(ra, rb)] for ra, rb in zip(a, b)] + + +def mscale(c, a): + return [[mul(c, x) for x in r] for r in a] + + +def transpose(a): + return [list(r) for r in zip(*a)] + + +X = [[ZERO, ONE], [ONE, ZERO]] +Z = [[ONE, ZERO], [ZERO, q(-1)]] +XZ = matmul(X, Z) +PAULI = [eye(2), X, Z, XZ] + + +def algebra(f): + """Return P, C and the basis I, P, C, PC of R at width f.""" + p, c = tensor_power(X, f), tensor_power(Z, f) + return p, c, [eye(2 ** f), p, c, matmul(p, c)] + + +# --------------------------------------------------- sparse echelon span +class Span: + """Incremental exact row echelon basis over Q(i) for sparse vectors.""" + + def __init__(self): + self.rows = {} # pivot key -> normalized sparse vector + + def reduce(self, vec): + v = {k: x for k, x in vec.items() if nz(x)} + for _ in range(len(self.rows) + 1): + hit = next((k for k in sorted(v) if k in self.rows), None) + if hit is None: + return v + c = v[hit] + for k, x in self.rows[hit].items(): + y = sub(v.get(k, ZERO), mul(c, x)) + if nz(y): + v[k] = y + else: + v.pop(k, None) + raise Check("echelon reduction did not terminate") + + def add(self, vec): + v = self.reduce(vec) + if not v: + return False + pivot = min(v) + s = inv(v[pivot]) + v = {k: mul(s, x) for k, x in v.items()} + for key, row in self.rows.items(): + c = row.get(pivot) + if c is not None and nz(c): + for k, x in v.items(): + y = sub(row.get(k, ZERO), mul(c, x)) + if nz(y): + row[k] = y + else: + row.pop(k, None) + self.rows[pivot] = v + return True + + def contains(self, vec): + return not self.reduce(vec) + + def dim(self): + return len(self.rows) + + +def flat(row): + """A history row is a tuple of N matrices; flatten to a sparse vector.""" + out = {} + for v, a in enumerate(row): + for i, r in enumerate(a): + for j, x in enumerate(r): + if nz(x): + out[(v, i, j)] = x + return out + + +def unit_row(n_owners, owner, mat): + size = len(mat) + zero = [[ZERO] * size for _ in range(size)] + return tuple(mat if v == owner else zero for v in range(n_owners)) + + +def left(r, row): + return tuple(matmul(r, a) for a in row) + + +def row_add(a, b): + return tuple(madd(x, y) for x, y in zip(a, b)) + + +# ------------------------------------------- invariants of a target H +def characters(f): + p, c, _ = algebra(f) + n = 2 ** f + out = {} + for e, h in product((1, -1), repeat=2): + a = madd(eye(n), mscale(q(e), p)) + b = madd(eye(n), mscale(q(h), c)) + out[(e, h)] = mscale(q(Fraction(1, 4)), matmul(a, b)) + return out + + +def even_profile(h, f, chars): + """Characters chi with E_chi H outside K E_chi.""" + out = [] + for key, e in chars.items(): + s = Span() + s.add(flat((e,))) + if s.add(flat((matmul(e, h),))): + out.append(key) + return tuple(sorted(out, reverse=True)) + + +def odd_excess(h, f, basis): + """s(H) = (dim(R + R H) - 4) / 2 at odd width.""" + s = Span() + for r in basis: + s.add(flat((r,))) + require(s.dim() == 4, "dim R = 4") + for r in basis: + s.add(flat((matmul(r, h),))) + d = s.dim() - 4 + require(d % 2 == 0, "R-module dimension is even at odd width") + return d // 2 + + +def minimum(targets, f): + """The exact history minimum mu of PROOF.md Theorem 1.""" + require(1 <= len(targets) <= MAX_OWNERS, "owner capacity") + if f % 2 == 0: + chars = characters(f) + prof = [even_profile(h, f, chars) for h in targets] + return max((sum(1 for p in prof if k in p) for k in chars), default=0), prof + _, _, basis = algebra(f) + ex = [odd_excess(h, f, basis) for h in targets] + return (sum(ex) + 1) // 2, ex + + +# ------------------------------------------------- attaining returns +def even_returns(targets, f): + chars = characters(f) + n = len(targets) + mu, prof = minimum(targets, f) + returns = [] + for k in range(mu): + t = unit_row(n, 0, [[ZERO] * 2 ** f for _ in range(2 ** f)]) + for key, e in chars.items(): + owners = [j for j in range(n) if key in prof[j]] + if k < len(owners): + j = owners[k] + t = row_add(t, unit_row(n, j, matmul(e, targets[j]))) + returns.append(t) + return returns + + +def odd_returns(targets, f): + p, c, basis = algebra(f) + n, size = len(targets), 2 ** f + e11 = mscale(q(Fraction(1, 2)), madd(eye(size), p)) + e21 = mscale(q(Fraction(1, 2)), matmul(madd(eye(size), mscale(q(-1), p)), c)) + span = Span() + for v in range(n): + for r in basis: + span.add(flat(unit_row(n, v, r))) + ys = [] + for j, h in enumerate(targets): + for r in basis: + y = left(e11, unit_row(n, j, matmul(r, h))) + if span.add(flat(y)): + ys.append(y) + returns = [] + for k in range(0, len(ys), 2): + t = ys[k] if k + 1 == len(ys) else row_add(ys[k], left(e21, ys[k + 1])) + returns.append(t) + return returns + + +def history_contains_targets(targets, f, returns): + """Every H_j e_j lies in I0 + sum_k R t_k.""" + _, _, basis = algebra(f) + n = len(targets) + span = Span() + for v in range(n): + for r in basis: + span.add(flat(unit_row(n, v, r))) + for t in returns: + for r in basis: + span.add(flat(left(r, t))) + return all(span.contains(flat(unit_row(n, j, h))) for j, h in enumerate(targets)) + + +def certify_instance(name, targets, f, expected_mu): + mu, invariant = minimum(targets, f) + require(mu == expected_mu, f"{name}: formula value") + returns = even_returns(targets, f) if f % 2 == 0 else odd_returns(targets, f) + require(len(returns) == mu, f"{name}: construction size") + require(history_contains_targets(targets, f, returns), f"{name}: attainment") + if mu > 0: + require(not history_contains_targets(targets, f, returns[:-1]), + f"{name}: dropping one return must fail") + return {"name": name, "width": f, "owners": len(targets), "mu": mu, + "invariant": [list(x) if isinstance(x, tuple) else x for x in invariant]} + + +# --------------------------------------------------- named 2 x 2 targets +def m2(a, b, c, d): + return [[a, b], [c, d]] + + +Y_LIKE = m2(q(2), q(0, -1), q(0, 1), q(2)) # 2I + Y +TARGETS = { + "2I+X": m2(q(2), q(1), q(1), q(2)), + "2I+Y": Y_LIKE, + "2I+Z": m2(q(3), ZERO, ZERO, q(1)), + "E11": m2(ONE, ZERO, ZERO, ZERO), + "(1,1)(1,1)^T": m2(ONE, ONE, ONE, ONE), + "(1,i)(1,i)^T": m2(ONE, IU, IU, q(-1)), + "(1,2)(1,0)^T": m2(ONE, ZERO, q(2), ZERO), + "diag(1,i)": m2(ONE, ZERO, ZERO, IU), + "generic": m2(q(1, 1), q(2), q(-1, 3), q(0, -2)), +} + + +def instances(): + t = TARGETS + cases = [ + ("width2 X,Y,Z types", ["2I+X", "2I+Y", "2I+Z"], 2, 2), + ("width2 two of each type", ["2I+X", "2I+Y", "2I+Z"] * 2, 2, 4), + ("width2 predecessor family", ["2I+X"] * 3, 2, 3), + ("width2 S gate and generic", ["diag(1,i)", "generic"], 2, 2), + ("width3 two rank-one Pauli eigen", ["E11", "(1,1)(1,1)^T"], 3, 1), + ("width3 rank-one with invertible", ["E11", "(1,i)(1,i)^T", "2I+X"], 3, 2), + ("width3 generic rank-one", ["(1,2)(1,0)^T", "E11"], 3, 2), + ("width3 predecessor family", ["2I+X", "2I+Z"], 3, 2), + ("width4 rank-one Pauli eigen", ["E11", "(1,1)(1,1)^T", "(1,i)(1,i)^T"], 4, 3), + ("width4 invertible", ["2I+Y", "generic"], 4, 2), + ("width5 two rank-one Pauli eigen", ["E11", "(1,i)(1,i)^T"], 5, 1), + ] + out = [] + for name, keys, f, mu in cases: + out.append(certify_instance(name, [tensor_power(t[k], f) for k in keys], f, mu)) + return out + + +# ------------------------------------------------ width-two classification +FORMS = {(1, 1): eye(2), (1, -1): X, (-1, 1): Z, (-1, -1): m2(ZERO, ONE, q(-1), ZERO)} + + +def proportional(a, b): + s = Span() + s.add(flat((b,))) + return s.contains(flat((a,))) + + +def form_profile(m): + mt = transpose(m) + return tuple(sorted((k for k, b in FORMS.items() + if not proportional(matmul(matmul(mt, b), m), b)), reverse=True)) + + +def projectively_pauli(m): + return any(proportional(m, s) for s in PAULI) + + +def width_two_census(): + """All 625 matrices with entries in {0, 1, -1, i, -i}.""" + chars = characters(2) + vals = [ZERO, ONE, q(-1), IU, q(0, -1)] + sizes = {} + for a, b, c, d in product(vals, repeat=4): + m = m2(a, b, c, d) + prof = even_profile(tensor_power(m, 2), 2, chars) + require(prof == form_profile(m), "character profile equals form profile") + require((-1, -1) not in prof, "singlet character is always ordinary") + pp = projectively_pauli(m) + require(pp == (len(prof) == 0), "empty profile iff projectively Pauli") + require(pp or len(prof) >= 2, "non-Pauli profile has at least two characters") + sizes[len(prof)] = sizes.get(len(prof), 0) + 1 + return {"matrices": 625, "profile_size_counts": {str(k): sizes[k] for k in sorted(sizes)}} + + +# ------------------------------------------------ rank-one classification +def vec_power(u, f): + out = [ONE] + for _ in range(f): + out = [mul(x, y) for x in out for y in u] + return out + + +def apply2(m, u): + return [add(mul(m[0][0], u[0]), mul(m[0][1], u[1])), + add(mul(m[1][0], u[0]), mul(m[1][1], u[1]))] + + +def pauli_eigen(u): + for s in PAULI[1:]: + w = apply2(s, u) + if not nz(sub(mul(w[0], u[1]), mul(w[1], u[0]))): + return True + return False + + +def rank_one_census(): + vals = [ZERO, ONE, q(-1), IU, q(0, -1), q(2), q(1, 1)] + us = [[a, b] for a, b in product(vals, repeat=2) if nz(a) or nz(b)] + counts = {"vectors": len(us), "pauli_eigen": 0, "widths": []} + for f in range(3, MAX_WIDTH_VECTOR + 1): + counts["widths"].append(f) + for u in us: + span = Span() + for s in PAULI: + span.add({k: x for k, x in enumerate(vec_power(apply2(s, u), f))}) + expected = 2 if pauli_eigen(u) else 4 + require(span.dim() == expected, "dim R u^f is 2 iff u is a Pauli eigenvector") + counts["pauli_eigen"] = sum(1 for u in us if pauli_eigen(u)) + return counts + + +def rank_one_even_profiles(): + """Predicted two-character profiles for Pauli eigenvectors at even widths.""" + cases = {"E11": [ONE, ZERO], "(1,1)": [ONE, ONE], "(1,i)": [ONE, IU]} + out = {} + for f in (4, 6, 8): + for name, u in cases.items(): + vecs = [vec_power(apply2(s, u), f) for s in PAULI] + prof = [] + for e, h in product((1, -1), repeat=2): + coef = [ONE, q(e), q(h), q(e * h)] + w = [ZERO] * len(vecs[0]) + for a, v in zip(coef, vecs): + w = [add(x, mul(a, y)) for x, y in zip(w, v)] + if any(nz(x) for x in w): + prof.append([e, h]) + sign = 1 if f % 4 == 0 else -1 + expected = {"E11": [[1, 1], [-1, 1]], "(1,1)": [[1, 1], [1, -1]], + "(1,i)": [[1, 1], [-1, -1]] if sign == 1 else [[1, -1], [-1, 1]]}[name] + require(prof == expected, f"rank-one even profile {name} width {f}") + out[f"{name}@{f}"] = prof + return out + + +# -------------------------------------------------------------- controls +def controls(): + results = [] + + def expect_fail(label, fn): + try: + fn() + except Check: + results.append(label) + return + raise Check(f"control accepted: {label}") + + t = TARGETS + expect_fail("per-owner count q claimed for the width-two X,Y,Z instance", + lambda: certify_instance("bad", [tensor_power(t[k], 2) for k in ("2I+X", "2I+Y", "2I+Z")], 2, 3)) + expect_fail("one return claimed for two invertible owners at width three", + lambda: certify_instance("bad", [tensor_power(t[k], 3) for k in ("2I+X", "2I+Z")], 3, 1)) + + def corrupted_return(): + hs = [tensor_power(t[k], 2) for k in ("2I+X", "2I+Y", "2I+Z")] + rs = even_returns(hs, 2) + rs[0] = rs[1] + require(history_contains_targets(hs, 2, rs), "duplicated return") + expect_fail("first return replaced by a copy of the second", corrupted_return) + + def pauli_target_nonordinary(): + chars = characters(2) + require(even_profile(tensor_power(XZ, 2), 2, chars) != (), "Pauli target") + expect_fail("projectively Pauli target declared nonordinary", pauli_target_nonordinary) + + def width_one(): + _, ex = minimum([tensor_power(t["generic"], 1)], 1) + require(ex[0] > 0, "width one") + expect_fail("width-one target declared nonordinary", width_one) + return results + + +def algebra_checks(): + out = [] + for f in range(1, MAX_WIDTH_MATRIX + 1): + p, c, basis = algebra(f) + n = 2 ** f + require(matmul(p, p) == eye(n) and matmul(c, c) == eye(n), "involutions") + sign = q(1 if f % 2 == 0 else -1) + require(matmul(p, c) == mscale(sign, matmul(c, p)), "PC = (-1)^f CP") + s = Span() + for r in basis: + s.add(flat((r,))) + require(s.dim() == 4, "dim R = 4") + if f % 2 == 0: + chars = characters(f) + total = None + for e in chars.values(): + require(matmul(e, e) == e, "idempotent") + total = e if total is None else madd(total, e) + require(total == eye(n), "character idempotents sum to I") + out.append(f) + return out + + +def file_hashes(): + records = json.loads((PACKAGE / "SOURCES.json").read_text())["files"] + src = next(r for r in records if r["path"] == SOURCE) + digest = sha256((PACKAGE.parents[1] / SOURCE).read_bytes()).hexdigest() + require(digest == src["sha256"], "cited source proof hash") + files = sorted(p for p in PACKAGE.iterdir() if p.is_file() and p.suffix in {".md", ".json", ".py"}) + require(len(files) <= 10, "package receipt file capacity") + return {p.name: sha256(p.read_bytes()).hexdigest() for p in files} + + +def main(): + receipt = { + "algebra_widths": algebra_checks(), + "instances": instances(), + "width_two_census": width_two_census(), + "rank_one_dimension_census": rank_one_census(), + "rank_one_even_profiles": rank_one_even_profiles(), + "controls": controls(), + "file_sha256": file_hashes(), + "marker": "PASS_PAULI_HISTORY_ARBITRARY_TARGETS", + } + print(json.dumps(receipt, indent=1, sort_keys=True)) + return 0 + + +if __name__ == "__main__": + try: + sys.exit(main()) + except (Check, ValueError) as exc: + print(f"FAIL: {exc}", file=sys.stderr) + sys.exit(1)