diff --git a/research/clifford-pointwise-audit/AUDIT.md b/research/clifford-pointwise-audit/AUDIT.md new file mode 100644 index 0000000000..e033bd1ff7 --- /dev/null +++ b/research/clifford-pointwise-audit/AUDIT.md @@ -0,0 +1,228 @@ +# Independent audit of the pointwise Clifford tensor bound + +Prepared for DLamdata with substantial OpenAI Codex assistance. Apache-2.0. +This is a written mathematical audit with exact finite corroboration, not a +formal-kernel proof or independent human review. + +## Verdict and source boundary + +No substantive gap was found in Sections 2–5 of Ali Romman's +[PR5526](https://github.com/CrocSwap/integer-mult-bounds/pull/5526), at +`45f7de73b168721cdf7ec8c1769b1b594493716a`. The immutable +[source proof](source/PR5526-PROOF.md) has SHA256 +`45483e4b5f604a5e70602c5caaa4394d4a0d0d1a6d0b6e8a93b836d50b23f764`. +The theorem, constants and constructions remain the predecessor's work. + +The audited statements are the stabilizer overlap count, the first Clifford +overlap count and general upper bound, the uniform rational Gram estimates, +and the exact central-phase/four-width implication. The source's later +paid-repair theorem, cost invoice, actual passive-caller binding, native frontend +implementation and selected multiplication construction are **not audited here**. +In particular, this result alone does not accept PR5526's 104-return conclusion. + +One verifier agent derived the symplectic and phase implications before seeing +any lead checker or result; a second reviewer derived the proof audit before +verdict comparison. The lead separately implemented literal Gaussian matrices. +These are independent AI-assisted approaches, with shared classical assumptions +and Python integer/rational arithmetic. They are not independent human reviews. +The lead read the source's census code to distinguish its coverage; the independent +binary-matrix checker imported and read no predecessor executable. The source +already has a projective Choi orbit and signed-Pauli census. Our literal matrix +orbit is related finite corroboration, not a new census theorem. The independent +exhaustive binary-matrix path, residual-form checks, full central extension and +written audit are the added review evidence. + +## 1. The exact phase group really has four elements + +Let R=Z[i,1/2]. If alpha I is unitary and has entries in R, write +alpha=(a+ib)/2^k. Then a^2+b^2=4^k. For k>0, reduction modulo four makes both +integers even; descent leaves alpha in {1,i,-1,-i}. If U and V in the group are +projectively equal, their scalar ratio belongs to R because UV* does. Thus the +argument does not rely on dividing an arbitrary matrix entry in R. + +The ordinary Hadamard is not itself in R. This does not remove projective +Cliffords: H'=(1+i)/2 [[1,1],[1,-1]] is unitary in R and induces the same Pauli +label action. H', S=diag(1,i) and CNOT supply the usual projective generators. +The classical Clifford-to-symplectic surjection and its Pauli kernel therefore +apply to these Gaussian-dyadic representatives. For the first-overlap equality +one can directly realize every transvection: for a nonidentity Hermitian Pauli +P_a, V_a=(1+i)(I-iP_a)/2 is Gaussian-dyadic, unitary, and induces the +transvection at a. This makes explicit an implicit lift step in the source; +no change to its theorem is needed. + +The matrix checker retains these phases during generation: (H')^2=iI. +It obtains 96 and 46,080 exact matrices on one and two axes, with exactly four +lifts in each of 24 and 11,520 projective classes. Unitarity is checked on every +projective representative; scalar-unit invariance covers its other three lifts. +Completeness uses the classical group order and generator theorem, not merely +the absence of a new element during enumeration. + +## 2. Stabilizer overlaps and the basis-counting issue + +Fix one coordinate basis for each k-dimensional binary support W. A stabilizer +ray supported on W with its amplitude at zero positive has phase polynomial + + q(t) = sum_j a_j t_j + 2 sum_(j. Those containing +zero are linear subspaces. Therefore the number of rays at squared overlap 2^-k is + + A_(N,k) = [N choose k]_2 2^(k(k+3)/2). + +The k=0 term is the reference ray and is excluded from the off-diagonal sum. +Other singleton supports have zero overlap. Clifford transitivity follows by +removing the support offset, choosing coordinate axes, undoing the quadratic +phase and applying Hadamards. This also proves that every Gram row has the same +absolute-overlap distribution. N=0 has one ray and an empty off-diagonal sum. + +This all-N statement is audited in writing. Our finite checker does not claim a +new exhaustive stabilizer-state census; its 528 bounded checks test the resulting +subspace-term inequality for 1<=N<=32. The predecessor retains its own state census. + +## 3. Why fixed Pauli signs are a character + +Use Hermitian Paulis P_v indexed by V=F2^(2n), with alternating form omega. +For a Clifford lift U of S in Sp(V), let L=ker(S-I). On fixed labels write +UP_v U*=epsilon(v)P_v. In P_v P_w=zeta(v,w)P_(v+w), conjugation preserves the +same zeta on both sides, so epsilon(v+w)=epsilon(v)epsilon(w). This remains true +when v and w anticommute; L need not be isotropic. + +The trace of conjugation on the Pauli basis is sum_(v in L) epsilon(v), while +on the full matrix space it is |tr U|^2. Character orthogonality makes this +zero or 2^dim(L). Multiplication of the lift by P_p changes its sign character +by (-1)^omega(p,v). Restriction V -> L* is onto and has kernel L-perp. Thus, +when rank(S-I)=k, exactly 2^k of the 2^(2n) projective Pauli lifts have nonzero +trace, and their normalized trace magnitude is 2^(-k/2). + +For rank-one displacement, write (S-I)x=ell(x)a. Symplecticity forces the two +nonzero linear forms ell and omega(-,a) to agree over F2. Conversely each +nonzero a defines a transvection x -> x+omega(x,a)a. There are 2^(2n)-1 such +maps and two nonzero-trace lifts each. Hence B_(n,1)=2(2^(2n)-1), half of +A_(2n,1). This factor is essential to the advertised uniform row budget. + +The independent checker tries **all** 16 binary 2x2 matrices and 65,536 binary +4x4 matrices, accepting only literal preservers of omega. It enumerates actual +fixed-space character sums without gate/tableau generation. At n=2 it finds +720 symplectic matrices with displacement counts + + k: 0 1 2 3 4 + symplectic maps: 1 15 100 300 304 + nonzero lifts: 1 30 400 2400 4864. + +The lead's literal trace calculation independently gives the latter distribution +and 3,825 zero-overlap projective classes. The checker relies on the written +identification between these abstract characters and actual Clifford lifts; +the direct matrix calculation corroborates that identification in these two +small dimensions. Neither finite path supplies the universal quantifier. + +## 4. Residual forms: an injection, not a claimed classification + +Put W=im(S-I). Symplecticity gives W-perp=ker(S-I). Therefore + + B((S-I)x,w)=omega(x,w) + +is well defined. If its left argument pairs to zero with W, its preimage lies +in W-perp and the left argument is zero; the right-kernel argument uses +nondegeneracy of omega. Substitution verifies B(u,v)+B(v,u)=omega(u,v). +For each fixed W of dimension k there are 2^(k(k+1)/2) bilinear forms with +this symmetrization, including singular forms. A nonsingular one determines +(S-I)x by its pairings with all w. Consequently S -> (W,B) is injective. +No converse realizing every counted form is needed for the upper bound. + +Counting W and the nonzero-trace lifts gives A_(2n,k) as an upper bound for +Clifford overlaps. The separate rank-one equality improves its first term. +The independent finite checker explicitly tests every preimage choice for B, +its kernel, symmetrization, and uniqueness of (W,B) across the enumerated maps. +These checks target potential failures hidden by simply comparing group totals. + +## 5. The entire tail, including odd widths + +Write d_k=product_(j=1..k)(2^j-1). At f=2N+4 the exact kth stabilizer row term is + + A_(N,k) 2^(-kf/2) + = product_(j=0..k-1)(1-2^(-(N-j))) / d_k <= 1/d_k. + +For Clifford Choi states N=2n, the first term is strictly below 1/2. Retain +terms through k=4; the k=5 tail has successive ratio at most 1/63. At the +extra even-width shift 2s, multiply the kth term by 2^(-sk), so the tail ratio +is at most 1/(63*2^s). The exact independently calculated majorants are: + +| Family/shift | Complete majorant | Required strict upper bound | +|---|---:|---:| +| Clifford s=0 | 53534/60543 | 8/9 | +| Stabilizer at f=2N+6 | 719543/1220625 | 3/5 | +| Clifford s=2 | 359294/2451015 | 3/20 | +| Clifford s=6 | 162912909217/20637399121920 | 1/126 | + +Terms beyond the actual dimension only enlarge the upper bound. Every overlap +has modulus at most one, so increasing f decreases the absolute row sum; this +covers intervening odd widths without a floating-point square root. +For Hermitian Gram diagonal one and row sum at most s, the elementary inequality +2|b_i b_j|<=|b_i|^2+|b_j|^2 gives spectral bounds 1-s and 1+s. It applies to every +subset. Thus the predecessor's Clifford bounds [1/9,17/9] at f>=4n+4 and +stabilizer bounds [2/5,8/5] at f>=2N+6 follow. Vectorization transfers the latter +to rectangular stabilizer maps with the stated norm weights. These are sufficient +bounds, not sharp thresholds or a physical implementation theorem. + +## 6. Four tests have a fixed-program premise + +Write each exact Clifford as i^j U_g for a chosen projective representative. +At width f the coefficient for that projective class is + + beta_(g,f mod 4) = sum_(j=0..3) c_(g,j) i^(jf). + +Pointwise positive Gram bounds identify the kernel exactly after this phase +combination. Four consecutive sufficiently large widths include all four +residues; Fourier inversion forces all **fixed** coefficients c_(g,j) to vanish. +Parseval gives sum_(g,r)|beta_(g,r)|^2=4M, where M=sum_(g,j)|c_(g,j)|^2. +Averaging the four separately normalized squared residual norms gives at least +M/9, hence at least one attains that bound. No common D^-f normalization across +different widths is assumed. For n=0 the same Fourier argument uses widths1..4. + +The necessity witness for residue r is sum_j i^(-rj)[i^j I]. It vanishes in the +other three residues and equals4I in residue r. Keeping U and iU as separate +pointwise columns instead makes a singular Gram matrix. Both failure modes are +checked with exact Gaussian arithmetic. + +Two stronger exclusions are explicit controls in the new matrix checker: + +* Width-dependent formal coefficients c_0(f)=1, c_1(f)=-i^(-f) give a nonzero + formal vector but the zero operator at every width. The pointwise theorem + allows this phase cancellation; it is not a fixed-coefficient certificate. +* For arbitrary nonunitary scalar maps, take + P(x)=product_(j=0..3)(x-2^(8+j))=sum_k c_k x^k. The nonzero residual + sum_k c_k[2^k I] vanishes at widths8..11 and not12. Each scalar map is a + stabilizer map, but the four-test implication does not extend to these scales. + +The source correctly makes these quantifier distinctions. We retain them rather +than promoting its pointwise stabilizer-map statement into a uniform program test. + +## Coverage and remaining obligations + +The independent checks and written arguments support only the scoped core theorem. +They share classical Pauli/Clifford/stabilizer structure, Fourier orthogonality, +and exact arithmetic; no formalization of those foundations was undertaken. +The full predecessor replay was not run: it includes frontend and caller claims +outside this audit. Actual costs, source versions, observation histories, routing, +precision, ownership and admission must be verified at each application. The +selected record and all frozen predecessors remain unchanged. + +This audit answers the independent core-proof portion of the handoff in +[Discussion1166](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19174354). +Its requested passive-contract implication remains a separate review task. +PR5531's application and PR5526's later paid-repair extension also remain outside +coverage. A reviewed universal algebraic implication is useful evidence, not +scientific approval of every downstream claim. diff --git a/research/clifford-pointwise-audit/MATRIX-RESULT.json b/research/clifford-pointwise-audit/MATRIX-RESULT.json new file mode 100644 index 0000000000..ff42c130dc --- /dev/null +++ b/research/clifford-pointwise-audit/MATRIX-RESULT.json @@ -0,0 +1,186 @@ +{ + "groups": [ + { + "absolute_gram_row_sum": "13/32", + "axes": 1, + "exact_matrices": 96, + "generator_edges": 192, + "normalized_trace_squared_histogram": { + "0": 9, + "1": 1, + "1/2": 6, + "1/4": 8 + }, + "phase_fiber_size": 4, + "projective_classes": 24, + "width": 8 + }, + { + "absolute_gram_row_sum": "37739/65536", + "axes": 2, + "exact_matrices": 46080, + "generator_edges": 276480, + "normalized_trace_squared_histogram": { + "0": 3825, + "1": 1, + "1/16": 4864, + "1/2": 30, + "1/4": 400, + "1/8": 2400 + }, + "phase_fiber_size": 4, + "projective_classes": 11520, + "width": 12 + } + ], + "phase_and_gram": { + "nonunitary_scale_counterexample_coefficients": [ + 274877906944, + -2013265920, + 4587520, + -3840, + 1 + ], + "nonunitary_scale_values_at_widths_8_to_12": [ + 0, + 0, + 0, + 0, + 86586540687360 + ], + "omitted_residue_controls": [ + { + "omitted_residue": 0, + "widths_8_to_11": [ + [ + "4", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ] + }, + { + "omitted_residue": 1, + "widths_8_to_11": [ + [ + "0", + "0" + ], + [ + "4", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ] + }, + { + "omitted_residue": 2, + "widths_8_to_11": [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "4", + "0" + ], + [ + "0", + "0" + ] + ] + }, + { + "omitted_residue": 3, + "widths_8_to_11": [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "4", + "0" + ] + ] + } + ], + "one_axis_gram_ranks": { + "1": 4, + "10": 24, + "11": 24, + "2": 10, + "3": 20, + "4": 23, + "5": 24, + "6": 24, + "7": 24, + "8": 24, + "9": 24 + }, + "other_controls": [ + "small_width", + "H_prime_square_phase", + "duplicate_phase_classes", + "omitted_H_generator", + "exterior_scalar_placement", + "width_dependent_coefficients", + "arbitrary_nonunitary_scales" + ] + }, + "schema": "clifford-pointwise-independent-matrix-audit/v1", + "scope": "Finite exact corroboration only; universal claims require AUDIT.md", + "sources": [ + { + "git_blob": "465009d9d1b6947e80e6f1e868022f47ddab1f3c", + "path": "source/PR5526-PROOF.md", + "sha256": "45483e4b5f604a5e70602c5caaa4394d4a0d0d1a6d0b6e8a93b836d50b23f764" + }, + { + "git_blob": "a250d034c5e7b9ac98e9049e039754b6b0c38158", + "path": "source/PR5526-README.md", + "sha256": "b929248f5ad414ac776a2fa9cdc52ab745305aa257946e9b3596684ba1d74721" + } + ], + "spectral_check": { + "axes": 1, + "positive_pivots": 192, + "strict_lower": "1/9", + "strict_upper": "17/9", + "widths": [ + 8, + 9, + 10, + 11 + ] + } +} diff --git a/research/clifford-pointwise-audit/README.md b/research/clifford-pointwise-audit/README.md new file mode 100644 index 0000000000..84465d3ef3 --- /dev/null +++ b/research/clifford-pointwise-audit/README.md @@ -0,0 +1,140 @@ +# Independent audit of the pointwise Clifford tensor theorem + +**Independent AI-assisted proof audit; no substantive gap found in the stated core theorem.** +This package audits Sections 2–5 of Ali Romman's +[PR5526](https://github.com/CrocSwap/integer-mult-bounds/pull/5526) at +`45f7de73b168721cdf7ec8c1769b1b594493716a`: stabilizer and Clifford overlap counts, +uniform rational Gram bounds, and the four-residue fixed-program implication. +The theorem and constants remain the predecessor's work. No new kappa, +selected-frontier change, independent human review or formal verification is claimed. + +The added value is a written independent review, a separate exhaustive binary-matrix +check, and literal exact matrix/phase evidence with failure controls. The +[audit](AUDIT.md) makes the Gaussian-dyadic lift step explicit and distinguishes +fixed exterior coefficients from width-dependent coefficients and arbitrary +nonunitary scales. The source already provides projective Choi and signed-Pauli +censuses; independently regenerating similar finite counts is corroboration, +not a new theorem. Our source proof and README copies are immutable, attributed +review inputs. No predecessor executable is imported. + +## Evidence and reproduction + +Python 3.12 and its standard library suffice. From the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/clifford-pointwise-audit +``` + +The six registered commands run serially, each with a 120-second limit. The +literal matrix and independent symplectic checkers run both normally and under +`-O`; two mutation drivers each test both modes. On the recorded Linux/Python +3.12.14 host this is a small, single-CPU replay, with no large tensor matrices. +Actual commands, timings and results are recorded in [VALIDATION.json](VALIDATION.json). +Direct standalone commands also work from a Git-free package export: + +```sh +python3.12 -I -W error -B research/clifford-pointwise-audit/verify.py +python3.12 -I -O -W error -B research/clifford-pointwise-audit/verify.py +python3.12 -I -W error -B research/clifford-pointwise-audit/verify_symplectic.py +python3.12 -I -O -W error -B research/clifford-pointwise-audit/verify_symplectic.py +python3.12 -I -W error -B research/clifford-pointwise-audit/audit_mutations.py +python3.12 -I -W error -B research/clifford-pointwise-audit/audit_matrix_mutations.py +``` + +The checks cover: + +* All **96 + 46,080 exact Gaussian-dyadic Clifford matrices** on one/two axes, + retaining central phases during generation and finding four phase lifts per + projective class. Literal normalized trace distributions agree with the + separate fixed-space character computation. The classical generator/order + theorem is an explicit shared assumption; finite closure alone is not a proof + of completeness for an unspecified group. +* All **16 + 65,536 binary matrices**, directly selecting 6 + 720 symplectic + preservers. Their fixed spaces, actual character sums, residual-form preimages, + nondegeneracy, symmetrization and injection are checked. This enumeration + does not use Clifford gate generation or predecessor code. +* Exact Gaussian-rational ranks of the one-axis Gram matrix at widths 1–11, + including the rank-23 width-four failure and rank-24 width-five positive + fixture. The earlier PR5376 already establishes the sharp one-axis result; + these are controls, not a claimed cutoff improvement. Both spectral bounds + are checked by 192 positive rational Schur pivots at widths 8–11. The finite + row budgets and complete infinite-tail majorants are checked separately. +* Four omitted-residue counterexamples; phase-copy singularity; the H-prime + central phase; an omitted generator; exterior versus tensor scalar placement; + changing coefficients; and a nonunitary-scale residual that passes four + consecutive widths but fails the next. These expose the theorem's boundaries. +* Six actual defects in the independent checker, two false mathematical + expectations and an erased tensor width in the matrix checker, plus source + and receipt corruption: **22 rejecting subprocess runs** across + normal/optimized modes. Expected diagnostics are required, not just nonzero exits. + +`verify.py --emit` prints a fresh complete matrix receipt for comparison. Ordinary +replay compares [MATRIX-RESULT.json](MATRIX-RESULT.json) without writing it. +Mutation drivers write only to temporary directories. Source replay hashes bind +both retained documents, and their bytes were compared with Git blobs at the +exact fetched source head. [SOURCE-RECEIPT.json](SOURCE-RECEIPT.json) records those +pins. No pending-source Git objects or network are needed for standalone replay; +[SOURCES.json](SOURCES.json) uses only the canonical base for package provenance. + +## Scope, coordination and review + +The base is canonical `32890bc5de034ab8fc93ac88ead7279a6a416d04`, priority revision 7. +The task picker retrieved `formal-interface-lemma` after the live handoff-first +check. [TASK.json](TASK.json) records the changed scope: an informal independent +core-proof audit, before any formalization campaign. It answers part of +[this handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19174354) +in [Discussion5236](https://github.com/CrocSwap/integer-mult-bounds/discussions/5236). +The direct API claim attempt was rejected with `FORBIDDEN: Resource not accessible +by integration`; copyable claim text was supplied to the donor. No retrospective +public reservation is asserted. + +Initial overlap covered 403 open PRs, 4,682 closed/merged PRs, 4,828 Discussion +records and all 7,402 local indexed notes. Snapshots are non-atomic and exclude +arbitrary diffs, nested source histories and unpublished work. PR5531 explicitly +uses the general bound as a premise; PR5521 audits the smaller monomial class. +The merged DLamdata PR2880 audits an unrelated encoded-bank theorem and is +unchanged. Neither an empty search nor a merged archive is scientific acceptance. + +An independently deriving verifier and a skeptical reviewer found no substantive +defect. Their arguments and coverage are consolidated in AUDIT.md; the review +resolutions are in [REVIEW.md](REVIEW.md). Both are native AI agents. Shared +assumptions include classical stabilizer/Clifford structure, character +orthogonality, exact integer/rational arithmetic and the reviewed statement. +The lead's literal matrix orbit shares the general gate-generation idea with +one predecessor check; the exhaustive binary-matrix method is complementary. +Agreement alone is not the evidence. + +The **later 104-return repair theorem, invoice, actual passive-caller binding, +native frontend implementation, physical costs and full multiplication theorem +remain unaudited here**. The source's complete registered suite was not run, +because it covers those additional claims and dependencies. The selected +PR5413 cold replay was also not run; the selected record is unchanged, and its +source-binding orientation is not scientific admission. This is a narrow audit, +not a general endorsement of PR5526 or any downstream application. + +## Open next questions + +The remaining portion of the original handoff is an independent source-bound +review of the actual passive-caller implication. Start with the latest pinned +application and inventory every allowed observation/operator, including ownership +and excluded internal prefixes. The blocker is that complete caller binding, +not another small-group census. Separately, the later paid-repair theorem needs +its own quotient/capacity/original-input audit and invoice binding. Check live +claims before taking either task. Structured first steps and blockers are in +TASK.json. This result does not justify another construction search within an +unchanged mechanism. + +## Credit and license + +Ali Romman supplies PR5526 and the retained PR5376 tensor-Gram/native lineage. +The classical ingredients include Dehaene–De Moor's stabilizer normal forms, +symplectic residual/Wall forms, character orthogonality, Fourier inversion and +Gram diagonal dominance. The source preserves related contributions by Chris R / +Clear1nsight, Krzysztof Wojt, Nick Petalas and the native/paid-history authors; +none of their applications or general methods is claimed as new here. The full +source attribution remains in the immutable copied README and proof. + +Prepared for DLamdata with substantial OpenAI Codex assistance, including two +scoped native subagents. New work is Apache-2.0 under the repository license; +source notices are retained. This package changes no frozen predecessor, +shared verifier, project guidance or selected result. diff --git a/research/clifford-pointwise-audit/REVIEW.md b/research/clifford-pointwise-audit/REVIEW.md new file mode 100644 index 0000000000..78fa914308 --- /dev/null +++ b/research/clifford-pointwise-audit/REVIEW.md @@ -0,0 +1,71 @@ +# Internal review and resolution + +Prepared for DLamdata with substantial OpenAI Codex assistance. Apache-2.0. +These are native AI reviews, not independent human or formal-kernel review. + +## Independent derivation + +The verifier agent read the pinned theorem and independently derived the fixed +Pauli-character, transvection, residual-form, rational-tail and Fourier steps +before comparing with the lead's executable evidence. It did not read or import +predecessor scientific code. Its exhaustive binary-matrix implementation is +retained as `verify_symplectic.py`. Normal/optimized receipts were identical; +six actual defects were rejected in both modes. The lead inspected its code and +compared its complete nonzero-trace histogram with the independently generated +literal-matrix histogram. The independent derivation found no substantive gap. + +## Skeptical proof review + +A second agent read the frozen proof and developed its analysis before reading +the source README/bounds implementation or any lead result. It independently +checked all four rational tail bounds and all central-phase filters. No +substantive defect was found. Its useful clarifications were incorporated: + +| Concern | Resolution | +|---|---| +| Ordinary Hadamard is outside Z[i,1/2]; does the full projective lift exist? | AUDIT section1 gives Gaussian-dyadic H' and a direct transvection lift. Literal generation retains (H')^2=iI. | +| Fixed Paulis can anticommute. Are their signs a character? | AUDIT section3 cancels the identical Pauli multiplication phase explicitly; isotropy of the fixed space is not assumed. | +| Does counting residual forms assume an unjustified converse? | AUDIT section4 uses only an injection and counts singular forms in an upper bound. The independent checker tests actual preimages and injectivity. | +| Four tests can be misread as covering changing coefficients or arbitrary scales. | AUDIT section6 and executable counterexamples retain both exclusions. | +| Finite agreement may be mistaken for an all-size proof. | AUDIT separates universal reasoning/classical inputs from every finite check; README states their precise domains. | +| Source includes later repair/application claims. | Core scope is explicit throughout; no passive-caller, paid-repair, invoice or selected construction is endorsed. | + +## Shared assumptions and implementation overlap + +Both agents necessarily read the same mathematical statement. Classical +Clifford generation/order, stabilizer normal forms, symplectic structure, +character orthogonality and exact arithmetic are shared assumptions. The lead's +Gaussian-matrix orbit is related to the predecessor's projective Choi orbit; +it is not represented as a wholly unrelated algorithm. Its explicit central +extension and phase-boundary controls complement the separate exhaustive +binary-matrix/residual-form path. No predecessor executable is imported. + +All tested assertions use explicit exceptions and remain active under `-O`. +Source/receipt corruption controls require specific failure diagnostics. +Mutation jobs are serial and operate only on temporary copies. A copied +read-only package is made writable only inside that temporary test directory. +The original package and its source inputs remain unchanged during replay. + +## Review scope still open + +The original handoff also requests an actual passive-contract audit. That part, +PR5526's later 104-return repair theorem and invoice, PR5531's application, +native frontend correctness, physical costs, selected cold replay and the full +multiplication theorem remain outside this contribution. External Claude +review was not required or obtained. + +## Final package review + +Both agents subsequently reviewed the frozen 15-file contribution. The independent +reviewer confirmed the unchanged independent checker and both complete trace +histograms, and tested Hermitian positive/singular/indefinite fixtures. The skeptical +reviewer authenticated both retained documents against exact-head Git blobs and +independently checked literal H-prime, S and CNOT fixtures. Neither reran the lead's +suite. No blocking defect was found. + +One wording ambiguity was resolved: two matrix mutation controls change a required +mathematical expectation (the first-overlap count and H-prime square), rather than +mutating the gate implementation. They are now named +`wrong-first-overlap-expectation` and `wrong-H-square-expectation`; the erased-width +control really does change Gram construction. The affected driver was rerun. +This clarification changes neither mathematical evidence nor source pins. diff --git a/research/clifford-pointwise-audit/SOURCE-RECEIPT.json b/research/clifford-pointwise-audit/SOURCE-RECEIPT.json new file mode 100644 index 0000000000..89a3f2405a --- /dev/null +++ b/research/clifford-pointwise-audit/SOURCE-RECEIPT.json @@ -0,0 +1,26 @@ +{ + "repository": "aliromman/integer-mult-bounds", + "source_pr": 5526, + "source_head": "45f7de73b168721cdf7ec8c1769b1b594493716a", + "retrieval": "GitHub contents API at exact commit, followed by git fetch upstream pull/5526/head and byte-exact git cat-file comparisons for both retained source documents. Offline replay checks both Git blob and SHA256; no pending-source Git object is needed.", + "files": [ + { + "file": "PROOF.md", + "path": "research/clifford-pointwise-faithfulness/PROOF.md", + "head": "45f7de73b168721cdf7ec8c1769b1b594493716a", + "git_blob": "465009d9d1b6947e80e6f1e868022f47ddab1f3c", + "sha256": "45483e4b5f604a5e70602c5caaa4394d4a0d0d1a6d0b6e8a93b836d50b23f764", + "bytes": 15173, + "local_path": "source/PR5526-PROOF.md" + }, + { + "file": "README.md", + "path": "research/clifford-pointwise-faithfulness/README.md", + "head": "45f7de73b168721cdf7ec8c1769b1b594493716a", + "git_blob": "a250d034c5e7b9ac98e9049e039754b6b0c38158", + "sha256": "b929248f5ad414ac776a2fa9cdc52ab745305aa257946e9b3596684ba1d74721", + "bytes": 12468, + "local_path": "source/PR5526-README.md" + } + ] +} diff --git a/research/clifford-pointwise-audit/SOURCES.json b/research/clifford-pointwise-audit/SOURCES.json new file mode 100644 index 0000000000..300446bf5b --- /dev/null +++ b/research/clifford-pointwise-audit/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + } + ] +} diff --git a/research/clifford-pointwise-audit/TASK.json b/research/clifford-pointwise-audit/TASK.json new file mode 100644 index 0000000000..10139d84ff --- /dev/null +++ b/research/clifford-pointwise-audit/TASK.json @@ -0,0 +1,124 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Independent proof audit of PR5526 Sections 2\u20135: projective Clifford/stabilizer overlap counts, universal rational Gram bounds, and fixed-program four-phase implication.", + "scope_change_reason": "Handoff-first override: Discussion1166 comment19174354 explicitly requests an independent proof audit of PR5526. This is an informal mathematical audit before formalization, not the historical formal-interface card's already-covered arithmetic or a Lean theorem.", + "bottleneck_link": "An algebraic tensor-separation acceptance gap is already consumed by PR5531 and passive-history proposals. Independently checking this implication supports scoped interface review; no physical caller or selected assumption is discharged.", + "budget_minutes": 60, + "stop_rule": "Stop after one bounded core-proof audit and exact corroboration, or report a precise gap/counterexample. No larger-family or sharp-threshold search.", + "outcome": "completed", + "evidence": "AUDIT.md; exact literal matrices, exhaustive binary symplectic census, rational tails, phase/domain controls; see VERIFY.json and VALIDATION.json.", + "author": "DLamdata, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex lead assistance, one independently deriving native verifier subagent and one skeptical native review subagent. Not independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Does the complete frozen PR5526 passive-caller observation alphabet meet the core theorem's hypotheses?", + "why_it_matters": "This audit resolves only the core algebraic implication; its source-bound passive application is a separate portion of the handoff.", + "first_step": "Pin the latest application and source heads, then independently bind every permitted observation/operator and all excluded internal prefixes to the stated columnwise Clifford contract.", + "blocked_by": "Requires a separate source/caller audit; no conclusion follows from the small-group census." + }, + { + "question": "Does the later 104-return repair theorem retain its quotient, capacity and original-input premises at the actual caller?", + "why_it_matters": "The later repair and invoice claims are explicitly outside this core proof audit.", + "first_step": "Check live overlap and independently review REPAIR.md at a pinned head, starting with its initial observation module and arbitrary-new-return step.", + "blocked_by": "Additional source-bound algebra/cost review; this package does not supply it." + } + ], + "overlap": { + "initial_base": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "task_picker_seed": "c99288522c14b979d3a20ee526fcea65", + "canonical_thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5236", + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19174354", + "discussion_status": "Direct API claim attempt rejected FORBIDDEN: Resource not accessible by integration; copyable claim supplied to donor. No public reservation is claimed.", + "nearest_predecessors": [ + 5526, + 5531, + 5521, + 5376, + 2880 + ], + "initial_coverage": { + "open_prs": 403, + "closed_prs": 4682, + "discussion_records": 4828, + "local_records": 7402, + "complete_pagination": true, + "complete_local_note_inventory": true + }, + "limits": "Titles/bodies, Discussion comments/replies, top-level local README/TASK and ledger; no arbitrary diffs, nested source histories or unpublished work. Snapshots non-atomic." + } +} diff --git a/research/clifford-pointwise-audit/VALIDATION.json b/research/clifford-pointwise-audit/VALIDATION.json new file mode 100644 index 0000000000..64d87d27d2 --- /dev/null +++ b/research/clifford-pointwise-audit/VALIDATION.json @@ -0,0 +1,121 @@ +{ + "environment": { + "python": "3.12.14 (main, Aug 25 2026, 14:00:49) [Clang 22.1.3 ]", + "platform": "Linux-6.18.55-x86_64-with-glibc2.41", + "dependencies": "standard library", + "max_child_rss_kib": 34848 + }, + "source_base": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "source_head": "45f7de73b168721cdf7ec8c1769b1b594493716a", + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "exit_code": 0, + "elapsed_seconds": 2.792, + "stdout": "PASS_CLIFFORD_POINTWISE_MATRIX_AUDIT: 46176 exact matrices; complete receipt matched\n", + "stderr": "" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "exit_code": 0, + "elapsed_seconds": 2.844, + "stdout": "PASS_CLIFFORD_POINTWISE_MATRIX_AUDIT: 46176 exact matrices; complete receipt matched\n", + "stderr": "" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify_symplectic.py" + ], + "exit_code": 0, + "elapsed_seconds": 0.241, + "stdout": "{\n \"bounds_and_phases\": {\n \"clifford_row_sum_majorants\": {\n \"s0\": \"53534/60543\",\n \"s2\": \"359294/2451015\",\n \"s6\": \"162912909217/20637399121920\"\n },\n \"finite_subspace_terms\": 528,\n \"four_residue_witness_values\": [\n [\n [\n 4,\n 0\n ],\n [\n 0,\n 0\n ],\n [\n 0,\n 0\n ],\n [\n 0,\n 0\n ]\n ],\n [\n [\n 0,\n 0\n ],\n [\n 4,\n 0\n ],\n [\n 0,\n 0\n ],\n [\n 0,\n 0\n ]\n ],\n [\n [\n 0,\n 0\n ],\n [\n 0,\n 0\n ],\n [\n 4,\n 0\n ],\n [\n 0,\n 0\n ]\n ],\n [\n [\n 0,\n 0\n ],\n [\n 0,\n 0\n ],\n [\n 0,\n 0\n ],\n [\n 4,\n 0\n ]\n ]\n ],\n \"stabilizer_row_sum_majorant\": \"719543/1220625\"\n },\n \"censuses\": [\n {\n \"axes\": 1,\n \"binary_matrices_tested\": 16,\n \"character_sums\": 24,\n \"displacement_rank_histogram\": {\n \"0\": 1,\n \"1\": 3,\n \"2\": 2\n },\n \"distinct_residual_forms\": 6,\n \"nonzero_trace_lift_histogram\": {\n \"0\": 1,\n \"1\": 6,\n \"2\": 8\n },\n \"residual_symmetrization_pairs\": 45,\n \"symplectic_matrices\": 6\n },\n {\n \"axes\": 2,\n \"binary_matrices_tested\": 65536,\n \"character_sums\": 11520,\n \"displacement_rank_histogram\": {\n \"0\": 1,\n \"1\": 15,\n \"2\": 100,\n \"3\": 300,\n \"4\": 304\n },\n \"distinct_residual_forms\": 720,\n \"nonzero_trace_lift_histogram\": {\n \"0\": 1,\n \"1\": 30,\n \"2\": 400,\n \"3\": 2400,\n \"4\": 4864\n },\n \"residual_symmetrization_pairs\": 98685,\n \"symplectic_matrices\": 720\n }\n ],\n \"controls\": [\n \"identity-positive\",\n \"invertible-nonsymplectic\",\n \"singular\",\n \"pairing-coordinates\",\n \"phase-deletion\",\n \"first-overlap-half\"\n ],\n \"scope\": \"PR5526 Sections 3--5 independent direct binary-matrix audit\"\n}\nPASS_INDEPENDENT_SYMPLECTIC_OVERLAP_AUDIT\n", + "stderr": "" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify_symplectic.py" + ], + "exit_code": 0, + "elapsed_seconds": 0.293, + "stdout": "{\n \"bounds_and_phases\": {\n \"clifford_row_sum_majorants\": {\n \"s0\": \"53534/60543\",\n \"s2\": \"359294/2451015\",\n \"s6\": \"162912909217/20637399121920\"\n },\n \"finite_subspace_terms\": 528,\n \"four_residue_witness_values\": [\n [\n [\n 4,\n 0\n ],\n [\n 0,\n 0\n ],\n [\n 0,\n 0\n ],\n [\n 0,\n 0\n ]\n ],\n [\n [\n 0,\n 0\n ],\n [\n 4,\n 0\n ],\n [\n 0,\n 0\n ],\n [\n 0,\n 0\n ]\n ],\n [\n [\n 0,\n 0\n ],\n [\n 0,\n 0\n ],\n [\n 4,\n 0\n ],\n [\n 0,\n 0\n ]\n ],\n [\n [\n 0,\n 0\n ],\n [\n 0,\n 0\n ],\n [\n 0,\n 0\n ],\n [\n 4,\n 0\n ]\n ]\n ],\n \"stabilizer_row_sum_majorant\": \"719543/1220625\"\n },\n \"censuses\": [\n {\n \"axes\": 1,\n \"binary_matrices_tested\": 16,\n \"character_sums\": 24,\n \"displacement_rank_histogram\": {\n \"0\": 1,\n \"1\": 3,\n \"2\": 2\n },\n \"distinct_residual_forms\": 6,\n \"nonzero_trace_lift_histogram\": {\n \"0\": 1,\n \"1\": 6,\n \"2\": 8\n },\n \"residual_symmetrization_pairs\": 45,\n \"symplectic_matrices\": 6\n },\n {\n \"axes\": 2,\n \"binary_matrices_tested\": 65536,\n \"character_sums\": 11520,\n \"displacement_rank_histogram\": {\n \"0\": 1,\n \"1\": 15,\n \"2\": 100,\n \"3\": 300,\n \"4\": 304\n },\n \"distinct_residual_forms\": 720,\n \"nonzero_trace_lift_histogram\": {\n \"0\": 1,\n \"1\": 30,\n \"2\": 400,\n \"3\": 2400,\n \"4\": 4864\n },\n \"residual_symmetrization_pairs\": 98685,\n \"symplectic_matrices\": 720\n }\n ],\n \"controls\": [\n \"identity-positive\",\n \"invertible-nonsymplectic\",\n \"singular\",\n \"pairing-coordinates\",\n \"phase-deletion\",\n \"first-overlap-half\"\n ],\n \"scope\": \"PR5526 Sections 3--5 independent direct binary-matrix audit\"\n}\nPASS_INDEPENDENT_SYMPLECTIC_OVERLAP_AUDIT\n", + "stderr": "" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/audit_mutations.py" + ], + "exit_code": 0, + "elapsed_seconds": 1.468, + "stdout": "[\n {\n \"mutation\": \"accept-all-matrices\",\n \"optimized\": false,\n \"exit\": 1,\n \"diagnostic\": \"noninvertible-preserver\"\n },\n {\n \"mutation\": \"accept-all-matrices\",\n \"optimized\": true,\n \"exit\": 1,\n \"diagnostic\": \"noninvertible-preserver\"\n },\n {\n \"mutation\": \"drop-displacement-identity\",\n \"optimized\": false,\n \"exit\": 1,\n \"diagnostic\": \"fixed-rank-disagreement\"\n },\n {\n \"mutation\": \"drop-displacement-identity\",\n \"optimized\": true,\n \"exit\": 1,\n \"diagnostic\": \"fixed-rank-disagreement\"\n },\n {\n \"mutation\": \"count-zero-trace-lifts\",\n \"optimized\": false,\n \"exit\": 1,\n \"diagnostic\": \"wrong-nonzero-lift-count\"\n },\n {\n \"mutation\": \"count-zero-trace-lifts\",\n \"optimized\": true,\n \"exit\": 1,\n \"diagnostic\": \"wrong-nonzero-lift-count\"\n },\n {\n \"mutation\": \"use-image-for-preimage\",\n \"optimized\": false,\n \"exit\": 1,\n \"diagnostic\": \"residual-left-degenerate\"\n },\n {\n \"mutation\": \"use-image-for-preimage\",\n \"optimized\": true,\n \"exit\": 1,\n \"diagnostic\": \"residual-left-degenerate\"\n },\n {\n \"mutation\": \"drop-first-overlap-half\",\n \"optimized\": false,\n \"exit\": 1,\n \"diagnostic\": \"clifford-uniform-tail\"\n },\n {\n \"mutation\": \"drop-first-overlap-half\",\n \"optimized\": true,\n \"exit\": 1,\n \"diagnostic\": \"clifford-uniform-tail\"\n },\n {\n \"mutation\": \"erase-central-phase\",\n \"optimized\": false,\n \"exit\": 1,\n \"diagnostic\": \"phase-fourier-orthogonality\"\n },\n {\n \"mutation\": \"erase-central-phase\",\n \"optimized\": true,\n \"exit\": 1,\n \"diagnostic\": \"phase-fourier-orthogonality\"\n }\n]\nPASS_INDEPENDENT_SYMPLECTIC_MUTATIONS\n", + "stderr": "" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/audit_matrix_mutations.py" + ], + "exit_code": 0, + "elapsed_seconds": 16.106, + "stdout": "[\n {\n \"mutation\": \"wrong-first-overlap-expectation\",\n \"optimized\": false,\n \"exit\": 1,\n \"diagnostic\": \"First Clifford overlap count\"\n },\n {\n \"mutation\": \"wrong-first-overlap-expectation\",\n \"optimized\": true,\n \"exit\": 1,\n \"diagnostic\": \"First Clifford overlap count\"\n },\n {\n \"mutation\": \"tensor-width-erased\",\n \"optimized\": false,\n \"exit\": 1,\n \"diagnostic\": \"Four-width positive fixture\"\n },\n {\n \"mutation\": \"tensor-width-erased\",\n \"optimized\": true,\n \"exit\": 1,\n \"diagnostic\": \"Four-width positive fixture\"\n },\n {\n \"mutation\": \"wrong-H-square-expectation\",\n \"optimized\": false,\n \"exit\": 1,\n \"diagnostic\": \"H-prime square retains i\"\n },\n {\n \"mutation\": \"wrong-H-square-expectation\",\n \"optimized\": true,\n \"exit\": 1,\n \"diagnostic\": \"H-prime square retains i\"\n },\n {\n \"mutation\": \"source-corrupted\",\n \"optimized\": false,\n \"exit\": 1,\n \"diagnostic\": \"Frozen source byte mismatch\"\n },\n {\n \"mutation\": \"source-corrupted\",\n \"optimized\": true,\n \"exit\": 1,\n \"diagnostic\": \"Frozen source byte mismatch\"\n },\n {\n \"mutation\": \"receipt-corrupted\",\n \"optimized\": false,\n \"exit\": 1,\n \"diagnostic\": \"Matrix receipt mismatch\"\n },\n {\n \"mutation\": \"receipt-corrupted\",\n \"optimized\": true,\n \"exit\": 1,\n \"diagnostic\": \"Matrix receipt mismatch\"\n }\n]\nPASS_CLIFFORD_MATRIX_MUTATIONS\n", + "stderr": "" + } + ], + "scope": "Executed command bodies serially from intended worktree; registered launcher and committed-byte portability recorded separately.", + "registered_replay": { + "argv": [ + "python3.12", + "-B", + "scripts/research_package.py", + "--package", + "research/clifford-pointwise-audit" + ], + "exit_code": 0, + "result": "PASS_REGISTERED_RESEARCH_PACKAGE research/clifford-pointwise-audit outcome=completed", + "note": "All six commands passed. Subsequent changes only clarify mutation labels/prose; the affected matrix-mutation driver was rerun and its row above updated." + }, + "execution_sources_sha256": { + "MATRIX-RESULT.json": "8cbc73e8f2022af3ddf2b479368aba1504d92094323d96d631fe98f3a830ee20", + "SOURCE-RECEIPT.json": "abf729a82315f679076386e213cc8940adaca229734bdd2eaa882e55572ca8a9", + "audit_matrix_mutations.py": "83044bd6ba57a7b5f8b86e01b1c8c10c7bb2f8ddc93817725c1e1d1f190399c2", + "audit_mutations.py": "54a0505090a42d76ad5fb799d03bf0a73add7f3973f84c46bd573d0c5f32fd01", + "source/PR5526-PROOF.md": "45483e4b5f604a5e70602c5caaa4394d4a0d0d1a6d0b6e8a93b836d50b23f764", + "source/PR5526-README.md": "b929248f5ad414ac776a2fa9cdc52ab745305aa257946e9b3596684ba1d74721", + "verify.py": "f162125433c292efb6495af70fd8a07117fca8b00ff915ebfca9ce8a351c043d", + "verify_symplectic.py": "ee23ab8fe38c3e33136be334042cb63ca79d4ae1c70ec1cf79400cce8091e1d9" + } +} diff --git a/research/clifford-pointwise-audit/VERIFY.json b/research/clifford-pointwise-audit/VERIFY.json new file mode 100644 index 0000000000..72f22f7b9b --- /dev/null +++ b/research/clifford-pointwise-audit/VERIFY.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Literal Gaussian matrices with phases, exact Gram ranks and bounds, quantified-domain controls, source/receipt equality" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Literal Gaussian matrices with phases, exact Gram ranks and bounds, quantified-domain controls, source/receipt equality (optimized)" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify_symplectic.py" + ], + "timeout_seconds": 120, + "checks": "Independent exhaustive binary symplectic matrices, actual fixed-space characters and residual forms, exact tails and phase controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify_symplectic.py" + ], + "timeout_seconds": 120, + "checks": "Independent exhaustive binary symplectic matrices, actual fixed-space characters and residual forms, exact tails and phase controls (optimized)" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/audit_mutations.py" + ], + "timeout_seconds": 120, + "checks": "Six deliberate independent-checker defects rejected in normal and optimized Python" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/audit_matrix_mutations.py" + ], + "timeout_seconds": 120, + "checks": "Source/receipt corruption and three actual matrix-checker defects rejected in normal and optimized Python" + } + ] +} diff --git a/research/clifford-pointwise-audit/audit_matrix_mutations.py b/research/clifford-pointwise-audit/audit_matrix_mutations.py new file mode 100644 index 0000000000..1debe4e02f --- /dev/null +++ b/research/clifford-pointwise-audit/audit_matrix_mutations.py @@ -0,0 +1,56 @@ +"""Reject corruption and actual defects in the literal matrix audit. + +Prepared for DLamdata with substantial OpenAI Codex assistance. Apache-2.0. +""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +source = (HERE/'verify.py').read_text() +mutations = [ + ('wrong-first-overlap-expectation', 'hist[F(1, 2)] == 2*((1 << (2*n))-1)', + 'hist[F(1, 2)] == ((1 << (2*n))-1)', 'First Clifford overlap count'), + ('tensor-width-erased', 'width) for b in matrices]', + '1) for b in matrices]', 'Four-width positive fixture'), + ('wrong-H-square-expectation', "== rotate(identity(1)), 'H-prime square retains i'", + "== identity(1), 'H-prime square retains i'", 'H-prime square retains i'), +] +results = [] +with tempfile.TemporaryDirectory(prefix='clifford-matrix-controls-') as tmp: + root = Path(tmp) + for name, old, new, diagnostic in mutations + [ + ('source-corrupted', None, None, 'Frozen source byte mismatch'), + ('receipt-corrupted', None, None, 'Matrix receipt mismatch'), + ]: + target = root/name + shutil.copytree(HERE, target, ignore=shutil.ignore_patterns('__pycache__')) + # A read-only source export is valid input; only the temporary copy is edited. + target.chmod(0o700) + for path in target.rglob('*'): + path.chmod(0o700 if path.is_dir() else 0o600) + if old is not None: + if source.count(old) != 1: + raise RuntimeError('Mutation site not unique: '+name) + (target/'verify.py').write_text(source.replace(old, new)) + elif name == 'source-corrupted': + with (target/'source/PR5526-PROOF.md').open('ab') as stream: + stream.write(b'\ncorruption control\n') + else: + path = target/'MATRIX-RESULT.json' + result = json.loads(path.read_text()) + result['groups'][1]['exact_matrices'] += 1 + path.write_text(json.dumps(result)) + for optimized in (False, True): + command = [sys.executable, '-I'] + (['-O'] if optimized else []) + command += ['-W', 'error', '-B', str(target/'verify.py')] + run = subprocess.run(command, capture_output=True, text=True, timeout=120) + if run.returncode == 0 or diagnostic not in run.stderr: + raise RuntimeError('Wrong rejection: '+name+' '+run.stderr) + results.append({'mutation':name,'optimized':optimized, + 'exit':run.returncode,'diagnostic':diagnostic}) +print(json.dumps(results,indent=2)) +print('PASS_CLIFFORD_MATRIX_MUTATIONS') diff --git a/research/clifford-pointwise-audit/audit_mutations.py b/research/clifford-pointwise-audit/audit_mutations.py new file mode 100644 index 0000000000..636dadcb3d --- /dev/null +++ b/research/clifford-pointwise-audit/audit_mutations.py @@ -0,0 +1,52 @@ +#!/usr/bin/env python3 +"""Reject six actual changes to the standalone independent checker. + +Prepared for DLamdata with substantial OpenAI Codex assistance. Apache-2.0. +""" +import json +from pathlib import Path +import subprocess +import sys +import tempfile + +source = Path(__file__).with_name('verify_symplectic.py').read_text() +mutations = [ + ('accept-all-matrices', + 'if not symplectic(columns, n):', 'if False:', 'noninvertible-preserver'), + ('drop-displacement-identity', + 'columns[j] ^ (1 << j) for j in range(m)', 'columns[j] for j in range(m)', + 'fixed-rank-disagreement'), + ('count-zero-trace-lifts', + 'positive = sum(s != 0 for s in sums)', 'positive = len(sums)', + 'wrong-nonzero-lift-count'), + ('use-image-for-preimage', + 'values = {omega(x, w, n) for x in preimages[u]}', + 'values = {omega(u, w, n) for x in preimages[u]}', + 'residual-left-degenerate'), + ('drop-first-overlap-half', + 'initial = Fraction(1, 1 << (s+1))', 'initial = Fraction(1, 1 << s)', + 'clifford-uniform-tail'), + ('erase-central-phase', + 'roots = ((1, 0), (0, 1), (-1, 0), (0, -1))', + 'roots = ((1, 0), (1, 0), (1, 0), (1, 0))', + 'phase-fourier-orthogonality'), +] +out = [] +with tempfile.TemporaryDirectory(prefix='independent-clifford-mutations-') as tmp: + target = Path(tmp)/'verify.py' + for name, old, new, diagnostic in mutations: + if old not in source: + raise RuntimeError('missing mutation site: '+name) + target.write_text(source.replace(old, new)) + for optimized in (False, True): + command = [sys.executable, '-I', '-W', 'error', '-B'] + if optimized: + command.append('-O') + command.append(str(target)) + run = subprocess.run(command, capture_output=True, text=True, timeout=120) + if run.returncode == 0 or diagnostic not in run.stderr: + raise RuntimeError('wrong mutation outcome: '+name+' '+run.stderr) + out.append({'mutation': name, 'optimized': optimized, + 'exit': run.returncode, 'diagnostic': diagnostic}) +print(json.dumps(out, indent=2)) +print('PASS_INDEPENDENT_SYMPLECTIC_MUTATIONS') diff --git a/research/clifford-pointwise-audit/source/PR5526-PROOF.md b/research/clifford-pointwise-audit/source/PR5526-PROOF.md new file mode 100644 index 0000000000..465009d9d1 --- /dev/null +++ b/research/clifford-pointwise-audit/source/PR5526-PROOF.md @@ -0,0 +1,305 @@ +# Pointwise tensor faithfulness for Clifford and stabilizer maps + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. + +This is an algebraic result. It supplies no physical implementation or new +kappa. The classical ingredients are stabilizer normal forms, symplectic +residual forms, character orthogonality and the Gram row bound. The new +contribution in this repository is their quantitative pointwise consequence. + +## 1. Statements + +Let C_n be the unitary n-qubit Clifford matrices with entries in Z[i,1/2]. +Its scalar subgroup is {I,iI,-I,-iI}. Choose one representative U_g for +each projective class. Indeed a unit Gaussian-dyadic scalar satisfies +a^2+b^2=4^k with integers a,b. Repeated parity reduction leaves only a +Gaussian unit. Set D=2^n. For n>=1 and every integer f>=4n+4, + + (1/9) sum_g |b_g|^2 + <= D^(-f) ||sum_g b_g U_g^(tensor f)||_HS^2 + <= (17/9) sum_g |b_g|^2. (1) + +The coefficients are arbitrary complex numbers at this one width. Thus all +the projective tensor operators are linearly independent at every such f. +Any subset has the same bounds. The choice of representative phase does not +change the bounds. The proof also applies to the usual Clifford group with +arbitrary unit scalar phases, after projective classes are combined. + +For a fixed residual in the exact dyadic group algebra, the following are +equivalent: + +1. Every exact-operator coefficient is zero. +2. The residual vanishes at every positive width. +3. It vanishes at the four widths 4n+4,...,4n+7. + +If M is the squared coefficient norm after equal exact operators are +combined, at least one of these four normalized squared norms is >= M/9. +Four tests are necessary for this exact group with arbitrary complex scalar +coefficients. This is a sufficient width bound, not a sharp width threshold. +For n=0 the group is the four scalar phases; widths 1,2,3,4 suffice. + +There is a broader result. A nonzero stabilizer map from a binary input +space to a binary output space is a matrix whose vectorization, up to a +nonzero scalar, is a pure stabilizer state. Let N be the total number of +input and output axes. Normalize these vectors to unit length and choose +one per projective class. At every f>=2N+6 their tensor Gram matrix has + + (2/5) I <= Gram_f <= (8/5) I. (2) + +This includes rectangular maps and Pauli projections. For arbitrary +unnormalized representatives A_g, (2) means + + ||sum_g b_g A_g^(tensor f)||_HS^2 + >= (2/5) sum_g |b_g|^2 ||A_g||_HS^(2f). (3) + +The statements at a single width allow different finite words, different +scalar coefficients and different subsets at each width. They do not infer +all-width equality of a changing family from four tests. Products must +still have the stated columnwise Clifford or stabilizer-map form. + +There is a robust consequence. If a unitary Clifford target T is absent +from a set of projective classes S, then for f>=4n+4, + + D^(-f) ||T^(tensor f)-sum_(g in S) b_g U_g^(tensor f)||_HS^2 + >= (1/9)(1+sum_g |b_g|^2) >= 1/9. (4) + +Its operator norm error is therefore at least 1/3. This is a worst-case +unit-input error bound, not a guarantee about the error on each input. +Later widths use the stronger constants in Section 4. In particular the +lower bound on normalized squared error tends to one as f increases. + +## 2. Count the stabilizer overlaps + +A projective N-qubit stabilizer state has a computational-basis support +which is an affine binary subspace. In coordinates t on its k-dimensional +support, its amplitudes have the form + + 2^(-k/2) i^(a.t + 2 sum_(j. A state has a nonzero overlap of modulus 2^(-k/2) +with it exactly when its support is a k-subspace containing zero. Normalize +its amplitude at zero to be positive. The remaining phase polynomial is +unique. There are + + A_(N,k) = [N choose k]_2 2^(k(k+3)/2) (5) + +such states, including A_(N,0)=1. Here + + [N choose k]_2 = product_(j=0..k-1) + (2^(N-j)-1)/(2^(k-j)-1). + +There are k coefficients with four choices and k(k-1)/2 coefficients with +two choices. This proves the exponent in (5). The other states have zero +overlap. Clifford conjugation is transitive on pure stabilizer states, so +the same distribution holds about every projective stabilizer state. + +Transitivity can also be seen directly: a basis change puts the support +on coordinate axes, a translation removes its offset, diagonal Clifford +phases remove its phase polynomial, and Hadamards send its uniform support +to zero. This argument does not use a counting formula for the Clifford +group. + +It follows that the absolute off-diagonal row sum of the f-fold tensor +Gram matrix of all these states is exactly + + S_(N,f) = sum_(k=1..N) A_(N,k) 2^(-kf/2). (6) + +An arbitrary subset has no larger row sum. This count concerns projective +states. Repeating scalar-phase copies would make a pointwise Gram singular. + +## 3. The Clifford first-overlap improvement + +Vectorize U/sqrt(D) to obtain its unit Choi state on 2n qubits. It is a +stabilizer state: the Bell state is a stabilizer state and Clifford action +on one half preserves that property. Projectively different matrices give +different projective Choi states. Formula (5), with N=2n, therefore bounds +their overlap counts. + +For k=1 the Clifford count is exactly + + B_(n,1) = 2(2^(2n)-1) = A_(2n,1)/2. (7) + +Here is a separate proof which retains the signs. Let S be the symplectic +Pauli action of U, and L=ker(S-I). In the Hermitian Pauli basis, conjugation +has trace |tr U|^2. Its contribution at a fixed label v is its sign epsilon(v). +On L these signs form a character: conjugation cancels the same Pauli +multiplication phase on both sides. Thus |tr U|^2 is either zero or +2^dim(L). + +For a fixed S, its projective Clifford lifts differ by the 2^(2n) Paulis. +They multiply the sign on L by every character of L, each with multiplicity +2^(2n-dim(L)). Therefore exactly 2^k lifts have nonzero trace when +rank(S-I)=k. Their normalized trace modulus is 2^(-k/2). + +A rank-one symplectic displacement is a transvection. Indeed, write +(S-I)x=ell(x)a for nonzero a. Symplecticity gives +ell(x) omega(a,y)+ell(y) omega(x,a)=0. Nondegeneracy then forces +ell(x)=omega(x,a) over F_2. Every nonzero a gives one such map. There are +2^(2n)-1 choices, and each has two nonzero-trace lifts. This proves (7). + +For clarity, a second count gives the same general upper bound without +Choi states. Put W=im(S-I), dim W=k. Then ker(S-I)=W-perp. The residual +form B((S-I)x,w)=omega(x,w) is well-defined, nonsingular and satisfies +B(u,v)+B(v,u)=omega(u,v). For fixed W there are at most +2^(k(k+1)/2) bilinear forms with this fixed symmetrization. Each nonsingular +one determines S uniquely: solve B((S-I)x,w)=omega(x,w) for every w in W. +There are [2n choose k]_2 possible W and 2^k nonzero-trace Pauli lifts. +Their product is exactly A_(2n,k). No equality is asserted for k>=2. + +The Choi and residual-form arguments are different derivations of the same +upper bound. The checks enumerate signed Pauli actions and literal Choi +vectors separately. + +## 4. Uniform rational row bounds + +Set d_k=product_(j=1..k)(2^j-1). The subspace count satisfies + + [N choose k]_2 <= 2^(k(N-k)) / + product_(j=1..k)(1-2^(-j)). + +At f=2N+4, its term in (6) is at most 1/d_k. The Clifford first term is +at most 1/2 by (7). Its whole off-diagonal row sum is consequently at most + + 1/2 + 1/3 + 1/21 + 1/315 + + (1/9765)/(1-1/63) < 8/9. (8) + +The tail starts at k=5. Each subsequent term has ratio at most 1/63. +The bound is independent of n. Terms with k>2n were added only to bound +the finite sum from above. At all larger widths the row sum can only fall. + +For all stabilizer states use f=2N+6. Each term is at most 2^(-k)/d_k, +so the full row sum is at most + + 1/2 + 1/12 + 1/168 + 1/5040 + + (1/312480)/(1-1/126) < 3/5. (9) + +Again this is a rational bound on the complete infinite tail. The executable +also provides the sharper finite sums for any specified axis count and any +even width. For an odd width it uses the preceding even width. A failed +sufficient bound is no decision, not evidence of linear dependence. + +If a Hermitian matrix has diagonal one and absolute off-diagonal row sums +at most s, then its eigenvalues lie in [1-s,1+s]. One direct proof bounds +each pair by 2|b_i b_j| <= |b_i|^2+|b_j|^2 in its quadratic form. +Apply this to the Gram matrices and (8)-(9). This proves (1)-(3). +Apply (1) to the residual with target coefficient one to obtain (4). +The inequality ||R||_HS <= sqrt(D^f)||R||_op gives its operator norm claim. + +There are useful stronger bounds at a slightly later width. At +f=4n+4+2s the Clifford row bound is at most + + 2^(-s-1) + sum_(k>=2) 2^(-sk)/d_k. (10) + +For s=2 this is <3/20. For s=6 it is <1/126. +Thus four consecutive widths starting at 4n+8 have a 17/20 lower bound; +four starting at 4n+16 have a 125/126 lower bound. The same geometric-tail +argument proves these constants. These are sufficient constants, not +optimal spectral values. + +## 5. Exact phases and the four-width theorem + +For the Gaussian-dyadic group write every exact matrix uniquely as i^j U_g, +where g is its projective class and j=0,1,2,3. For a fixed residual define + + beta_(g,r) = sum_(j=0..3) c_(g,j) i^(jr). + +At any f>=4n+4 with f=r modulo four, (1) says that the residual is zero +exactly when all beta_(g,r) vanish. This is the exact pointwise kernel: +only the unavoidable scalar-phase relations remain. Four consecutive +widths supply all four residues. Fourier inversion then makes every +c_(g,j) zero. + +Parseval gives (1/4) sum_(g,r)|beta_(g,r)|^2=M. Averaging (1) over the +four tested widths proves the M/9 claim. Formula (10) gives the two stronger +four-width constants stated above. Apply the argument to each entry of a +complete input-to-output register matrix; every dirty role must be retained. + +For each r the residual sum_(j=0..3) i^(-rj)[i^j I] vanishes at every width +outside r modulo four and is 4I in that residue. Thus three widths cannot +be a universal fixed-residual test. The same argument gives eight necessary +residues if a chosen finite normalized Clifford lift includes eighth-root +scalar phases. The four-test conclusion is for the repository's exact +Gaussian-dyadic group, not that larger central extension. + +## 6. Quantifiers, applications and exclusions + +At a single specified f>=4n+4, the coefficient vector may be chosen after +f. Its entries may be arbitrary complex numbers. Its finite support and +the finite word that produces it may also depend on f. There is no term +count in the theorem. Thus an equality at that width can be read as an +identity in the projective phase quotient of the group algebra. A scalar +phase is evaluated as its f-th power, not discarded. + +This gives an explicit threshold for future applications of the retained +finite-alphabet tensor-separation arguments. It replaces an unspecified +large width or a projective-group-size bound when the entire operator +alphabet in the argument is contained in this fixed n-axis Clifford group. +For n=9 the pointwise threshold is 40 and the four test widths are 40..43. +For n=17 they are 72 and 72..75. At n=64 they are 260 and 260..263. +The prior full-Clifford fixed-residual tests are 69..76, 133..140 and +509..516 respectively. These comparisons are theorem bounds, not measured +execution speedups. + +The [retained passive application](APPLICATION.md) meets the full alphabet +premise. It gives a uniform width-72 obstruction and an operator error bound +of 1/3 under that exact passive contract. Its sources and both mandatory +clarifications are retained as byte-pinned inputs. + +For stabilizer maps, terms which differ by any nonzero scalar must first be +combined with that scalar raised to f. Their coefficients may then depend +on f. Formula (3) does not identify scaled copies at all widths, and it does +not give four tests for arbitrary nonunitary scalings. + +This does not by itself strengthen an additional-call bound at a caller +cut with already paid observations. That needs its correct initial module, +source versions, ownership and cost ledger. Nor does it show that any +particular paid-history theorem's whole alphabet consists of Clifford +maps. A nominal matrix or a sum of Cliffords is not automatically a +Clifford or a stabilizer map. Each application must check that premise. + +Arbitrary non-Clifford matrices, nonlinear/rounded operations, operators +which act across tensor columns, unpriced physical routing, and omitted +dirty returns remain outside the result. No all-size multiplication +assumption is declared discharged by this algebraic theorem alone. + +## 7. Verification and attribution + +The registered verifier checks the finite counting identities by separate +state and signed-Pauli enumerations, the rational tail bounds, literal Gram +matrices, complete native register examples and deliberate invalid inputs. +The written proof supplies the all-dimension and all-width quantifiers. +Finite computation is corroboration; it is not a formal-kernel proof or +independent human acceptance. + +The retained tensor-Gram package supplies the exact native grammar, compact +quadratic sums and complete register frontend. Its original trace filter, +code invariant, one-axis sharpness and provider results remain its work. +The monomial tensor-cutoff package remains a stronger cutoff for its smaller +class. Chris R and the retained paid-history authors supply the earlier +finite-alphabet applications. Krzysztof Wojt and Nick Petalas supply the +repository's related residual-form and partial-Pauli statements. + +Classical stabilizer descriptions follow Dehaene and De Moor, +[*Clifford group, stabilizer states, and linear and quadratic operations +over GF(2)*](https://arxiv.org/abs/quant-ph/0304125). The finite symplectic residual-form +method is classical Wall-form theory. No general counting, Gram, Fourier, +stabilizer-simulation or literature-priority claim is made. Exact repository +pins and the role of each source are in SOURCES.json and README.md. + +## Open next questions + +Find the least pointwise threshold and best spectral constant for this +group, with the phase residue kept explicit. Test one actual complete +caller against the new pointwise kernel, retaining its available history +and complete bill. Extend the exact native frontend to a source-bound +nonunitary stabilizer caller only when its projections and scalar factors +are supplied. None of these follow-ups is claimed complete here. diff --git a/research/clifford-pointwise-audit/source/PR5526-README.md b/research/clifford-pointwise-audit/source/PR5526-README.md new file mode 100644 index 0000000000..a250d034c5 --- /dev/null +++ b/research/clifford-pointwise-audit/source/PR5526-README.md @@ -0,0 +1,207 @@ +# Pointwise Clifford tensor faithfulness and a complete frozen-repair obstruction + +**Enabling proof and exact verification tools; no new kappa.** +For the full n-axis Clifford group, projectively distinct operators have +linearly independent tensor powers at **every width f>=4n+4**. Their +normalized tensor Gram matrix lies between **I/9 and 17I/9**. This holds +for arbitrary complex coefficients and finite words chosen separately at +each width. It gives a dimension-based threshold for the finite-alphabet +arguments used throughout the native-interface research. + +For one fixed complete scalar register program over the Gaussian-dyadic +Clifford group, **four tests at 4n+4,...,4n+7 decide equality at all positive +widths**. Four tests are necessary because of scalar phases. At least one +of those four normalized squared residuals is at least M/9, where M is the +squared coefficient norm after equal exact operators are combined. + +Read the [proof](PROOF.md), [exact result](RESULT.json), [source pins](SOURCES.json) +and [source-bound application](APPLICATION.md). The application strengthens +the retained passive saved-query ceiling: failure holds at every **f>=72**, +with worst-case operator error at least **1/3** in each affected coefficient. +At every f>=84 its normalized squared error is at least **125/126**. +The old observation contract and both source clarifications remain binding. + +The [paid-repair extension](REPAIR.md) now proves that this caller needs +**at least 104 additional field returns**, even with feedback among new +calls. With q returns, the selected block has squared operator norm error +at least **(1-q/104)_+/9** from width 72. The cheapest possible 104-return +repair makes the complete frozen invoice adverse for **every r^p tariff, +0> axis) & 1) << other) + out[2*r*d:2*(r+1)*d] = a[2*s*d:2*(s+1)*d] + else: + raise ValueError('Unknown gate') + return e, tuple(out) + + +def exact_group(n, omit_h=False): + alphabet = [(kind, j, 0) for j in range(n) + for kind in (('S',) if omit_h else ('H', 'S'))] + alphabet += [('CX', j, k) for j in range(n) for k in range(n) if j != k] + start = identity(n) + found, queue = {start}, deque([start]) + while queue: + m = queue.popleft() + for name, j, k in alphabet: + out = gate(m, n, name, j, k) + if out not in found: + found.add(out) + queue.append(out) + need(len(found) <= 46080, 'Finite-domain guard') + return sorted(found), len(alphabet)*len(found) + + +def inner(a, b): + """Unnormalized Hilbert--Schmidt inner product, exact in Q(i).""" + ea, aa = a + eb, bb = b + re = sum(aa[j]*bb[j]+aa[j+1]*bb[j+1] for j in range(0, len(aa), 2)) + im = sum(aa[j]*bb[j+1]-aa[j+1]*bb[j] for j in range(0, len(aa), 2)) + return F(re, 1 << (ea+eb)), F(im, 1 << (ea+eb)) + + +def unitary(matrix, d): + e, a = matrix + for r in range(d): + for s in range(d): + real = imag = 0 + for c in range(d): + j, k = 2*(r*d+c), 2*(s*d+c) + real += a[j]*a[k]+a[j+1]*a[k+1] + imag += a[j+1]*a[k]-a[j]*a[k+1] + need(real == ((1 << (2*e)) if r == s else 0) and imag == 0, + 'Literal unitary identity') + + +def mul(a, b): + return a[0]*b[0]-a[1]*b[1], a[0]*b[1]+a[1]*b[0] + + +def sub(a, b): + return a[0]-b[0], a[1]-b[1] + + +def div(a, b): + den = b[0]*b[0]+b[1]*b[1] + need(den != 0, 'Nonzero Gaussian divisor') + return (a[0]*b[0]+a[1]*b[1])/den, (a[1]*b[0]-a[0]*b[1])/den + + +def power(a, n): + result = (F(1), F(0)) + while n: + if n & 1: + result = mul(result, a) + a = mul(a, a) + n //= 2 + return result + + +def rank(matrix): + a = [row.copy() for row in matrix] + pivot = 0 + for j in range(len(a[0])): + found = next((i for i in range(pivot, len(a)) if a[i][j] != (0, 0)), None) + if found is None: + continue + a[pivot], a[found] = a[found], a[pivot] + for i in range(pivot+1, len(a)): + if a[i][j] == (0, 0): + continue + factor = div(a[i][j], a[pivot][j]) + for k in range(j, len(a[0])): + a[i][k] = sub(a[i][k], mul(factor, a[pivot][k])) + pivot += 1 + if pivot == len(a): + break + return pivot + + +def gram(matrices, n, width): + d = 1 << n + return [[power(tuple(x/d for x in inner(a, b)), width) for b in matrices] + for a in matrices] + + +def positive(matrix): + """Exact Hermitian Schur complements; no floating eigenvalue routine.""" + a = [row.copy() for row in matrix] + for j in range(len(a)): + need(a[j][j][1] == 0 and a[j][j][0] > 0, 'Strictly positive Hermitian pivot') + for r in range(j+1, len(a)): + factor = div(a[r][j], a[j][j]) + for c in range(j+1, len(a)): + a[r][c] = sub(a[r][c], mul(factor, a[j][c])) + + +def spectral_checks(matrices): + for width in range(8, 12): + g = gram(matrices, 1, width) + low = [[sub(g[r][c], (F(int(r == c), 9), F(0))) for c in range(24)] + for r in range(24)] + high = [[sub((F(17*int(r == c), 9), F(0)), g[r][c]) for c in range(24)] + for r in range(24)] + positive(low) + positive(high) + return {'axes': 1, 'widths': [8, 9, 10, 11], + 'strict_lower': '1/9', 'strict_upper': '17/9', 'positive_pivots': 192} + + +def group_receipt(n): + group, edges = exact_group(n) + expected_projective = (1 << (n*n+2*n)) + for j in range(1, n+1): + expected_projective *= (1 << (2*j))-1 + need(len(group) == 4*expected_projective, 'Complete exact Clifford group size') + fibers = Counter(projective(m) for m in group) + need(set(fibers.values()) == {4}, 'Four exact Gaussian phase lifts') + hist = Counter() + for m in fibers: + unitary(m, 1 << n) + real, imag = inner(identity(n), m) + hist[(real*real+imag*imag)/(1 << (2*n))] += 1 + need(hist[F(1, 2)] == 2*((1 << (2*n))-1), 'First Clifford overlap count') + need(hist[F(1)] == 1, 'Only identity projective class has unit trace overlap') + width = 4*n+4 + row_sum = sum(count*q**(width//2) for q, count in hist.items() if q != 1) + need(row_sum < F(8, 9), 'Literal finite Gram row budget') + return {'axes': n, 'exact_matrices': len(group), 'projective_classes': len(fibers), + 'generator_edges': edges, 'phase_fiber_size': 4, + 'width': width, 'absolute_gram_row_sum': str(row_sum), + 'normalized_trace_squared_histogram': {str(k): v for k, v in sorted(hist.items())}}, sorted(fibers) + + +def phase_and_gram_checks(one_axis): + ranks = {str(f): rank(gram(one_axis, 1, f)) for f in range(1, 12)} + need(all(ranks[str(f)] == 24 for f in range(8, 12)), 'Four-width positive fixture') + need(ranks['1'] < 24, 'Small-width independence must fail') + i = (F(0), F(1)) + phase_controls = [] + for omitted in range(4): + values = [] + for f in range(8, 12): + terms = [power(i, ((f-omitted)*j) % 4) for j in range(4)] + value = tuple(sum(t[k] for t in terms) for k in range(2)) + need(value == ((F(4), F(0)) if f % 4 == omitted else (F(0), F(0))), + 'Missing-residue false acceptance control') + values.append([str(x) for x in value]) + phase_controls.append({'omitted_residue': omitted, 'widths_8_to_11': values}) + h = gate(identity(1), 1, 'H', 0) + need(gate(h, 1, 'H', 0) == rotate(identity(1)), 'H-prime square retains i') + duplicate = [identity(1), rotate(identity(1))] + need(all(rank(gram(duplicate, 1, f)) == 1 for f in range(1, 9)), + 'Scalar copies must be combined pointwise') + smaller, _ = exact_group(1, omit_h=True) + need(len(smaller) != 96, 'Omitted Hadamard must not certify the full group') + need(mul((F(2), F(0)), power(i, 2)) != power(mul((F(2), F(0)), i), 2), + 'Exterior scalar differs from tensor-lifted scalar') + for f in range(1, 13): + c = tuple(-x for x in power(i, (-f) % 4)) + need(mul(c, power(i, f)) == (-F(1), F(0)), + 'Width-dependent formal residual vanishes pointwise') + need(c != (0, 0), 'Width-dependent coefficient vector is nonzero') + # P(x)=product_(j=0..3)(x-2**(8+j)); coefficient c_k multiplies [2**k I]. + coeffs = [1] + for f in range(8, 12): + out = [0]*(len(coeffs)+1) + for k, c in enumerate(coeffs): + out[k] -= (1 << f)*c + out[k+1] += c + coeffs = out + values = [sum(c*(1 << (k*f)) for k, c in enumerate(coeffs)) for f in range(8, 13)] + need(values[:4] == [0]*4 and values[4] != 0, + 'Arbitrary nonunitary scales do not have a four-width test') + return {'one_axis_gram_ranks': ranks, 'omitted_residue_controls': phase_controls, + 'nonunitary_scale_counterexample_coefficients': coeffs, + 'nonunitary_scale_values_at_widths_8_to_12': values, + 'other_controls': ['small_width', 'H_prime_square_phase', 'duplicate_phase_classes', + 'omitted_H_generator', 'exterior_scalar_placement', + 'width_dependent_coefficients', 'arbitrary_nonunitary_scales']} + + +def source_checks(): + rows = json.loads((HERE/'SOURCE-RECEIPT.json').read_text())['files'] + result = [] + for row in rows: + data = (HERE/row['local_path']).read_bytes() + sha = hashlib.sha256(data).hexdigest() + blob = hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest() + need(sha == row['sha256'] and blob == row['git_blob'], 'Frozen source byte mismatch') + result.append({'path': row['local_path'], 'sha256': sha, 'git_blob': blob}) + return result + + +def calculate(): + sources = source_checks() + one, matrices = group_receipt(1) + two, _ = group_receipt(2) + return {'schema': 'clifford-pointwise-independent-matrix-audit/v1', + 'scope': 'Finite exact corroboration only; universal claims require AUDIT.md', + 'sources': sources, 'groups': [one, two], 'phase_and_gram': phase_and_gram_checks(matrices), + 'spectral_check': spectral_checks(matrices)} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit', action='store_true') + args = parser.parse_args() + result = calculate() + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + need(result == json.loads((HERE/'MATRIX-RESULT.json').read_text()), 'Matrix receipt mismatch') + print('PASS_CLIFFORD_POINTWISE_MATRIX_AUDIT: 46176 exact matrices; complete receipt matched') + + +if __name__ == '__main__': + main() diff --git a/research/clifford-pointwise-audit/verify_symplectic.py b/research/clifford-pointwise-audit/verify_symplectic.py new file mode 100644 index 0000000000..27d0781745 --- /dev/null +++ b/research/clifford-pointwise-audit/verify_symplectic.py @@ -0,0 +1,247 @@ +#!/usr/bin/env python3 +"""Independent finite evidence for PR5526 Sections 3--5; standard library only. + +Prepared for DLamdata with substantial OpenAI Codex assistance, Apache-2.0. +No predecessor executable is imported. Enumerates every binary matrix on <=4 +coordinates, rather than generating Clifford gates/tableaux or Choi states. +Finite evidence does not replace the all-dimension proof review. +""" + +from collections import Counter, defaultdict +from fractions import Fraction +from itertools import product +import json + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def omega(x, y, n): + mask = (1 << n) - 1 + return (((x & mask) & (y >> n)).bit_count() + + ((x >> n) & (y & mask)).bit_count()) % 2 + + +def apply(columns, v): + out = 0 + for j, column in enumerate(columns): + if (v >> j) & 1: + out ^= column + return out + + +def binary_rank(columns): + pivots = {} + for column in columns: + while column: + p = column.bit_length() - 1 + if p in pivots: + column ^= pivots[p] + else: + pivots[p] = column + break + return len(pivots) + + +def symplectic(columns, n): + return all(omega(columns[i], columns[j], n) == omega(1 << i, 1 << j, n) + for i in range(2*n) for j in range(i + 1, 2*n)) + + +def transvections(n): + return { + tuple((1 << j) ^ (a if omega(1 << j, a, n) else 0) + for j in range(2*n)) + for a in range(1, 1 << (2*n)) + } + + +def gaussian_binomial(n, k): + if k < 0 or k > n: + return 0 + rows = [1] + [0] * k + for dim in range(1, n + 1): + rows = [1] + [rows[j] + (1 << (dim-j)) * rows[j-1] + if j <= dim else 0 for j in range(1, k+1)] + return rows[k] + + +def state_overlap_bound(naxes, k): + return gaussian_binomial(naxes, k) * (1 << (k*(k+3)//2)) + + +def census(n): + m, q = 2*n, 1 << (2*n) + hist = Counter() + lifted = Counter() + rank_one = set() + residual_keys = set() + per_subspace = Counter() + character_sums = 0 + residual_pairs = 0 + candidates = 0 + for columns in product(range(q), repeat=m): + candidates += 1 + if not symplectic(columns, n): + continue + images = tuple(apply(columns, v) for v in range(q)) + require(len(set(images)) == q, 'noninvertible-preserver') + displacement = tuple(columns[j] ^ (1 << j) for j in range(m)) + k = binary_rank(displacement) + fixed = tuple(v for v in range(q) if images[v] == v) + require(len(fixed) == 1 << (m-k), 'fixed-rank-disagreement') + image = tuple(sorted({images[v] ^ v for v in range(q)})) + require(len(image) == 1 << k, 'image-rank-disagreement') + hist[k] += 1 + if k == 1: + rank_one.add(columns) + + # Restrict every Pauli commutation character to the actual fixed space. + # An arbitrary base sign character translates this multiset, so the + # count is independent of which Clifford lift is chosen first. + sums = [sum(1 if omega(p, v, n) == 0 else -1 for v in fixed) + for p in range(q)] + character_sums += q + require(set(sums) <= {0, len(fixed)}, 'character-not-orthogonal') + positive = sum(s != 0 for s in sums) + require(positive == 1 << k, 'wrong-nonzero-lift-count') + lifted[k] += positive + + # Compute B from actual preimages; no formula enumeration is used. + preimages = defaultdict(list) + for x in range(q): + preimages[images[x] ^ x].append(x) + table = [] + for u in image: + row = [] + for w in image: + values = {omega(x, w, n) for x in preimages[u]} + require(len(values) == 1, 'residual-not-well-defined') + row.append(values.pop()) + table.append(tuple(row)) + require(all(u == 0 or any(table[i]) for i, u in enumerate(image)), + 'residual-left-degenerate') + for i, u in enumerate(image): + for j, v in enumerate(image): + require(table[i][j] ^ table[j][i] == omega(u, v, n), + 'wrong-residual-symmetrization') + residual_pairs += 1 + key = (image, tuple(table)) + require(key not in residual_keys, 'residual-not-injective') + residual_keys.add(key) + per_subspace[image] += 1 + + require(candidates == 1 << (m*m), 'incomplete-matrix-domain') + require(rank_one == transvections(n), 'rank-one-transvection-mismatch') + for image, count in per_subspace.items(): + k = len(image).bit_length() - 1 + require(count <= 1 << (k*(k+1)//2), 'too-many-residual-forms') + require(lifted[0] == 1, 'identity-overlap-count') + require(lifted[1] == 2*(q-1), 'first-overlap-count') + for k in range(m+1): + require(lifted[k] <= state_overlap_bound(m, k), 'general-overlap-bound') + require(sum(hist.values()) == (6 if n == 1 else 720), 'group-size-fixture') + return { + 'axes': n, 'binary_matrices_tested': candidates, + 'symplectic_matrices': sum(hist.values()), + 'displacement_rank_histogram': dict(sorted(hist.items())), + 'nonzero_trace_lift_histogram': dict(sorted(lifted.items())), + 'character_sums': character_sums, + 'residual_symmetrization_pairs': residual_pairs, + 'distinct_residual_forms': len(residual_keys), + } + + +def dk(k): + out = 1 + for j in range(1, k+1): + out *= (1 << j) - 1 + return out + + +def bound_and_phases(): + # Independent rational series: retain four terms and dominate k>=5 by + # the geometric ratio first encountered after k=5 (1/63, scaled by 2^-s). + def clifford_tail(s): + initial = Fraction(1, 1 << (s+1)) + finite = sum((Fraction(1, (1 << (s*k))*dk(k)) for k in range(2, 5)), + Fraction()) + tail = Fraction(1, (1 << (5*s))*dk(5)) / (1-Fraction(1, (1 << s)*63)) + return initial + finite + tail + + c0, c2, c6 = (clifford_tail(s) for s in (0, 2, 6)) + require(c0 < Fraction(8, 9), 'clifford-uniform-tail') + require(c2 < Fraction(3, 20), 'clifford-later-tail-s2') + require(c6 < Fraction(1, 126), 'clifford-later-tail-s6') + st = sum((Fraction(1, (1 << k)*dk(k)) for k in range(1, 5)), Fraction()) + st += Fraction(1, (1 << 5)*dk(5)) / (1-Fraction(1, 126)) + require(st < Fraction(3, 5), 'stabilizer-uniform-tail') + + # Independent finite rational check of the subspace-count domination, + # including all actual k, for an explicit bounded 1<=N<=32 domain. + finite_terms = 0 + for axes in range(1, 33): + for k in range(1, axes+1): + term = Fraction(state_overlap_bound(axes, k), 1 << (k*(axes+2))) + require(term <= Fraction(1, dk(k)), 'finite-subspace-term') + finite_terms += 1 + + # Gaussian integers represented as pairs; no floating complex arithmetic. + roots = ((1, 0), (0, 1), (-1, 0), (0, -1)) + def add(xs): + return (sum(x[0] for x in xs), sum(x[1] for x in xs)) + # Fourier orthogonality simultaneously checks inversion and each missing + # residue witness. The four exact operators i^j I are kept separate. + fourier = [] + for r in range(4): + row = [add([roots[((f-r)*j) % 4] for j in range(4)]) for f in range(4)] + require(row == [(4, 0) if f == r else (0, 0) for f in range(4)], + 'phase-fourier-orthogonality') + fourier.append(row) + return { + 'clifford_row_sum_majorants': {'s0': str(c0), 's2': str(c2), 's6': str(c6)}, + 'stabilizer_row_sum_majorant': str(st), + 'finite_subspace_terms': finite_terms, + 'four_residue_witness_values': fourier, + } + + +def controls(): + # Direct domain controls: reject invertible matrices that fail the actual + # alternating form, and reject singular matrices even if a few pairs agree. + identity = (1, 2, 4, 8) + require(symplectic(identity, 2), 'identity-positive-control') + bad = (1, 3, 4, 8) + require(binary_rank(bad) == 4 and not symplectic(bad, 2), + 'invertible-is-not-symplectic-control') + require(not symplectic((1, 2, 4, 4), 2), 'singular-control') + require(omega(1, 4, 2) == 1 and omega(1, 2, 2) == 0, + 'pairing-coordinate-control') + # Explicit failure of phase deletion: [I]-[iI] is zero at f=4 and nonzero + # at f=1; three residue tests miss their complementary Fourier witness. + roots = ((1, 0), (0, 1), (-1, 0), (0, -1)) + def identity_minus_phase(f): + phase = roots[f % 4] + return (1-phase[0], -phase[1]) + require(identity_minus_phase(4) == (0, 0) + and identity_minus_phase(1) != (0, 0), 'phase-deletion-control') + # Dropping the half factor in the first overlap estimate destroys the + # claimed 8/9 universal row budget even before the remaining positive tail. + require(Fraction(1) + Fraction(1, 3) > Fraction(8, 9), + 'first-overlap-half-is-essential') + return ['identity-positive', 'invertible-nonsymplectic', 'singular', + 'pairing-coordinates', 'phase-deletion', 'first-overlap-half'] + + +def main(): + result = {'scope': 'PR5526 Sections 3--5 independent direct binary-matrix audit', + 'censuses': [census(1), census(2)], + 'bounds_and_phases': bound_and_phases(), 'controls': controls()} + print(json.dumps(result, indent=2, sort_keys=True)) + print('PASS_INDEPENDENT_SYMPLECTIC_OVERLAP_AUDIT') + + +if __name__ == '__main__': + main()