From 0cb193553398e9ce6f44bd7cff553e234a9acc2f Mon Sep 17 00:00:00 2001 From: Mihir Srivastava Date: Sat, 24 Oct 2026 23:22:11 -0700 Subject: [PATCH 1/2] Audit native tensor cutoff and prove sharp one-axis test Independently review PR5369 Sections 2/3/5 and corroborate them with exact phase-character enumeration and literal Gaussian ranks. Preserve the general theorem and selected frontier; disclose substantial OpenAI Codex assistance and predecessor credit. --- .../EVIDENCE.json | 7 + .../native-cutoff-independent-audit/LICENSE | 201 ++++++++++++ .../MUTATIONS.json | 79 +++++ .../native-cutoff-independent-audit/PROOF.md | 214 +++++++++++++ .../native-cutoff-independent-audit/README.md | 142 +++++++++ .../RESULT.json | 133 ++++++++ .../SOURCES.json | 24 ++ .../native-cutoff-independent-audit/TASK.json | 103 +++++++ .../VERIFY.json | 48 +++ .../audit_mutations.py | 68 +++++ .../native-cutoff-independent-audit/verify.py | 287 ++++++++++++++++++ 11 files changed, 1306 insertions(+) create mode 100644 research/native-cutoff-independent-audit/EVIDENCE.json create mode 100644 research/native-cutoff-independent-audit/LICENSE create mode 100644 research/native-cutoff-independent-audit/MUTATIONS.json create mode 100644 research/native-cutoff-independent-audit/PROOF.md create mode 100644 research/native-cutoff-independent-audit/README.md create mode 100644 research/native-cutoff-independent-audit/RESULT.json create mode 100644 research/native-cutoff-independent-audit/SOURCES.json create mode 100644 research/native-cutoff-independent-audit/TASK.json create mode 100644 research/native-cutoff-independent-audit/VERIFY.json create mode 100644 research/native-cutoff-independent-audit/audit_mutations.py create mode 100644 research/native-cutoff-independent-audit/verify.py diff --git a/research/native-cutoff-independent-audit/EVIDENCE.json b/research/native-cutoff-independent-audit/EVIDENCE.json new file mode 100644 index 0000000000..22cfbb211b --- /dev/null +++ b/research/native-cutoff-independent-audit/EVIDENCE.json @@ -0,0 +1,7 @@ +{ + "python": "3.12.0", + "platform": "Windows-11-10.0.26300-SP0", + "normal_optimized_identical": true, + "source_base": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "scope": "Local native Windows execution. Registered replay and export evidence are reported in README.md. Finite controls are not a proof kernel." +} diff --git a/research/native-cutoff-independent-audit/LICENSE b/research/native-cutoff-independent-audit/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/native-cutoff-independent-audit/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/native-cutoff-independent-audit/MUTATIONS.json b/research/native-cutoff-independent-audit/MUTATIONS.json new file mode 100644 index 0000000000..ce18a4b459 --- /dev/null +++ b/research/native-cutoff-independent-audit/MUTATIONS.json @@ -0,0 +1,79 @@ +{ + "mutation_driver_sha256": "891ba9a53c44246355bd03cb477aaaa176eba6269910ab7bbba856d5095e097c", + "records": [ + { + "exit_code": 1, + "expected_rejection": "literal phase mismatch", + "mutation": "erase_quadratic_phase", + "optimized": false + }, + { + "exit_code": 1, + "expected_rejection": "one-axis window rank failed", + "mutation": "tensor_constant_once", + "optimized": false + }, + { + "exit_code": 1, + "expected_rejection": "padding changed character or span", + "mutation": "omit_span_condition", + "optimized": false + }, + { + "exit_code": 1, + "expected_rejection": "missing phase character", + "mutation": "forbid_multiplicity_four", + "optimized": false + }, + { + "exit_code": 1, + "expected_rejection": "sharpness trap did not vanish", + "mutation": "wrong_weight_projector", + "optimized": false + }, + { + "exit_code": 1, + "expected_rejection": "source proof hash mismatch", + "mutation": "changed_source_proof", + "optimized": false + }, + { + "exit_code": 1, + "expected_rejection": "literal phase mismatch", + "mutation": "erase_quadratic_phase", + "optimized": true + }, + { + "exit_code": 1, + "expected_rejection": "one-axis window rank failed", + "mutation": "tensor_constant_once", + "optimized": true + }, + { + "exit_code": 1, + "expected_rejection": "padding changed character or span", + "mutation": "omit_span_condition", + "optimized": true + }, + { + "exit_code": 1, + "expected_rejection": "missing phase character", + "mutation": "forbid_multiplicity_four", + "optimized": true + }, + { + "exit_code": 1, + "expected_rejection": "sharpness trap did not vanish", + "mutation": "wrong_weight_projector", + "optimized": true + }, + { + "exit_code": 1, + "expected_rejection": "source proof hash mismatch", + "mutation": "changed_source_proof", + "optimized": true + } + ], + "status": "PASS_NATIVE_CUTOFF_AUDIT_MUTATIONS", + "verifier_sha256": "2f0166a9e0bd0a2e5113f3a6847e8f7e3642a8bf69032a53d7ce72fd21995b7a" +} diff --git a/research/native-cutoff-independent-audit/PROOF.md b/research/native-cutoff-independent-audit/PROOF.md new file mode 100644 index 0000000000..8d9aa719f9 --- /dev/null +++ b/research/native-cutoff-independent-audit/PROOF.md @@ -0,0 +1,214 @@ +# Independent audit and the sharp one-axis monomial cutoff + +Mihir Srivastava, with substantial OpenAI Codex assistance. Apache-2.0. + +## Source and decision + +This reviews Sections 2, 3 and 5 of Ali Romman's +[PR5369 proof](https://github.com/aliromman/integer-mult-bounds/blob/18354f41de4dc7bfda4692e814cf1d91a6d619ef/research/native-tensor-cutoff/PROOF.md). +The reviewed source is retained unchanged on base main +`32890bc5de034ab8fc93ac88ead7279a6a416d04`, at +`research/native-tensor-cutoff/PROOF.md`, Git blob +`2d92f17cd8e1064028656cd4ff06c1d38f14ebc0`, SHA256 +`b2d31ea52b652f43cc8576affde6092a884d2832820221a43933e7e27dc07041`. +The central ledger records archival intake with scientific review open. + +**Scoped assessment:** the phase-character construction, affine separation +and fixed-residue conclusion follow under the written hypotheses. No gap was +found in these implications. The proof below spells out the factorization and +quantifier steps used in that assessment. This is a separate agent-assisted +mathematical audit, not independent human review or formal-kernel acceptance. +It does not validate the predecessor's entire executable checker. + +**Additional result:** for the one-axis monomial group, the evaluation rank is +`2 min(f+1,4)` at every positive width f. The least common stabilization +threshold is 3; widths **3,4,5,6** form a complete fixed-program test, with +both four tests and maximum width six necessary. This is a specialization +and sharpening of the source's sufficient window 6,7,8,9. It is not a +correction to that sufficient theorem. No global literature priority is claimed. + +## Audit of the general argument + +Use the source's exact group: on x in F2^n, + + U(A,t,c,a,b)e_x = i^(c + sum a_j x_j + 2 sum b_jk x_j x_k) e_(Ax+t). + +Here A is invertible, c and a_j are modulo four, b_jk modulo two, and the +phase is evaluated at the input. Coefficients of the group algebra element +P are fixed complex scalars outside tensor powers. The same P is used at +every test width. The recipe is independent of width. Those premises are +needed for the four-width implication. + +### 1. Binary Gram factorization is sufficient, including singular forms + +For any symmetric binary n-by-n matrix B, congruence elimination gives a +direct sum of a one-dimensional identity blocks, b hyperbolic pairs and a +zero radical. To justify the elimination: a vector with self-pairing one +splits off a one-dimensional nondegenerate summand. Once all self-pairings +are zero, a nonzero pairing splits off a hyperbolic pair; repeat until only +the radical remains. + +Realize the identity blocks on a separate a-dimensional orthonormal space. +If b>0, the even-weight subspace E of F2^(2b+1) is alternating and +nondegenerate. Indeed E-perp is the span of the all-ones vector, which has +odd weight and does not lie in E. Choose a symplectic basis by successively +pairing a nonzero vector with a vector having pairing one, then passing to +their orthogonal complement. This realizes the b hyperbolic pairs. +Map the radical to zero. Undo the congruence to obtain B=YY^T with at most +a+2b+1 <= n+1 columns (a columns if b=0). No nonsingularity of B is assumed. + +### 2. Gram parity and the two-copy correction have different jobs + +Given a phase character (r,u,v), start with 0,e_1,...,e_n. Its Gram matrix +is I. Let M have diagonal u mod two and off-diagonal v. Append columns of a +factorization M+I=YY^T. This supplies the desired pair statistics and the +parity of every coordinate count, but not yet its residue modulo four. + +If w is the resulting coordinate-count vector modulo four, each u_j-w_j +is even. Set z_j=(u_j-w_j)/2 modulo two and append z twice when z is nonzero. +This adds 2z_j to each coordinate count and zero to each pair count modulo +two. The tuple still contains the original affine basis. Its length is at +most (n+1)+(n+1)+2=2n+4. For ANY prescribed f>=2n+4 with f=r modulo four, +pad with zero points to length f. Coordinate and pair statistics stay fixed; +the constant statistic becomes f modulo four=r. Padding is valid even if +the intermediate tuple has a different length residue. + +Thus every phase character is realizable at the appropriate member of the +four-width window. The executable audit uses complete small multisets instead +of this Gram construction; it does not test an independently rewritten copy +of the same factorization algorithm. + +### 3. The chosen tuple isolates the affine bucket + +Select a bucket (A,t) with a nonzero coefficient function on the diagonal +phase subgroup D. Fourier inversion on +`D = (Z/4)^(n+1) x (Z/2)^(n(n-1)/2)` supplies a character chi with nonzero +coefficient sum. Take its spanning tuple X and put Y=AX+t componentwise. +If another affine map agrees on all of X, it agrees on an affine basis and +is the same map. Therefore the (Y,X) matrix entry is exactly that nonzero +Fourier sum: other buckets cannot cancel it. + +The source's sequential sparse Fourier choices are also sufficient: if all +two or four choices on one coefficient coordinate gave zero remaining +tables, inverse Fourier transformation on that coordinate would give the +zero original table. Retain one nonzero table at each stage. There are +O(n^2) coordinates, at most four trials each, with at most s stored terms. +This verifies the stated O(s n^2) exact scalar-operation count. It is not a +bit-complexity bound or a polynomial bound on circuit expansion. + +### 4. The residue statement and all-width statement use different quantifiers + +For a FIXED residue r, define + + beta(A,t,a,b) = sum_c alpha(A,t,c,a,b) i^(r c). + +At any specified f>=2n+4 with f=r modulo four, beta=0 implies a zero +operator by collecting terms. Conversely, a nonzero beta has a nonzero +Fourier coefficient over (a,b). Step 2 realizes that character at this +specified f with constant statistic r, and Step 3 gives a nonzero entry. +Thus the kernel at each such f is exactly the constant-phase relation. + +For a single fixed P, zero operators at the four consecutive widths imply +beta=0 for all four r. Fourier inversion on c then gives every alpha=0. +Allowing a different P_f at each width invalidates this last inference: +`[iI] - i^f[I]` is a nonzero group-algebra element that evaluates to zero at +that f. This is an explicit control, not a counterexample to the source. + +The central projectors `C_r=sum_c i^(-r c)[i^c I]` show why every residue is +needed. This step and the source's phase grammar were inspected as dependencies +of Sections 2/3/5. Section 4's growing-width projector family and Section 6's +complexity reduction were not audited here. + +## Sharp one-axis theorem + +For n=1 there is no quadratic pair and GL_1(F2)={1}. The group has exactly +32 elements U(t,c,a), with t in F2 and c,a in Z/4. Write + + P = sum_(t,c,a) alpha(t,c,a) [U(t,c,a)], + beta_r(t,a) = sum_c alpha(t,c,a) i^(r c). + +For a binary tuple x of length f and weight k, its output tuple under +U(t,c,a) is x+t (componentwise), with phase i^(fc+ak). As f>0, the t=0 and +t=1 outputs are distinct. Hence the two translation buckets have disjoint +matrix-entry supports, and evaluation on each bucket is the Fourier map + + (beta_r(t,a))_(a=0..3) -> (sum_a beta_r(t,a) i^(a k))_(k=0..f), + r = f mod 4. + +Every weight 0,...,f occurs. The distinct rows are min(f+1,4) rows of the +invertible four-point Fourier matrix, so each bucket has that rank. The map +alpha -> beta_r is onto. Consequently + + rank rho_f = 2 min(f+1,4) (f>=1). + +For f>=3, the rank is eight and the kernel is exactly beta_r=0. At f=2 it +is six, so no threshold below three has this stabilization property. + +Fourier transformation in c splits the 32-dimensional group algebra into +four eight-dimensional residue sectors. The widths 3,4,5,6 provide rank eight +in every sector and therefore have joint rank 32. The first two positive +consecutive windows have ranks 26 (1..4) and 30 (2..5). The verification +computes those ranks from literal operator entries using Gaussian rational +elimination, without using weights to generate the entries. + +Both the number of tests and maximum width six are sharp. The central +projectors above exclude any set missing a residue. More strongly, consider + + R = sum_(c,a=0..3) i^(-2c-3a) [U(0,c,a)] = C_2 Q_3, + Q_3 = sum_a i^(-3a)[U(0,0,a)]. + +R has sixteen nonzero coefficients. Its diagonal entry on a weight-k tuple +is 16 exactly when f=2 modulo four and k=3 modulo four; it is zero otherwise. +It vanishes at ALL positive f<6: at f=2 no weight-three tuple exists, and +the other widths have the wrong central residue. At f=6 the tuple +`(1,1,1,0,0,0)` has entry 16. No test set with maximum width below six can +therefore certify all-width equality. Normalizing R by 16 is optional. + +This is the monomial subgroup, not PR5376's full Clifford group. The +one-axis full-Clifford cutoff and the all-axis least monomial cutoff are +separate questions. In particular, a shortest affinely spanning realization +of every phase character need not give the least faithful tensor width. +For n=1 even one input point distinguishes the only two affine maps; the +general affine-span requirement is sufficient but unnecessarily strong. + +## Complete small character enumeration and its limits + +For a tuple, reduce every positive point multiplicity m to +`1+((m-1) mod 4)`. This preserves its support, all phase statistics and +affine span, and weakly decreases its length. Therefore enumerating +`{0,1,2,3,4}^(2^n)` contains a shortest spanning tuple for every character. +The verifier exhausts this domain for n=1,2,3, then evaluates every chosen +witness and zero-padded witness against the literal phase generators. + +| Axes | Multisets | Characters | Spanning supports | Affine maps | Largest shortest length for residues 0,1,2,3 | +|---:|---:|---:|---:|---:|---| +| 1 | 25 | 16 | 1 | 2 | 8,5,6,7 | +| 2 | 625 | 128 | 5 | 24 | 8,9,6,7 | +| 3 | 390625 | 2048 | 149 | 1344 | 8,9,10,7 | + +Every spanning support is also checked against every affine map, independently +of the tuple minimization. Receipt digests bind the complete sorted minima +tables. These are exact finite character-realization minima; the table is +NOT a claim of least representation cutoff for n=2 or n=3. + +The trust base includes Python integers/Fraction, this verifier, its phase +grammar, and the written argument above. Neither predecessor executable is +imported. Source hashes authenticate the reviewed text; they do not validate +its implementation or any mathematical proposition automatically. + +## Remaining review obligations + +The coNP reduction, general circuit compiler, native composition/inversion +implementation, event8814 adapter and actual caller remain outside this audit. +No physical stock, movement, precision, paid invoice, supplier admission, +selected cold replay or complete multiplication theorem has been checked. +The selected conditional result is unchanged. The two concrete next steps are +an independent Section 6 audit and an actual implementation-to-grammar audit; +neither requires extending this small census. + +Ali Romman retains the general four-width theorem and witness construction. +Jose Manuel's phase-sector and native recipe work, ywz65's binary-stream +affine-basis argument, Chris R's tensor-separation work, and the retained +source authors keep their attribution. Symmetric-form elimination, finite +Fourier inversion and Fourier projectors are classical tools; this package +claims a scoped review and explicit one-axis specialization, not those tools. diff --git a/research/native-cutoff-independent-audit/README.md b/research/native-cutoff-independent-audit/README.md new file mode 100644 index 0000000000..0269df4ad7 --- /dev/null +++ b/research/native-cutoff-independent-audit/README.md @@ -0,0 +1,142 @@ +# Audit the native tensor cutoff and sharpen its one-axis case + +This independently audits the phase-character, affine-separation and residue +arguments in Ali Romman's [PR #5369](https://github.com/CrocSwap/integer-mult-bounds/pull/5369), +Sections 2, 3 and 5. No gap was found under the stated hypotheses. A separate +exact implementation corroborates those implications, and the +[written proof](PROOF.md) gives a **sharp one-axis monomial test at widths +3,4,5,6**. Four tests and maximum width six are necessary; the source's +general sufficient bound gives 6,7,8,9 for this case. + +The added one-axis result distinguishes two questions: realizing every phase +character with a spanning tuple, and faithfulness of the tensor representation. +The former is sufficient but can overestimate the latter. The complete +multiplication kappa and selected frontier are unchanged. + +## Scope and sources + +The [canonical claim and result](https://github.com/CrocSwap/integer-mult-bounds/discussions/5354#discussioncomment-19174027) +answers the [open independent-review handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19153575). +The original `formal-interface-lemma` card is retained in [TASK.json](TASK.json); +the scope is declared changed to this live mathematical audit before +formalization. No Lean build is claimed. + +Base: current canonical main `32890bc5de034ab8fc93ac88ead7279a6a416d04`, +priority revision 7. The predecessor head is +`18354f41de4dc7bfda4692e814cf1d91a6d619ef`. [SOURCES.json](SOURCES.json) +pins its unchanged main-branch proof by Git blob and SHA256, plus the task and +selected-record provenance. The verifier authenticates the proof text on every +run. No predecessor executable, arithmetic library or fixture is imported. +The existing ledger's `partially_reviewed` archival status is not upgraded by +this contribution. + +## Evidence and reproduction + +Python 3.12, standard library only: + +```sh +python -I -W error -B research/native-cutoff-independent-audit/verify.py +python -I -O -W error -B research/native-cutoff-independent-audit/verify.py +python -I -W error -B research/native-cutoff-independent-audit/audit_mutations.py +python -B scripts/research_package.py --package research/native-cutoff-independent-audit +``` + +The complete checker reports `PASS_NATIVE_CUTOFF_INDEPENDENT_AUDIT`; the +mutation driver reports `PASS_NATIVE_CUTOFF_AUDIT_MUTATIONS`. The registered +manifest runs both complete modes and the mutation driver. Section-only runs +are diagnostic and carry a different status. Each complete direct run takes +about five seconds on the local Windows environment. + +[RESULT.json](RESULT.json) contains the identical normal/optimized result: + +- **391,275 multisets**, exhausting all 2,192 phase characters on one, two and + three axes. Reduction of positive multiplicities to 1..4 proves that the + search contains a shortest spanning tuple for every character. This uses a + different method from the predecessor's Gram-factor construction. +- **29,760 literal phase-generator probes**, including the padded tuples in + the published four-width window; **200,378 affine-map restrictions** over + every spanning support in the same domain. +- All **32 one-axis group elements**, with exact Gaussian rational ranks from + **2,044 literal matrix-entry rows** at widths 1..9. The consecutive windows + 1..4, 2..5 and 3..6 have ranks 26, 30 and 32. An explicit residual vanishes + at all positive widths below six and has entry **16** at width six. +- Controls for modulo-four counts, quadratic pair statistics, affine span, + tensor-scaled constant phase, missing central residues and width-dependent + coefficients. + +[MUTATIONS.json](MUTATIONS.json) records **12 expected rejections**: five +mathematical code mutations and a changed proof byte, each tested in normal +and optimized mode in disposable copies. These remove a quadratic phase, +apply the constant only once, omit span, forbid multiplicity four, change the +sharpness projector, or corrupt the reviewed source. Each fails at its named +semantic/hash check. [EVIDENCE.json](EVIDENCE.json) identifies the local runtime. + +The scoped registered replay, committed-byte comparison and whitespace check +pass. The official package exporter includes this package and its single +declared proof input; export integrity and complete normal/optimized direct +replays pass in a Git-free tree. The selected metadata baseline also passes; +that baseline is source-binding orientation, not a selected scientific replay. + +For an exported tree, retain the repository-relative paths above and run the +direct commands. They require neither Git nor network access. Generic metadata +validation still needs the recorded Git objects. Full-history provenance +preflight was not run in this shallow checkout; the base and source are already +on canonical main. Hosted CI is separate from the local evidence. + +## What remains unverified + +The result is a separate agent-assisted proof review and finite exact check, +not independent human review or a formal proof kernel. It does not review +Section 6's coNP reduction, the general compiler or native composition code, +event8814's source adapter, physical cost/stock/precision, or a complete +supplier. No selected cold replay was run. The one-axis result is for the +monomial group; PR5376's larger full Clifford group has a different contract. +The least representation cutoff for n>=2 remains open here. The small +character minima are not asserted to be representation minima. + +## Coordination and overlap + +The initial completed snapshot searched 377 open PR bodies, 4,786 Discussion +records and all 7,402 tracked in-scope local notes, with complete reported +pagination/inventory and no coverage warnings (2026-10-25 06:11 UTC). +The direct canonical thread, central handoff, partially reviewed ledger entry +and the full relevant match set were inspected. PR5441 uses the predecessor's +source recipe for finite-memory lifting; PR5376 treats full Clifford operators. +Neither is this audit. The final refresh at 06:22 UTC covered 378 open PRs, +4,797 Discussion records and all 7,402 tracked base notes (plus this package's +two new notes), again with complete reported coverage and no warnings. Main +and priority revision remained unchanged. + +That refresh found [Hiroki KUMAZAKI's complementary two-axis claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5354#discussioncomment-19174077). +It explicitly takes the n=2 representation-kernel question excluded here. +Our small character table is corroboration, not a competing n=2 cutoff claim. +These searches do not cover arbitrary diffs, all historical versions or +unpublished work, and do not establish novelty. + +## Open next questions + +1. Independently audit Section 6's reversible complexity reduction. Begin with + the dirty controlled swap and permutation convention, then the balanced CNF + size bound and implementation. This closes a separate proof obligation; + it was deliberately left outside this session. +2. Audit the predecessor implementation against the established grammar at an + actual source-bound caller, retaining every dirty input and return. Start + with composition, inversion and self-query semantics. The present abstract + audit and source hash cannot supply that implementation evidence. + +Both questions and their blockers are also in TASK.json. Extending the small +census is not required for either one. + +## Attribution + +Prepared for Mihir Srivastava (@mihir-s-05) with substantial OpenAI Codex +assistance in proof review, implementation, verification and writing; one +agent. Ali Romman retains the general four-width theorem, constructive +witness and package. Jose Manuel's phase-sector and native-recipe work, +ywz65's affine-basis argument, Chris R's finite-alphabet tensor separation, +and the source lineage including Douglas Colkitt, JoyboyBrian and Cinna Davis +retain their credit. The associated interface work of zxv and Krzysztof Wójt +remains credited by the predecessor. Binary symmetric factorization, finite +Fourier inversion and central projectors are classical; no priority for those +tools is claimed. New prose and code are Apache-2.0; [LICENSE](LICENSE) is +included for standalone redistribution. No frozen source was changed. diff --git a/research/native-cutoff-independent-audit/RESULT.json b/research/native-cutoff-independent-audit/RESULT.json new file mode 100644 index 0000000000..217c63ccb1 --- /dev/null +++ b/research/native-cutoff-independent-audit/RESULT.json @@ -0,0 +1,133 @@ +{ + "character_census": [ + { + "affine_maps": 2, + "affine_restrictions": 2, + "axes": 1, + "characters": 16, + "full_span_supports": 1, + "largest_minimum_by_residue": [ + 8, + 5, + 6, + 7 + ], + "literal_generator_probes": 64, + "minima_sha256": "28d469ffe0850a136cea27b9c9625d3f3e64bf16f1b27b205daf389f694343bf", + "minimum_length_histogram": { + "2": 1, + "3": 2, + "4": 3, + "5": 4, + "6": 3, + "7": 2, + "8": 1 + }, + "multisets": 25 + }, + { + "affine_maps": 24, + "affine_restrictions": 120, + "axes": 2, + "characters": 128, + "full_span_supports": 5, + "largest_minimum_by_residue": [ + 8, + 9, + 6, + 7 + ], + "literal_generator_probes": 1024, + "minima_sha256": "8c84a43713968c5901c131f03b610f7c06363ef80db314f01f8ba091250f267d", + "minimum_length_histogram": { + "3": 4, + "4": 13, + "5": 28, + "6": 32, + "7": 28, + "8": 19, + "9": 4 + }, + "multisets": 625 + }, + { + "affine_maps": 1344, + "affine_restrictions": 200256, + "axes": 3, + "characters": 2048, + "full_span_supports": 149, + "largest_minimum_by_residue": [ + 8, + 9, + 10, + 7 + ], + "literal_generator_probes": 28672, + "minima_sha256": "4e43292e3b231f799bc00cffe20face65e4d4ca6144911020b2c8903b095850f", + "minimum_length_histogram": { + "4": 56, + "5": 280, + "6": 476, + "7": 512, + "8": 456, + "9": 232, + "10": 36 + }, + "multisets": 390625 + } + ], + "hypothesis_controls": { + "constant_character_required": true, + "mod_four_not_parity": true, + "nonspanning_affine_collision": true, + "pair_statistic_not_marginals": true, + "tensor_constant_scaled_by_width": true + }, + "one_axis": { + "earliest_complete_consecutive_window": [ + 3, + 4, + 5, + 6 + ], + "group_order": 32, + "least_uniform_stabilization_threshold": 3, + "literal_matrix_entry_rows": 2044, + "ranks": [ + 4, + 6, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "width_2_to_5_trap_width_6_entry": [ + 16, + 0 + ], + "widths": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9 + ], + "window_ranks_by_first_width": { + "1": 26, + "2": 30, + "3": 32, + "6": 32 + } + }, + "proof_sha256": "b2d31ea52b652f43cc8576affde6092a884d2832820221a43933e7e27dc07041", + "section": "all", + "status": "PASS_NATIVE_CUTOFF_INDEPENDENT_AUDIT", + "verifier_sha256": "2f0166a9e0bd0a2e5113f3a6847e8f7e3642a8bf69032a53d7ce72fd21995b7a" +} diff --git a/research/native-cutoff-independent-audit/SOURCES.json b/research/native-cutoff-independent-audit/SOURCES.json new file mode 100644 index 0000000000..224c716abb --- /dev/null +++ b/research/native-cutoff-independent-audit/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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" + }, + { + "path": "research/native-tensor-cutoff/PROOF.md", + "usage": "input", + "git_blob": "2d92f17cd8e1064028656cd4ff06c1d38f14ebc0", + "sha256": "b2d31ea52b652f43cc8576affde6092a884d2832820221a43933e7e27dc07041" + } + ] +} diff --git a/research/native-cutoff-independent-audit/TASK.json b/research/native-cutoff-independent-audit/TASK.json new file mode 100644 index 0000000000..cb1a98920c --- /dev/null +++ b/research/native-cutoff-independent-audit/TASK.json @@ -0,0 +1,103 @@ +{ + "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 PR5369 Sections 2/3/5, complete small phase-character realizations, and the sharp one-axis monomial tensor cutoff.", + "scope_change_reason": "Took the live independent-review handoff in Discussion 5354 before random selection. This audits a mathematical interface before formalization; no Lean build or selected-caller admission is claimed.", + "bottleneck_link": "Native identity checkers are used to support all-column supplier identities. Auditing their finite-width implication reduces a specific verification gap; the one-axis specialization exposes why phase-character span and faithful representation thresholds differ. This does not discharge the selected physical premises.", + "budget_minutes": 60, + "stop_rule": "Stop after Sections 2/3/5, a proved or falsified one-axis threshold, exact n<=3 character controls and a reproducible handoff. Do not expand to higher-dimensional minimum cutoffs, full Clifford operators, Section 6, or physical supplier admission.", + "outcome": "completed", + "evidence": "PROOF.md, RESULT.json, MUTATIONS.json and EVIDENCE.json; source-bound registered normal/optimized replay and committed Git-free export.", + "author": "Mihir Srivastava", + "ai_assistance": "Substantial OpenAI Codex assistance in proof review, implementation, verification and writing; one agent. No independent human or formal-kernel acceptance.", + "open_questions": [ + { + "question": "Does PR5369 Section 6's full reversible complexity reduction satisfy its exact grammar and size bound?", + "why_it_matters": "The complexity claim is a separate unreviewed assertion of the same interface package.", + "first_step": "Audit the five-step controlled swap and balanced CNF construction against the written permutation convention, then compare to reversible_cnf.py.", + "blocked_by": "Not included in this scoped audit; needs its own overlap check and source binding." + }, + { + "question": "Does the native checker implement the audited grammar for every supported instruction and actual source recipe?", + "why_it_matters": "A correct abstract cutoff does not validate the predecessor compiler or its caller adapter.", + "first_step": "Bind composition, inverse, self-query and all dirty returns to one source-pinned word; test against direct basis action.", + "blocked_by": "The present checker deliberately imports no predecessor executable and does not audit event8814 or physical admission." + } + ], + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5354#discussioncomment-19174027", + "predecessor_head": "18354f41de4dc7bfda4692e814cf1d91a6d619ef" +} diff --git a/research/native-cutoff-independent-audit/VERIFY.json b/research/native-cutoff-independent-audit/VERIFY.json new file mode 100644 index 0000000000..3b42a8a8a0 --- /dev/null +++ b/research/native-cutoff-independent-audit/VERIFY.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/native-tensor-cutoff/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "Exact n<=3 phase-character minima and affine separation; literal one-axis ranks and hypothesis controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "The same complete audit with assertions disabled." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/audit_mutations.py" + ], + "timeout_seconds": 90, + "checks": "Five mathematical code mutations and a proof-byte mutation rejected in both modes." + } + ] +} diff --git a/research/native-cutoff-independent-audit/audit_mutations.py b/research/native-cutoff-independent-audit/audit_mutations.py new file mode 100644 index 0000000000..69cf1450b3 --- /dev/null +++ b/research/native-cutoff-independent-audit/audit_mutations.py @@ -0,0 +1,68 @@ +#!/usr/bin/env python3 +"""Reject deliberate regressions in disposable copies; no source tree edits. + +Mihir Srivastava, with substantial OpenAI Codex assistance. Apache-2.0. +""" +from hashlib import sha256 +import json +from pathlib import Path +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +PROOF = "research/native-tensor-cutoff/PROOF.md" +VERIFIER = "research/native-cutoff-independent-audit/verify.py" +MUTATIONS = ( + ("erase_quadratic_phase", "characters", + "answer += 2 * b *", "answer += 0 * b *", "literal phase mismatch"), + ("tensor_constant_once", "one-axis", + "sum(phase(x, c, [a], []) for x in bits) % 4", + "(c + sum(phase(x, 0, [a], []) for x in bits)) % 4", "one-axis window rank failed"), + ("omit_span_condition", "characters", + "if mask not in full:", "if False:", "padding changed character or span"), + ("forbid_multiplicity_four", "characters", + "product(range(5), repeat=size)", "product(range(4), repeat=size)", "missing phase character"), + ("wrong_weight_projector", "one-axis", + "(-2 * c - 3 * a) % 4", "(-2 * c - 2 * a) % 4", "sharpness trap did not vanish"), +) + + +def main(): + source = (ROOT / VERIFIER).read_text(encoding="utf-8") + proof = (ROOT / PROOF).read_bytes() + records = [] + with tempfile.TemporaryDirectory(prefix="native-cutoff-audit-") as temporary: + root = Path(temporary) + script = root / VERIFIER + pinned = root / PROOF + script.parent.mkdir(parents=True) + pinned.parent.mkdir(parents=True) + for optimized in (False, True): + for name, section, old, new, expected in (*MUTATIONS, + ("changed_source_proof", "controls", None, None, "source proof hash mismatch")): + if old is not None: + if source.count(old) != 1: + raise ValueError("mutation target is not unique: " + name) + changed = source.replace(old, new) + else: + changed = source + script.write_text(changed, encoding="utf-8", newline="\n") + pinned.write_bytes(proof + (b"\nchanged\n" if old is None else b"")) + command = [sys.executable, "-I", *(["-O"] if optimized else []), + "-W", "error", "-B", str(script), "--section", section] + result = subprocess.run(command, cwd=root, capture_output=True, + text=True, encoding="utf-8", timeout=30) + if result.returncode == 0 or expected not in result.stderr or result.stdout: + raise ValueError(f"mutation did not fail as expected: {name}: {result}") + records.append({"mutation": name, "optimized": optimized, + "exit_code": result.returncode, "expected_rejection": expected}) + print(json.dumps({"status": "PASS_NATIVE_CUTOFF_AUDIT_MUTATIONS", + "verifier_sha256": sha256((ROOT / VERIFIER).read_bytes()).hexdigest(), + "mutation_driver_sha256": sha256(Path(__file__).read_bytes()).hexdigest(), + "records": records}, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/native-cutoff-independent-audit/verify.py b/research/native-cutoff-independent-audit/verify.py new file mode 100644 index 0000000000..5e18b0101f --- /dev/null +++ b/research/native-cutoff-independent-audit/verify.py @@ -0,0 +1,287 @@ +#!/usr/bin/env python3 +"""Independent finite checks for the scoped PR5369 proof audit. + +Mihir Srivastava, with substantial OpenAI Codex assistance. Apache-2.0. +No predecessor executable or arithmetic module is imported. All arithmetic is exact. +""" +import argparse +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +SOURCE = "research/native-tensor-cutoff/PROOF.md" +SOURCE_SHA = "b2d31ea52b652f43cc8576affde6092a884d2832820221a43933e7e27dc07041" +UNITS = ((1, 0), (0, 1), (-1, 0), (0, -1)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def source_check(): + require(sha256((ROOT / SOURCE).read_bytes()).hexdigest() == SOURCE_SHA, + "source proof hash mismatch") + + +def binary_rank(vectors): + pivots = {} + for value in vectors: + while value: + bit = value.bit_length() - 1 + if bit not in pivots: + pivots[bit] = value + break + value ^= pivots[bit] + return len(pivots) + + +def spanning(points, n): + return bool(points) and binary_rank([x ^ points[0] for x in points]) == n + + +def phase(x, c, linear, pairs): + answer = c + for j, a in enumerate(linear): + answer += a * ((x >> j) & 1) + for j, k, b in pairs: + answer += 2 * b * ((x >> j) & 1) * ((x >> k) & 1) + return answer % 4 + + +def literal_character(points, n): + # Evaluate actual phase generators point by point, without the count formula. + generators = [(1, [0] * n, [])] + for j in range(n): + linear = [0] * n + linear[j] = 1 + generators.append((0, linear, [])) + for j in range(n): + for k in range(j + 1, n): + generators.append((0, [0] * n, [(j, k, 1)])) + values = [sum(phase(x, *g) for x in points) % 4 for g in generators] + require(all(v % 2 == 0 for v in values[n + 1:]), "pair phase parity") + return tuple(values[:n + 1] + [v // 2 for v in values[n + 1:]]) + + +def count_character(counts, n): + r = sum(counts) % 4 + u = [sum(counts[x] for x in range(1 << n) if x & (1 << j)) % 4 + for j in range(n)] + v = [sum(counts[x] for x in range(1 << n) + if x & (1 << j) and x & (1 << k)) % 2 + for j in range(n) for k in range(j + 1, n)] + return (r, *u, *v) + + +def affine_maps(n): + result = [] + for rows in product(range(1 << n), repeat=n): + if binary_rank(rows) != n: + continue + for offset in range(1 << n): + result.append(tuple(offset ^ sum(((row & x).bit_count() % 2) << j + for j, row in enumerate(rows)) + for x in range(1 << n))) + return result + + +def character_census(): + reports = [] + for n in (1, 2, 3): + size = 1 << n + support_points = {mask: tuple(x for x in range(size) if mask & (1 << x)) + for mask in range(1 << size)} + full = {mask for mask, points in support_points.items() if spanning(points, n)} + minima, witnesses = {}, {} + visited = 0 + # Reducing each positive multiplicity to 1+((m-1) mod 4) preserves + # character and support and cannot increase length. This finite domain + # therefore contains a shortest spanning tuple for EACH character. + for counts in product(range(5), repeat=size): + visited += 1 + mask = sum(1 << x for x, count in enumerate(counts) if count) + if mask not in full: + continue + key = count_character(counts, n) + length = sum(counts) + if key not in minima or length < minima[key]: + minima[key], witnesses[key] = length, counts + expected_keys = set(product(*([range(4)] * (n + 1) + + [range(2)] * (n * (n - 1) // 2)))) + require(set(minima) == expected_keys, "missing phase character") + literal_probes = 0 + for key, counts in witnesses.items(): + points = tuple(x for x, count in enumerate(counts) for _ in range(count)) + require(literal_character(points, n) == key, "literal phase mismatch") + F = 2 * n + 4 + f = F + (key[0] - F) % 4 + require(len(points) <= f, "published four-width bound failed") + padded = points + (0,) * (f - len(points)) + require(spanning(padded, n) and literal_character(padded, n) == key, + "padding changed character or span") + literal_probes += 2 * (1 + n + n * (n - 1) // 2) + maps = affine_maps(n) + require(len(maps) == {1: 2, 2: 24, 3: 1344}[n], "affine group inventory") + # Test isolation on every full-span support, not only a canonical basis. + for mask in full: + points = support_points[mask] + require(len({tuple(mapping[x] for x in points) for mapping in maps}) == len(maps), + "affine maps collide on a spanning support") + table = [[list(key), minima[key]] for key in sorted(minima)] + reports.append({ + "axes": n, "multisets": visited, "characters": len(minima), + "full_span_supports": len(full), "affine_maps": len(maps), + "affine_restrictions": len(full) * len(maps), + "literal_generator_probes": literal_probes, + "largest_minimum_by_residue": [max(length for key, length in minima.items() + if key[0] == r) for r in range(4)], + "minimum_length_histogram": dict(sorted(Counter(minima.values()).items())), + "minima_sha256": sha256(json.dumps(table, separators=(",", ":")).encode()).hexdigest(), + }) + return reports + + +def add(z, w): + return (z[0] + w[0], z[1] + w[1]) + + +def mul(z, w): + return (z[0] * w[0] - z[1] * w[1], z[0] * w[1] + z[1] * w[0]) + + +def divide(z, w): + den = w[0] * w[0] + w[1] * w[1] + return (Fraction(z[0] * w[0] + z[1] * w[1], den), + Fraction(z[1] * w[0] - z[0] * w[1], den)) + + +def gaussian_rank(rows): + pivots = {} + for raw in rows: + row = list(raw) + for col in range(len(row)): + if row[col] == (0, 0): + continue + if col not in pivots: + pivot = row[col] + pivots[col] = [divide(value, pivot) for value in row] + break + factor = row[col] + row = [add(value, mul((-factor[0], -factor[1]), old)) + for value, old in zip(row, pivots[col])] + return len(pivots) + + +ONE_AXIS_GROUP = tuple(product(range(2), range(4), range(4))) # t,c,a + + +def operator_rows(f): + require(f >= 1, "positive width required") + rows = [] + # Literal entries of all operators; only identically zero rows are omitted. + # No Hamming-weight or theoretical rank formula is used here. + for bits in product(range(2), repeat=f): + outputs = {} + for index, (t, c, a) in enumerate(ONE_AXIS_GROUP): + y = tuple(x ^ t for x in bits) + exponent = sum(phase(x, c, [a], []) for x in bits) % 4 + outputs.setdefault(y, [(0, 0)] * len(ONE_AXIS_GROUP))[index] = UNITS[exponent] + rows.extend(tuple(row) for row in outputs.values()) + return rows + + +def dot(row, coefficients): + answer = (0, 0) + for x, y in zip(row, coefficients): + answer = add(answer, mul(x, y)) + return answer + + +def one_axis(): + ranks, raw_counts, distinct = [], [], {} + for f in range(1, 10): + rows = operator_rows(f) + raw_counts.append(len(rows)) + distinct[f] = sorted(set(rows)) + rank = gaussian_rank(distinct[f]) + require(rank == 2 * min(f + 1, 4), "one-axis rank formula failed") + ranks.append(rank) + windows = {} + for first, expected in ((1, 26), (2, 30), (3, 32), (6, 32)): + rows = [row for f in range(first, first + 4) for row in distinct[f]] + windows[str(first)] = gaussian_rank(rows) + require(windows[str(first)] == expected, "one-axis window rank failed") + # C_2 times the weight-three projector (unnormalized): missed by widths 2..5. + trap = [UNITS[(-2 * c - 3 * a) % 4] if t == 0 else (0, 0) + for t, c, a in ONE_AXIS_GROUP] + require(all(dot(row, trap) == (0, 0) for f in range(1, 6) for row in distinct[f]), + "sharpness trap did not vanish") + require(any(dot(row, trap) == (16, 0) for row in distinct[6]), + "sharpness trap missing width-six witness") + # Each central residue is necessary, even at large widths. + for r in range(4): + projector = [UNITS[(-r * c) % 4] if t == 0 and a == 0 else (0, 0) + for t, c, a in ONE_AXIS_GROUP] + for f in range(3, 7): + values = {dot(row, projector) for row in distinct[f]} + require(((4, 0) in values) == (f % 4 == r), "central residue control failed") + if f % 4 != r: + require(values == {(0, 0)}, "central projector leaked into another residue") + # A DIFFERENT residual at each f can vanish despite nonzero coefficients. + for f in range(3, 7): + residual = [(0, 0)] * 32 + residual[ONE_AXIS_GROUP.index((0, 1, 0))] = (1, 0) + residual[ONE_AXIS_GROUP.index((0, 0, 0))] = tuple(-x for x in UNITS[f % 4]) + require(any(z != (0, 0) for z in residual) + and all(dot(row, residual) == (0, 0) for row in distinct[f]), + "width-dependent-program control failed") + return {"group_order": 32, "widths": list(range(1, 10)), "ranks": ranks, + "literal_matrix_entry_rows": sum(raw_counts), "window_ranks_by_first_width": windows, + "earliest_complete_consecutive_window": [3, 4, 5, 6], + "width_2_to_5_trap_width_6_entry": [16, 0], + "least_uniform_stabilization_threshold": 3} + + +def hypothesis_controls(): + require(literal_character((1, 1), 1) == (2, 2), "mod-four repair control") + X, Y = (0, 3, 0, 1, 2), (1, 2, 0, 1, 2) + left, right = literal_character(X, 2), literal_character(Y, 2) + require(spanning(X, 2) and spanning(Y, 2), "pair control span") + require(left[:3] == right[:3] and left[3] != right[3], "pair statistic control") + identity, shear = (0, 1, 2, 3), (0, 1, 3, 2) + require(identity[:2] == shear[:2] and identity != shear, "affine span control") + require(literal_character((0, 1), 1) != literal_character((0, 1, 0), 1), + "constant phase control") + require(sum(phase(x, 1, [0], []) for x in (0, 1)) % 4 == 2, + "tensor constant must be multiplied by width") + return {"mod_four_not_parity": True, "pair_statistic_not_marginals": True, + "nonspanning_affine_collision": True, "constant_character_required": True, + "tensor_constant_scaled_by_width": True} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--section", choices=("all", "characters", "one-axis", "controls"), default="all") + args = parser.parse_args() + source_check() + status = ("PASS_NATIVE_CUTOFF_INDEPENDENT_AUDIT" if args.section == "all" + else "PASS_NATIVE_CUTOFF_AUDIT_SECTION") + report = {"status": status, "section": args.section, + "proof_sha256": SOURCE_SHA, "verifier_sha256": sha256(Path(__file__).read_bytes()).hexdigest()} + if args.section in ("all", "characters"): + report["character_census"] = character_census() + if args.section in ("all", "one-axis"): + report["one_axis"] = one_axis() + if args.section in ("all", "controls"): + report["hypothesis_controls"] = hypothesis_controls() + print(json.dumps(report, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() From 5fe6693dd023cedddb0972f1006d7fa50ba94595 Mon Sep 17 00:00:00 2001 From: Mihir Srivastava Date: Sat, 24 Oct 2026 23:27:05 -0700 Subject: [PATCH 2/2] Record standalone native cutoff audit validation --- .../EVIDENCE.json | 24 ++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/research/native-cutoff-independent-audit/EVIDENCE.json b/research/native-cutoff-independent-audit/EVIDENCE.json index 22cfbb211b..a043d692d3 100644 --- a/research/native-cutoff-independent-audit/EVIDENCE.json +++ b/research/native-cutoff-independent-audit/EVIDENCE.json @@ -3,5 +3,27 @@ "platform": "Windows-11-10.0.26300-SP0", "normal_optimized_identical": true, "source_base": "32890bc5de034ab8fc93ac88ead7279a6a416d04", - "scope": "Local native Windows execution. Registered replay and export evidence are reported in README.md. Finite controls are not a proof kernel." + "scope": "Local native Windows execution. Registered replay and export evidence are reported in README.md. Finite controls are not a proof kernel.", + "registered_replay": "PASS_REGISTERED_RESEARCH_PACKAGE", + "export_validation": { + "status": "PASS_READONLY_GIT_FREE_NATIVE_AUDIT_EXPORT", + "file_count": 13, + "empty_path": true, + "git_directory_present": false, + "checks": [ + { + "optimized": false, + "result_equals_committed_receipt": true + }, + { + "optimized": true, + "result_equals_committed_receipt": true + } + ], + "all_12_mutations_match": true, + "all_file_hashes_unchanged": true, + "verifier_sha256": "2f0166a9e0bd0a2e5113f3a6847e8f7e3642a8bf69032a53d7ce72fd21995b7a" + }, + "publication_bytes": "All 12 package/input files matched the committed bytes before export", + "selected_metadata_baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY" }