From 8fc6f31851f897acbddabe70db219889e8a3068f Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Tue, 13 Oct 2026 04:51:01 -0700 Subject: [PATCH 1/2] Add independent exhaustive binary residual and phase-interface audit Prepared for ToikY with substantial OpenAI Codex assistance. Finite evidence; no new kappa. --- .../binary-residual-exhaustive/CLAIM.json | 22 ++ .../binary-residual-exhaustive/EXPECTED.json | 157 ++++++++++ research/binary-residual-exhaustive/NOTICE.md | 32 +++ research/binary-residual-exhaustive/PROOF.md | 91 ++++++ research/binary-residual-exhaustive/README.md | 101 +++++++ .../binary-residual-exhaustive/SOURCES.json | 49 ++++ .../VALIDATION.json | 53 ++++ research/binary-residual-exhaustive/oracle.py | 188 ++++++++++++ .../binary-residual-exhaustive/test_verify.py | 155 ++++++++++ research/binary-residual-exhaustive/verify.py | 269 ++++++++++++++++++ 10 files changed, 1117 insertions(+) create mode 100644 research/binary-residual-exhaustive/CLAIM.json create mode 100644 research/binary-residual-exhaustive/EXPECTED.json create mode 100644 research/binary-residual-exhaustive/NOTICE.md create mode 100644 research/binary-residual-exhaustive/PROOF.md create mode 100644 research/binary-residual-exhaustive/README.md create mode 100644 research/binary-residual-exhaustive/SOURCES.json create mode 100644 research/binary-residual-exhaustive/VALIDATION.json create mode 100644 research/binary-residual-exhaustive/oracle.py create mode 100644 research/binary-residual-exhaustive/test_verify.py create mode 100644 research/binary-residual-exhaustive/verify.py diff --git a/research/binary-residual-exhaustive/CLAIM.json b/research/binary-residual-exhaustive/CLAIM.json new file mode 100644 index 0000000000..b500359c0d --- /dev/null +++ b/research/binary-residual-exhaustive/CLAIM.json @@ -0,0 +1,22 @@ +{ + "track": "Independent verification or formalization", + "assignment_seed": 83, + "seed_origin": "Python secrets.randbelow(100), backed by operating-system randomness", + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "claimed_at_utc": "2026-10-13T11:34:00Z", + "expected_finish_utc": "2026-10-13T12:00:00Z", + "coordination": "No sprint coordination issue found: open-issue inventory contains only issue 650, requesting Discussions. Claim recorded locally; no reservation issue opened.", + "candidates": [ + "Exhaustive independent vector-set check of binary residual classification, characteristic-vector acceptance, and orthonormal outputs through ambient dimension six", + "Independent reconstruction of the historical ternary central-plus-side coefficient partition", + "Independent quadratic-phase certificate for a historical wrapper" + ], + "chosen_object": "scripts/binary_phase_frames.py residual/orthonormal_basis and scripts/experiments/parity_phase_repair.py characteristic criterion", + "method": "Enumerate every F2 subspace for ambient dimensions 0 through 6 by full vector-set closure; compute radicals, characteristic vectors, residuals and output spans by direct pairings. Compare predecessor outputs without using predecessor elimination as the oracle.", + "seed_diversification": "Seed 83 selects ambient cap 6 (5 + seed mod 2) and fixes shuffled presentation of independent generators. Coverage remains exhaustive, not sampled.", + "stopping_rule": "Complete the declared finite domain once, stop at dimension six; reserve the final quarter of the 30-minute session for verification and handoff.", + "overlap": "All-state targeted PR searches inspected binary_phase_frames, orthonormal, nonalternating and alternating residual. PR771 enumerates full-space isometry bases and invoices; PR831 studies F4 phase interfaces; PR712 checks one cold wrapper. None supplies the all-subspace/nested-pair residual census proposed here. No pending PR supplies code or inputs.", + "expected_deliverable": "One standalone independent-verification package with exact census, source pins, corruption controls and written scope; no new kappa and no frontier edits.", + "delegation": "One worker owns only the independent vector-set oracle; one worker performs a read-only mathematical review. Both stay within this claim.", + "status": "CLAIMED" +} diff --git a/research/binary-residual-exhaustive/EXPECTED.json b/research/binary-residual-exhaustive/EXPECTED.json new file mode 100644 index 0000000000..9b3c4bb0c7 --- /dev/null +++ b/research/binary-residual-exhaustive/EXPECTED.json @@ -0,0 +1,157 @@ +{ + "status": "PASS_BINARY_RESIDUAL_EXHAUSTIVE", + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "assignment_seed": 83, + "ambient_cap": 6, + "source_assertions": "Explicit compile(optimize=0); unchanged predecessor source", + "coverage": [ + { + "ambient_dimension": 0, + "subspaces_by_dimension": [ + 1 + ], + "subspaces": 1, + "nondegenerate_subspaces": 1, + "accepted_basis_presentations": 2, + "admissible_pairs": 1, + "characteristic_presentations": 2, + "classified_presentations": 2, + "nested_pairs": 1, + "phase_inputs": 1, + "zero_residual_pairs": 1 + }, + { + "ambient_dimension": 1, + "subspaces_by_dimension": [ + 1, + 1 + ], + "subspaces": 2, + "nondegenerate_subspaces": 2, + "accepted_basis_presentations": 4, + "admissible_pairs": 3, + "characteristic_presentations": 4, + "classified_presentations": 4, + "nested_pairs": 3, + "phase_inputs": 6, + "zero_residual_pairs": 2 + }, + { + "ambient_dimension": 2, + "subspaces_by_dimension": [ + 1, + 3, + 1 + ], + "subspaces": 5, + "nondegenerate_subspaces": 4, + "accepted_basis_presentations": 8, + "admissible_pairs": 9, + "characteristic_presentations": 8, + "classified_presentations": 10, + "nested_pairs": 9, + "phase_inputs": 36, + "rejected_basis_presentations": 2, + "zero_residual_pairs": 4 + }, + { + "ambient_dimension": 3, + "subspaces_by_dimension": [ + 1, + 7, + 7, + 1 + ], + "subspaces": 16, + "nondegenerate_subspaces": 10, + "accepted_basis_presentations": 18, + "admissible_pairs": 31, + "characteristic_presentations": 20, + "classified_presentations": 32, + "nested_pairs": 33, + "nonzero_alternating_pairs": 2, + "phase_inputs": 248, + "rejected_basis_presentations": 14, + "zero_residual_pairs": 10 + }, + { + "ambient_dimension": 4, + "subspaces_by_dimension": [ + 1, + 15, + 35, + 15, + 1 + ], + "subspaces": 67, + "nondegenerate_subspaces": 38, + "accepted_basis_presentations": 68, + "admissible_pairs": 191, + "characteristic_presentations": 76, + "classified_presentations": 134, + "nested_pairs": 207, + "nonzero_alternating_pairs": 16, + "phase_inputs": 3056, + "rejected_basis_presentations": 66, + "zero_residual_pairs": 38 + }, + { + "ambient_dimension": 5, + "subspaces_by_dimension": [ + 1, + 31, + 155, + 155, + 31, + 1 + ], + "subspaces": 374, + "nondegenerate_subspaces": 194, + "accepted_basis_presentations": 346, + "admissible_pairs": 1697, + "characteristic_presentations": 388, + "classified_presentations": 748, + "nested_pairs": 1899, + "nonzero_alternating_pairs": 202, + "phase_inputs": 54304, + "rejected_basis_presentations": 402, + "zero_residual_pairs": 194 + }, + { + "ambient_dimension": 6, + "subspaces_by_dimension": [ + 1, + 63, + 651, + 1395, + 651, + 63, + 1 + ], + "subspaces": 2825, + "nondegenerate_subspaces": 1378, + "accepted_basis_presentations": 2564, + "admissible_pairs": 24643, + "characteristic_presentations": 2756, + "classified_presentations": 5650, + "nested_pairs": 27747, + "nonzero_alternating_pairs": 3104, + "phase_inputs": 1577152, + "rejected_basis_presentations": 3086, + "zero_residual_pairs": 1378 + } + ], + "controls": { + "nonzero_alternating_rejected": true, + "degenerate_lower_rejected": true, + "degenerate_upper_rejected": true, + "nonnested_rejected": true, + "degenerate_characteristic_rejected": true, + "nonorthogonal_unit_basis_rejected": true, + "zero_residual_at_alternating_endpoints_accepted": true, + "unit_phase_weight_substitution_detected": true, + "reverse_phase_sign_substitution_detected": true, + "same_rank_wrong_span_detected": true + }, + "scope": "Exhaustive finite evidence only; historical binary residual interface, no new kappa" +} diff --git a/research/binary-residual-exhaustive/NOTICE.md b/research/binary-residual-exhaustive/NOTICE.md new file mode 100644 index 0000000000..93f7aeed81 --- /dev/null +++ b/research/binary-residual-exhaustive/NOTICE.md @@ -0,0 +1,32 @@ +# License, predecessor credit and assistance + +New files in this package are contributed under the repository's Apache-2.0 +license. Existing source files and their notices are unchanged. + +Credit **Douglas R. Colkitt** for `scripts/binary_phase_frames.py`, the +historical complex-network compiler, parity-side repair, tests and documentation. +The source histories identify `1c09a5887e3f900798eef904371441ab18c057de` for the +binary-frame module and `d55bcd62ceb8f322bcf311a5a66e94c3ac7724f0` for the +preserved parity repair. The exact execution pins are the blobs at base +`f567884aeb8851b6e794af1184119a3bfbe1e631`, listed in SOURCES.json. + +Credit **OpenAI's September 23, 2026 integer-multiplication manuscript** for the +retained binary orthonormal absorption and phase identities. Its pinned source, +license and attribution remain in `upstream/`. The characteristic-vector test +is already stated in the historical parity-side note; this contribution adds +independent finite evidence rather than claiming the criterion as new. + +The context selection credits **Jeremy Kothe (PR799)**, **Chafik Boukhalfa +(PR741)**, **DreamingOfClouds (PR589)** and **eumemic (PR555)**, together with +icekylinx, Rohan Arun and the retained predecessors identified in its review. +No selected construction or pending-PR implementation is imported here. +**Sricharan Vagvala's PR771** supplies related but distinct full-space isometry +and invoice evidence; **PR831** addresses F4 alternating phase interfaces; +**PR712** checks a specific cold-wrapper phase. Their work is credited for +overlap context, without asserting incorporation or complete approval. + +Prepared for **ToikY** with substantial **OpenAI Codex assistance** in task +selection, mathematical reasoning, implementation, tests and documentation. +A separate AI worker implemented the independent vector-set oracle and another +performed a scoped mathematical/code review. This is code-disjoint evidence, +not a claim of independent human peer review or a formal theorem audit. diff --git a/research/binary-residual-exhaustive/PROOF.md b/research/binary-residual-exhaustive/PROOF.md new file mode 100644 index 0000000000..b09f871314 --- /dev/null +++ b/research/binary-residual-exhaustive/PROOF.md @@ -0,0 +1,91 @@ +# Precise obligations and independent finite evidence + +Let F = F₂ⁿ with the standard symmetric bilinear form B. The endpoint frames +A ⊆ U must both be nondegenerate. Define R = U ∩ A⊥. The source obligations are +`residual`, `classify`, and `orthonormal_basis` in `scripts/binary_phase_frames.py`, +and `characteristic` and its membership test in +`scripts/experiments/parity_phase_repair.py`. The retained manuscript supplies +the orthonormal absorption and signed weight-phase arguments in +`upstream/build/sections/03-motifs.tex`. Exact source bytes are in SOURCES.json. + +## Orthogonal residual and characteristic test + +Nondegeneracy of A gives U = A ⊥ R, and nondegeneracy of U implies that R is +nondegenerate. Thus dim R = dim U − dim A. The map d(v) = B(v,v) is F₂-linear: +the two cross terms in d(v+w) cancel. Nondegeneracy identifies U with its dual, +so there is a unique w_U ∈ U satisfying B(w_U,v) = d(v) for every v ∈ U. + +The orthogonal decomposition gives w_U = w_A + w_R. Therefore R is alternating +exactly when d restricted to R vanishes, equivalently w_R = 0, equivalently +**w_U ∈ A**. This includes R = 0: the zero form is alternating and nondegenerate, +and its empty orthonormal basis is admissible. The compiler rejects only +**nonzero** alternating residuals. It cannot replace the criterion with a test +of B(w_U,w_U): in full F₂², w_U = 3 is isotropic but the space is nonalternating. + +The oracle computes R by filtering every vector of U against every vector of A. +It computes the radical directly and searches all w ∈ U for the characteristic +equations. These calculations do not use the subject's Gram elimination. + +## Orthonormal basis obligation + +An orthonormal basis has identity Gram matrix, so a nonzero space admitting one +is nondegenerate and nonalternating. Conversely, split off unit lines until the +remaining nondegenerate space is alternating. Such a remainder splits into +hyperbolic planes with B(a,a)=B(b,b)=0 and B(a,b)=1. One prior unit line w, +orthogonal to a plane, absorbs it via + + w+a, w+b, w+a+b. + +These vectors are independent and have Gram matrix I₃. Retain one of them to +absorb the next plane. This proves sufficiency in every finite dimension. The +checker independently validates each returned vector, the complete output span +and every Gram entry; it does not regard a reported dimension as enough. + +## Signed phase obligation + +For q(y) = wt(y) modulo four, binary addition satisfies + + wt(z+w) = wt(z) + wt(w) − 2|supp(z) ∩ supp(w)|. + +If B(z,w)=0, the intersection size is even, hence q is additive on that +orthogonal sum. Orthogonal projection exists and is unique for a nondegenerate +space, including an alternating endpoint. If v_i is an orthonormal basis of R, + + P_U x = P_A x + P_R x, + P_R x = sum_i [B(v_i,x)] v_i, + q(P_U x) − q(P_A x) = sum_i wt(v_i)[B(v_i,x)] mod 4. + +The reverse edge negates the last expression. Each wt(v_i) is odd; its residue +may be 1 or 3, so replacing every coefficient with +1 is incorrect. The oracle +finds P_U x and P_A x by testing all candidate projected vectors for the required +pairings, independently of the subject's returned orthonormal basis. + +Concrete controls: U=F₂³, A=span(7) has rejected residual span(3,5). +The opposite pair A=span(3,5), U=F₂³ has admissible residual span(7). +At U=span(7), A=0, x=1, the phase is 3; substituting +1 or reversing the edge +incorrectly gives 1. The independent unit basis (1,2,7) of F₂³ is not mutually +orthogonal and gives an incorrect phase at x=1. Equal alternating endpoints +have a valid zero residual. Degenerate and nonnested endpoints violate explicit +preconditions and are tested separately. + +## Completeness of the declared domain + +Begin at {0}. For each enumerated space S and each v outside it, enumerate the +full extension S ∪ (v+S), then deduplicate by vector-set equality. Every +(k+1)-space has a k-dimensional subspace and an outside vector, so induction +covers every subspace, without relying on row-reduction correctness. Counting +by dimension is checked against the independent recurrence + + [n,k]₂ = [n−1,k−1]₂ + 2^k [n−1,k]₂. + +Every pair of enumerated nondegenerate spaces is inspected for A ⊆ U. Every +admissible residual is checked at all 2ⁿ ambient inputs, in both directions. +The cap is six and the stopping rule is completion of this domain once; no +sampling or larger-domain exclusion is claimed. The seed changes input +presentation, not which subspaces or endpoint pairs are covered. + +The written arguments above explain the encoded obligations. The finite +certificate checks their implementation through n=6; it is not formal proof of +the all-size compiler, physical hosting, scalar circuits, tape/precision bounds, +analytic transfer or complete multiplication theorem. Later interfaces that +permit alternating kernels have a different scope. No new κ is inferred. diff --git a/research/binary-residual-exhaustive/README.md b/research/binary-residual-exhaustive/README.md new file mode 100644 index 0000000000..8ae0a21c11 --- /dev/null +++ b/research/binary-residual-exhaustive/README.md @@ -0,0 +1,101 @@ +# Exhaustive binary residual and phase-interface verification + +**Independent finite verification; no new κ.** For the historical binary-frame +compiler and parity-side repair, a vector-set oracle checks all subspaces of +F₂ⁿ for **0 ≤ n ≤ 6**, all nondegenerate nested endpoint pairs, the exact +residual span, characteristic-vector criterion, and returned orthonormal bases. +For every admissible pair it checks the signed Hamming-weight phase identity on +every ambient input. No predecessor arithmetic is used as the oracle. + +The exact base is `f567884aeb8851b6e794af1184119a3bfbe1e631`. The selected +conditional saving at that base remains `1661634653669567/10^18`; the selected +certificate, construction and maintainer review are pinned as context, not +replayed by this package. `upstream/` and all existing sources are unchanged. + +## Reproduce + +From the repository root, with **Python 3.10+**, standard library only: + +```sh +python3 -I -B research/binary-residual-exhaustive/verify.py +python3 -I -B research/binary-residual-exhaustive/test_verify.py +``` + +Expected main output: + +```text +PASS_BINARY_RESIDUAL_EXHAUSTIVE subspaces=3290 nested_pairs=29899 phase_inputs=1634803 controls=10 kappa=unchanged +``` + +The seven test groups also run under `-I -O -B`. The predecessor's assertion +preconditions are preserved by compiling its unchanged pinned source with +`optimize=0`, even when the independent checker runs under `-O`. This does not +assert that running the historical modules directly under `-O` is supported. +The independent checks use explicit exceptions, not assertions. + +`--output /tmp/binary-residual-result.json` optionally writes the verified +receipt to a **new** file. It refuses to overwrite an existing output and never +writes on a failed source or receipt check. Default execution changes no files. + +## Completed coverage + +| Ambient n | All subspaces | Nondegenerate nested pairs | Nonzero alternating residuals | Admissible phase inputs | +|---:|---:|---:|---:|---:| +| 0 | 1 | 1 | 0 | 1 | +| 1 | 2 | 3 | 0 | 6 | +| 2 | 5 | 9 | 0 | 36 | +| 3 | 16 | 33 | 2 | 248 | +| 4 | 67 | 207 | 16 | 3,056 | +| 5 | 374 | 1,899 | 202 | 54,304 | +| 6 | 2,825 | 27,747 | 3,104 | 1,577,152 | +| **Total** | **3,290** | **29,899** | **3,324** | **1,634,803** | + +Each space is presented twice: a canonical greedy set basis and its complete +vector list shuffled by seed 83, including zero and redundant generators. +The checker validates **6,580** classifications, **3,254** characteristic-vector +presentations and **3,010** accepted basis presentations; **3,570** inadmissible +presentations are rejected. All **1,627** equal nondegenerate endpoint pairs +correctly admit a zero residual, including alternating endpoints. + +The enumerator adjoins every outside vector and deduplicates the resulting full +vector sets. Its dimension census matches the independent Gaussian-binomial +integer recurrence. A second, powerset-based test examines all 32,768 subsets +of the 15 nonzero vectors of F₂⁴ and recovers precisely the same 67 subspaces. +[EXPECTED.json](EXPECTED.json) freezes the full typed receipt; +[SOURCES.json](SOURCES.json) binds every predecessor executable input and cited proof/context file +by SHA256 and its exact base Git blob. Runtime does not require Git or network. + +## What the result adds + +The predecessor tests cover selected frame examples and one characteristic +example. This package covers every embedded subspace and nested nondegenerate +pair in the declared finite domain, including degenerate spaces, nonzero +alternating residuals, alternating endpoints and basis-presentation changes. +The direct radical, characteristic and projector calculations use coordinate +pairings and full vector sets, with no row elimination or predecessor imports. + +Ten explicit controls distinguish rank from exact span, unit norms from mutual +orthogonality, weight-three phases from unit phases, and increasing from +decreasing edges. Test mutations also replace each of the classification, +characteristic, residual and orthonormal-output functions with faulty versions; +the checker detects them. Source drift, missing inputs, digest drift, incomplete +inventories, receipt-value/type corruption and failed-output preservation are +tested. The optimized minimal-closure replay runs in a path containing spaces. + +[PROOF.md](PROOF.md) gives the mathematical dependencies and explains why the +criterion applies in all dimensions; that written argument is separate from +the finite replay and is not a Lean proof. No source defect was found in this +domain. This is neither a frame-search optimum nor an alternative kernel for +alternating residuals, and it does not validate the complete historical repair +cost, a selected supplier, a whole multiplication machine, or any new bound. +All inherited all-size/compiler, realization, hosting, precision/tape and +analytic assumptions remain. + +The OS-random assignment seed is **83** (independent verification track). +[CLAIM.json](CLAIM.json) records the three candidates, local coordination claim, +domain, stopping rule and overlap check. PR771 checks full-space isometry-group +orders and invoices; PR831 studies F4 alternating phase interfaces; PR712 +checks a single cold-wrapper phase certificate. This all-subspace residual +census is distinct and consumes none of their pending code. Credit Douglas R. +Colkitt and the original OpenAI manuscript; see [NOTICE.md](NOTICE.md) for +predecessor credit, Apache-2.0 licensing and substantial AI-assistance disclosure. diff --git a/research/binary-residual-exhaustive/SOURCES.json b/research/binary-residual-exhaustive/SOURCES.json new file mode 100644 index 0000000000..36c7770cca --- /dev/null +++ b/research/binary-residual-exhaustive/SOURCES.json @@ -0,0 +1,49 @@ +{ + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "files": { + "scripts/binary_phase_frames.py": { + "sha256": "4148cfa313cf050ed25296e8db36d35871520b8318fd086c7d1facf0c6af67d7", + "git_blob": "c8e4fa71fe60550324f9e43c1dd5ad6d9bf4e2f4" + }, + "scripts/experiments/parity_phase_repair.py": { + "sha256": "1f76f3b96ed556ed901835bd101d0e2588c997d2ed39bdfca097f0187aa86d40", + "git_blob": "abefe12ede95a382b9eeb74906c7c519d94bd705" + }, + "scripts/certify.py": { + "sha256": "2348d95008276c5d5764f7e028c3918e484582cd589bd4d9b82919161745e53e", + "git_blob": "a773311b726fd1ef98a056f6f76010e872d7908a" + }, + "notes/complex-compression.tex": { + "sha256": "10312815290c7bb8ef4db153e30fba13c032bf17ccaf991a34f1aa6340405a0d", + "git_blob": "186328572907c63735a9ccb403326ffb747773bf" + }, + "docs/research/parity-side.md": { + "sha256": "75de20f8dcd3d1a2e2d19bc087eda50a6cc77027651f48198868426a80cd12f2", + "git_blob": "b36c404820b3e9c0f28be64ba4ea2a8e924704b3" + }, + "tests/test_complex_compression.py": { + "sha256": "e22e0a339fad8ce2f73312eb7e47a762360f8c1c78122cdd8e0dc85c5fbce99f", + "git_blob": "6ca63fe751559a2418dd261bf5b24fe8486ac1b6" + }, + "tests/test_parity_side.py": { + "sha256": "4b6e78dd62e53defc2aeb29dd87df941b975fba376fbe868ad197216468bbfdb", + "git_blob": "51312c21e92adff87cc30d3f057fdf1911ccae0e" + }, + "certificates/selected-result.json": { + "sha256": "9873519224e2db72d6a8c926f51e3e75129671e467948c6f6b03744f8bcfc699", + "git_blob": "1f107b55a2f045fa66d9c35d658b3b79549f5ba6" + }, + "research/community-frontier799-audit/ASSEMBLY.json": { + "sha256": "65c7648a8edaeaf4e0b8de3e21eeda94fba124d0935010d45ac9f76375b72cec", + "git_blob": "a04bfd932a15196fe8e2418eae912ea745152593" + }, + "docs/research/community-frontier799-review.md": { + "sha256": "bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052", + "git_blob": "7a2cd0a64199e0aaf93451377acbed3e8c7ae6b7" + }, + "upstream/build/sections/03-motifs.tex": { + "sha256": "ed76761194988a01af77ead0ea6469cb5dcd29690ab985a0b5a4006b0f2b69bb", + "git_blob": "cdb0ba527aa8df5d57c151183fd3893c1a7e21ab" + } + } +} diff --git a/research/binary-residual-exhaustive/VALIDATION.json b/research/binary-residual-exhaustive/VALIDATION.json new file mode 100644 index 0000000000..ec55d6d443 --- /dev/null +++ b/research/binary-residual-exhaustive/VALIDATION.json @@ -0,0 +1,53 @@ +{ + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "environment": { + "python": "CPython 3.12.14", + "platform": "macOS 26.5.2 arm64", + "executable_used": "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3" + }, + "result": { + "status": "PASS_BINARY_RESIDUAL_EXHAUSTIVE", + "subspaces": 3290, + "nested_pairs": 29899, + "phase_inputs": 1634803, + "explicit_boundary_controls": 10, + "normal_optimized_receipts_byte_identical": true, + "receipt_sha256": "f1d401a145c49292af111e2fd1e52bbee52d4ce5e27214498e4cd516727df99d" + }, + "completed_checks": [ + { + "command": "python3 -I -B research/binary-residual-exhaustive/verify.py --output /tmp/new-normal-receipt.json", + "result": "PASS; full exact EXPECTED.json receipt matched" + }, + { + "command": "python3 -I -O -B research/binary-residual-exhaustive/verify.py --output /tmp/new-optimized-receipt.json", + "result": "PASS; full receipt byte-identical to normal replay" + }, + { + "command": "python3 -I -B research/binary-residual-exhaustive/test_verify.py", + "result": "7 test groups passed; final root run 8.724 seconds" + }, + { + "command": "python3 -I -O -B research/binary-residual-exhaustive/test_verify.py", + "result": "7 test groups passed; final root run 8.293 seconds" + }, + { + "command": "python3 -B -m unittest tests.test_complex_compression.ComplexCompression.test_binary_basis_and_rejection_of_alternating_residual tests.test_complex_compression.ComplexCompression.test_local_frames_and_phase_identity tests.test_parity_side.ParitySideTest.test_characteristic_detects_alternating_residual -v", + "result": "3 unchanged predecessor tests passed" + }, + { + "command": "python3 -I -B scripts/verify_selected_result.py", + "result": "PASS selected record, exact kappa, original source inventory and proof supplement: 1661634653669567/1000000000000000000" + } + ], + "minimal_relocation": "The test suite ran the complete optimized verifier with only the 11 pinned predecessor/context inputs and four package files, no Git or network, under a directory path containing spaces.", + "failure_detection": "Faulty classification, characteristic, residual and orthonormal-output functions, omitted subspace, source drift/missing inputs, digest/blob drift, incomplete inventory, receipt values/types and failed-output preservation were rejected.", + "review": "Separate AI mathematical review and scoped read-only code review reported no correctness blockers. Code reviewer independently ran all 7 test groups in 8.400 seconds. No independent human review claimed.", + "not_run": [ + "whole-repository make verify", + "selected supplier cold replay", + "Lean or formal multiplication theorem", + "hosted CI or Linux execution" + ], + "scope": "Only research/binary-residual-exhaustive/ is added. Existing sources, selected frontier and upstream are unchanged. Finite historical-interface evidence; no new kappa. Timings are local validation durations, not performance claims." +} diff --git a/research/binary-residual-exhaustive/oracle.py b/research/binary-residual-exhaustive/oracle.py new file mode 100644 index 0000000000..57e9ff32a9 --- /dev/null +++ b/research/binary-residual-exhaustive/oracle.py @@ -0,0 +1,188 @@ +"""Independent finite F2 oracle using complete vector sets, not elimination. + +Vectors are integer masks in an explicitly specified ambient dimension. +Subspaces are frozensets containing every vector, including zero. The bounded +enumerator covers ambient dimensions zero through six; all other helpers work +with any nonnegative ambient dimension that the caller can enumerate. +""" + +from functools import cache + + +def _dimension(n): + if not isinstance(n, int) or isinstance(n, bool) or n < 0: + raise ValueError("Ambient dimension must be a nonnegative integer") + return n + + +def _vector(vector, n): + if (not isinstance(vector, int) or isinstance(vector, bool) + or not 0 <= vector < (1 << n)): + raise ValueError("Vector must be an integer mask in the ambient space") + return vector + + +def _vectors(vectors, n): + _dimension(n) + try: + return frozenset(_vector(vector, n) for vector in vectors) + except TypeError as error: + raise ValueError("Vectors must be iterable") from error + + +@cache +def _check_space(space, n): + if 0 not in space or any(a ^ b not in space for a in space for b in space): + raise ValueError("A subspace must contain zero and be closed under XOR") + return space + + +def _space(vectors, n): + return _check_space(_vectors(vectors, n), n) + + +@cache +def _dot(a, b, n): + # Each coordinate contributes separately; no population count is used. + value = 0 + for coordinate in range(n): + value ^= ((a >> coordinate) & 1) * ((b >> coordinate) & 1) + return value + + +def dot(a, b, n): + """Compute the binary scalar product by explicit coordinate iteration.""" + _dimension(n) + return _dot(_vector(a, n), _vector(b, n), n) + + +def span(rows, n): + """Return every XOR combination of the supplied vectors.""" + rows = _vectors(rows, n) + result = frozenset({0}) + for vector in sorted(rows): + if vector not in result: + result = result | frozenset(value ^ vector for value in result) + return result + + +def _space_order(space): + return len(space), tuple(sorted(space)) + + +def list_subspaces(n): + """Enumerate all subspaces of F2^n, ordered by size and sorted vectors. + + Each next layer is obtained by adjoining every vector outside each space + in the preceding layer, taking its complete XOR closure, and deduplicating + equal vector sets. No choice of pivots or row reduction is involved. + """ + _dimension(n) + if n > 6: + raise ValueError("Exhaustive enumeration is bounded to dimension six") + return _list_subspaces(n) + + +@cache +def _list_subspaces(n): + layer = (frozenset({0}),) + result = [] + for dimension in range(n + 1): + result.extend(layer) + if dimension == n: + break + extensions = set() + for space in layer: + for vector in range(1, 1 << n): + if vector not in space: + extensions.add(space | frozenset(x ^ vector for x in space)) + layer = tuple(sorted(extensions, key=_space_order)) + return tuple(result) + + +@cache +def _basis(space, n): + generated = frozenset({0}) + result = [] + for vector in sorted(space): + if vector not in generated: + result.append(vector) + generated = generated | frozenset(x ^ vector for x in generated) + return tuple(result) + + +def basis(space, n): + """Choose deterministic representatives by greedy closure membership.""" + return _basis(_space(space, n), n) + + +@cache +def _radical(space, n): + return frozenset(x for x in space if all(_dot(x, y, n) == 0 for y in space)) + + +def radical(space, n): + """Return the radical by testing all vectors against the full space.""" + return _radical(_space(space, n), n) + + +@cache +def _classification(space, n): + alternating = all(_dot(x, x, n) == 0 for x in space) + return (len(space).bit_length() - 1, _radical(space, n) == frozenset({0}), + alternating) + + +def classify(space, n): + """Classify the restricted form, including the nondegenerate zero space.""" + dimension, nondegenerate, alternating = _classification(_space(space, n), n) + return dict(dimension=dimension, nondegenerate=nondegenerate, + nonalternating=not alternating, alternating=alternating) + + +@cache +def _characteristic_vectors(space, n): + return tuple(v for v in sorted(space) + if all(_dot(v, x, n) == _dot(x, x, n) for x in space)) + + +def characteristic_vectors(space, n): + """Find every characteristic vector by exhaustively testing candidates.""" + return _characteristic_vectors(_space(space, n), n) + + +def characteristic(space, n): + """Return the unique characteristic vector of a nondegenerate space.""" + space = _space(space, n) + if _radical(space, n) != frozenset({0}): + raise ValueError("A unique characteristic vector needs a nondegenerate space") + candidates = _characteristic_vectors(space, n) + if len(candidates) != 1: + raise ValueError("The space does not have a unique characteristic vector") + return candidates[0] + + +@cache +def _project(space, vector, n): + representatives = _basis(space, n) + candidates = tuple(candidate for candidate in sorted(space) + if all(_dot(candidate, b, n) == _dot(vector, b, n) + for b in representatives)) + if len(candidates) != 1: + raise ValueError("Orthogonal projection needs a nondegenerate space") + return candidates[0] + + +def project(space, vector, n): + """Find the unique vector in the space with matching basis pairings.""" + space = _space(space, n) + vector = _vector(vector, n) + return _project(space, vector, n) + + +def residual(lower, upper, n): + """Return U intersect A-perp for nested complete vector sets A <= U.""" + lower, upper = _space(lower, n), _space(upper, n) + if not lower <= upper: + raise ValueError("Residual spaces must be nested") + return frozenset(x for x in upper if all(_dot(x, a, n) == 0 for a in lower)) diff --git a/research/binary-residual-exhaustive/test_verify.py b/research/binary-residual-exhaustive/test_verify.py new file mode 100644 index 0000000000..79b7c734b5 --- /dev/null +++ b/research/binary-residual-exhaustive/test_verify.py @@ -0,0 +1,155 @@ +#!/usr/bin/env python3 +"""Failure-mode and independent-completeness controls; Apache-2.0.""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest +from unittest.mock import patch + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import oracle +import verify + + +class ResidualAuditTests(unittest.TestCase): + def test_independent_powerset_census(self): + # Different enumeration: inspect every subset of the 15 nonzero vectors. + # Direct XOR closure identifies all subspaces, without the extension tree. + brute = set() + for mask in range(1 << 15): + space = frozenset([0] + [i + 1 for i in range(15) if mask >> i & 1]) + if all(a ^ b in space for a in space for b in space): + brute.add(space) + self.assertEqual(brute, set(oracle.list_subspaces(4))) + self.assertEqual(len(brute), 67) + + def test_direct_projection_and_characteristic(self): + plane = oracle.span((3, 5), 3) + full = oracle.span((1, 2, 4), 3) + self.assertEqual(oracle.characteristic(plane, 3), 0) + self.assertEqual(oracle.characteristic(full, 3), 7) + self.assertEqual(oracle.residual(plane, full, 3), oracle.span((7,), 3)) + for x in range(8): + projected = oracle.project(plane, x, 3) + self.assertIn(projected, plane) + self.assertTrue(all(oracle.dot(projected ^ x, y, 3) == 0 for y in plane)) + # Isotropic characteristic != alternating form. + f2 = oracle.span((1, 2), 2) + self.assertEqual(oracle.characteristic(f2, 2), 3) + self.assertFalse(oracle.classify(f2, 2)["alternating"]) + + def test_invalid_domains(self): + for n in (-1, True, 1.5, 7): + with self.assertRaises(ValueError): + oracle.list_subspaces(n) + for vector in (-1, 8, True): + with self.assertRaises(ValueError): + oracle.dot(vector, 1, 3) + for space in ((1,), (0, 1, 2), None): + with self.assertRaises(ValueError): + oracle.classify(space, 3) + with verify.subjects() as (frames, parity): + for cap in (-1, True, 1.5, 7): + with self.assertRaises(ValueError): + verify.audit(frames, parity, cap) + + def test_predecessor_assertions_and_boundary_controls(self): + with verify.subjects() as (frames, parity): + self.assertEqual(len(verify.controls(frames, parity)), 10) + # This must fail under -O too: source is compiled with optimize=0. + with self.assertRaises(AssertionError): + frames.orthonormal_basis((3, 5)) + result = verify.audit(frames, parity, cap=3) + self.assertEqual(result["coverage"][-1]["nested_pairs"], 33) + self.assertEqual(result["coverage"][-1]["nonzero_alternating_pairs"], 2) + + def test_faulty_subjects_detected(self): + with verify.subjects() as (frames, parity): + real_classify = frames.classify + def wrong_classify(rows): + result = real_classify(rows) + result["nonalternating"] = not result["nonalternating"] + return result + with patch.object(frames, "classify", wrong_classify): + with self.assertRaisesRegex(ValueError, "Classification mismatch"): + verify.audit(frames, parity, cap=1) + with patch.object(parity, "characteristic", lambda rows: 0): + with self.assertRaisesRegex(ValueError, "Characteristic mismatch"): + verify.audit(frames, parity, cap=1) + with patch.object(frames, "residual", lambda lower, upper: ()): + with self.assertRaisesRegex(ValueError, "Residual set mismatch"): + verify.audit(frames, parity, cap=1) + real_basis = frames.orthonormal_basis + def wrong_basis(rows): + result = real_basis(rows) + return (1, 2, 7) if len(result) == 3 else result + with patch.object(frames, "orthonormal_basis", wrong_basis): + with self.assertRaisesRegex(ValueError, "Nonorthonormal output"): + verify.audit(frames, parity, cap=3) + + def test_pins_and_typed_receipt_controls(self): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + verify.check_sources() + missing = json.loads(json.dumps(manifest)) + missing["files"].pop(verify.SOURCE_PATHS[0]) + with self.assertRaisesRegex(ValueError, "Incomplete source inventory"): + verify.check_sources(manifest=missing) + for key in ("sha256", "git_blob"): + bad = json.loads(json.dumps(manifest)) + bad["files"][verify.SOURCE_PATHS[0]][key] = "0" * len(bad["files"][verify.SOURCE_PATHS[0]][key]) + with self.assertRaisesRegex(ValueError, "mismatch"): + verify.check_sources(manifest=bad) + expected = json.loads((HERE / "EXPECTED.json").read_text()) + for replacement in (True, 1.0, 2): + bad = json.loads(json.dumps(expected)) + bad["coverage"][0]["subspaces"] = replacement + self.assertFalse(verify.same_typed(expected, bad)) + with patch.object(verify, "audit", return_value=expected): + with self.assertRaisesRegex(ValueError, "Exact typed receipt mismatch"): + verify.run(expected=bad) + with verify.subjects() as (frames, parity): + small = verify.audit(frames, parity, cap=1) + with patch.object(verify, "audit", return_value=small): + with self.assertRaisesRegex(ValueError, "Exact typed receipt mismatch"): + verify.run(expected={}) + real_spaces = oracle.list_subspaces + with verify.subjects() as (frames, parity): + with patch.object(oracle, "list_subspaces", lambda n: real_spaces(n)[:-1]): + with self.assertRaisesRegex(ValueError, "Incomplete all-subspace census"): + verify.audit(frames, parity, cap=1) + + def test_minimal_relocation_and_output_preservation(self): + with tempfile.TemporaryDirectory(prefix="binary audit with spaces ") as tmp: + root = Path(tmp) + package = root / "research/binary-residual-exhaustive" + package.mkdir(parents=True) + for relative in verify.SOURCE_PATHS: + destination = root / relative + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copy2(verify.ROOT / relative, destination) + for name in ("verify.py", "oracle.py", "SOURCES.json", "EXPECTED.json"): + shutil.copy2(HERE / name, package / name) + cmd = [sys.executable, "-I", "-O", "-B", str(package / "verify.py")] + # Minimal source closure: no .git, predecessor tests are pinned context, + # and no repository module beyond the three declared subjects is loaded. + result = subprocess.run(cmd, cwd=tmp, capture_output=True, text=True, check=True) + self.assertIn("PASS_BINARY_RESIDUAL_EXHAUSTIVE", result.stdout) + output = root / "keep.json" + output.write_text("preserve me\n") + (root / verify.SOURCE_PATHS[0]).write_text("corrupt source\n") + failure = subprocess.run(cmd + ["--output", str(output)], cwd=tmp, + capture_output=True, text=True) + self.assertNotEqual(failure.returncode, 0) + self.assertIn("Source SHA256 mismatch", failure.stderr) + self.assertEqual(output.read_text(), "preserve me\n") + (root / verify.SOURCE_PATHS[0]).unlink() + with self.assertRaisesRegex(ValueError, "Missing/escaping source"): + verify.check_sources(root) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/binary-residual-exhaustive/verify.py b/research/binary-residual-exhaustive/verify.py new file mode 100644 index 0000000000..47c24d70d5 --- /dev/null +++ b/research/binary-residual-exhaustive/verify.py @@ -0,0 +1,269 @@ +#!/usr/bin/env python3 +"""Independent exhaustive finite binary-frame audit. Apache-2.0; see NOTICE.md.""" +import argparse +from collections import Counter +from contextlib import contextmanager +from functools import lru_cache +from hashlib import sha256 +import json +from pathlib import Path +import random +import sys +from types import ModuleType + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE = "f567884aeb8851b6e794af1184119a3bfbe1e631" +SEED = 83 +CAP = 6 +SOURCE_PATHS = ( + "scripts/binary_phase_frames.py", + "scripts/experiments/parity_phase_repair.py", + "scripts/certify.py", + "notes/complex-compression.tex", + "docs/research/parity-side.md", + "tests/test_complex_compression.py", + "tests/test_parity_side.py", + "certificates/selected-result.json", + "research/community-frontier799-audit/ASSEMBLY.json", + "docs/research/community-frontier799-review.md", + "upstream/build/sections/03-motifs.tex", +) +sys.path.insert(0, str(HERE)) +import oracle + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def same_typed(actual, expected): + """JSON equality that does not equate bools, integers or floats.""" + if type(actual) is not type(expected): + return False + if isinstance(actual, dict): + return actual.keys() == expected.keys() and all( + same_typed(actual[k], expected[k]) for k in actual) + if isinstance(actual, list): + return len(actual) == len(expected) and all( + same_typed(a, b) for a, b in zip(actual, expected)) + return actual == expected + + +def check_sources(root=ROOT, manifest=None): + root = Path(root).resolve() + if manifest is None: + manifest = json.loads((HERE / "SOURCES.json").read_text()) + require(manifest["base_commit"] == BASE, "Wrong base commit") + require(set(manifest["files"]) == set(SOURCE_PATHS), "Incomplete source inventory") + for relative, pin in manifest["files"].items(): + path = (root / relative).resolve() + require(path.is_relative_to(root) and path.is_file(), "Missing/escaping source: " + relative) + data = path.read_bytes() + require(sha256(data).hexdigest() == pin["sha256"], "Source SHA256 mismatch: " + relative) + from hashlib import sha1 + blob = sha1(b"blob " + str(len(data)).encode() + b"\0" + data).hexdigest() + require(blob == pin["git_blob"], "Source Git blob mismatch: " + relative) + return manifest + + +@contextmanager +def subjects(root=ROOT): + """Execute pinned originals with their assertions intact, including under -O.""" + names = ("certify", "binary_phase_frames", "binary_residual_subject_parity") + paths = ("scripts/certify.py", "scripts/binary_phase_frames.py", + "scripts/experiments/parity_phase_repair.py") + saved = {name: sys.modules.get(name) for name in names} + modules = [] + try: + for name, relative in zip(names, paths): + path = Path(root) / relative + module = ModuleType(name) + module.__file__ = str(path) + sys.modules[name] = module + exec(compile(path.read_bytes(), str(path), "exec", optimize=0), module.__dict__) + modules.append(module) + yield modules[1], modules[2] + finally: + for name, previous in saved.items(): + if previous is None: + sys.modules.pop(name, None) + else: + sys.modules[name] = previous + + +def orthonormal_output(vectors, space, n): + vectors = tuple(vectors) + require(len(vectors) == len(oracle.basis(space, n)), "Wrong orthonormal dimension") + require(oracle.span(vectors, n) == space, "Wrong orthonormal output span") + require(all(oracle.dot(a, b, n) == int(i == j) + for i, a in enumerate(vectors) for j, b in enumerate(vectors)), + "Nonorthonormal output") + return vectors + + +def expect_rejection(call, message): + try: + call() + except (ValueError, AssertionError): + return + raise ValueError("Missed rejection: " + message) + + +def controls(frames, parity): + full = (1, 2, 4) + even = (3, 5) + # This residual has no unit vector despite both endpoints being admissible. + r = frames.residual((7,), full) + require(oracle.span(r, 3) == oracle.span(even, 3), "Wrong alternating control") + expect_rejection(lambda: frames.orthonormal_basis(r), "nonzero alternating residual") + expect_rejection(lambda: frames.residual((3,), (1, 2)), "degenerate lower") + expect_rejection(lambda: frames.residual((), (3,)), "degenerate upper") + expect_rejection(lambda: frames.residual((1,), (2,)), "nonnested endpoints") + expect_rejection(lambda: parity.characteristic((3,)), "degenerate characteristic") + expect_rejection(lambda: orthonormal_output((1, 2, 7), oracle.span(full, 3), 3), + "nonorthogonal unit basis") + require(frames.orthonormal_basis(frames.residual(even, even)) == (), + "Equal alternating endpoints must allow zero residual") + # q(7)=3, so an odd norm cannot be replaced by phase weight +1. + phase = oracle.project(oracle.span((7,), 3), 1, 3).bit_count() % 4 + require(phase == 3 and phase != 1, "Odd phase weight control failed") + require((-phase) % 4 != phase, "Reverse phase sign control failed") + # Checking only dimension/rank would accept the wrong orthonormal plane. + expect_rejection(lambda: orthonormal_output((1, 2), oracle.span((1, 4), 3), 3), + "wrong residual of same rank") + return { + "nonzero_alternating_rejected": True, + "degenerate_lower_rejected": True, + "degenerate_upper_rejected": True, + "nonnested_rejected": True, + "degenerate_characteristic_rejected": True, + "nonorthogonal_unit_basis_rejected": True, + "zero_residual_at_alternating_endpoints_accepted": True, + "unit_phase_weight_substitution_detected": True, + "reverse_phase_sign_substitution_detected": True, + "same_rank_wrong_span_detected": True, + } + + +def gaussian_counts(n): + """Independent integer recurrence [n,k]_2=[n-1,k-1]_2+2^k[n-1,k]_2.""" + row = [1] + for size in range(1, n + 1): + row = [(row[k - 1] if k else 0) + ((1 << k) * row[k] if k < size else 0) + for k in range(size + 1)] + return row + + +def audit(frames, parity, cap=CAP): + require(type(cap) is int and 0 <= cap <= CAP, "Audit cap must be an integer in 0..6") + rng = random.Random(SEED) + rows = [] + for n in range(cap + 1): + spaces = oracle.list_subspaces(n) + classes = {s: oracle.classify(s, n) for s in spaces} + dims = Counter(c["dimension"] for c in classes.values()) + require([dims[k] for k in range(n + 1)] == gaussian_counts(n), + "Incomplete all-subspace census") + nondegenerate = [s for s in spaces if classes[s]["nondegenerate"]] + canonical = {s: oracle.basis(s, n) for s in spaces} + presented = {} + totals = Counter() + for space in spaces: + redundant = list(sorted(space)) + rng.shuffle(redundant) + presented[space] = tuple(redundant) + expected = {key: classes[space][key] + for key in ("dimension", "nondegenerate", "nonalternating")} + for vectors in (canonical[space], presented[space]): + require(same_typed(frames.classify(vectors), expected), "Classification mismatch") + admissible = expected["dimension"] == 0 or ( + expected["nondegenerate"] and expected["nonalternating"]) + if admissible: + orthonormal_output(frames.orthonormal_basis(vectors), space, n) + totals["accepted_basis_presentations"] += 1 + else: + expect_rejection(lambda: frames.orthonormal_basis(vectors), "inadmissible space") + totals["rejected_basis_presentations"] += 1 + totals["classified_presentations"] += 1 + if expected["nondegenerate"]: + want = oracle.characteristic(space, n) + for vectors in (canonical[space], presented[space]): + require(parity.characteristic(vectors) == want, "Characteristic mismatch") + totals["characteristic_presentations"] += 1 + @lru_cache(None) + def projection(space, x): + return oracle.project(space, x, n) + for upper in nondegenerate: + w = oracle.characteristic(upper, n) + for lower in nondegenerate: + if not lower <= upper: + continue + expected_residual = oracle.residual(lower, upper, n) + result = frames.residual(canonical[lower], presented[upper]) + require(oracle.span(result, n) == expected_residual, "Residual set mismatch") + c = oracle.classify(expected_residual, n) + require(c["nondegenerate"], "Residual lost nondegeneracy") + require(c["dimension"] == classes[upper]["dimension"] - classes[lower]["dimension"], + "Residual dimension mismatch") + require(c["alternating"] == (w in lower), "Characteristic membership criterion failed") + totals["nested_pairs"] += 1 + if c["dimension"] and c["alternating"]: + expect_rejection(lambda: frames.orthonormal_basis(result), "alternating pair residual") + totals["nonzero_alternating_pairs"] += 1 + continue + units = orthonormal_output(frames.orthonormal_basis(result), expected_residual, n) + totals["admissible_pairs"] += 1 + totals["zero_residual_pairs"] += int(c["dimension"] == 0) + for x in range(1 << n): + pu, pa = projection(upper, x), projection(lower, x) + pr = 0 + phase = 0 + for v in units: + if oracle.dot(v, x, n): + pr ^= v + phase += v.bit_count() + require(pu ^ pa == pr, "Orthogonal projector decomposition mismatch") + require((pu.bit_count() - pa.bit_count()) % 4 == phase % 4, + "Forward Hamming-weight phase mismatch") + require((pa.bit_count() - pu.bit_count()) % 4 == (-phase) % 4, + "Reverse Hamming-weight phase mismatch") + totals["phase_inputs"] += 1 + rows.append({"ambient_dimension": n, "subspaces_by_dimension": gaussian_counts(n), + "subspaces": len(spaces), "nondegenerate_subspaces": len(nondegenerate), + **dict(sorted(totals.items()))}) + return {"status": "PASS_BINARY_RESIDUAL_EXHAUSTIVE", "base_commit": BASE, + "assignment_seed": SEED, "ambient_cap": cap, + "source_assertions": "Explicit compile(optimize=0); unchanged predecessor source", + "coverage": rows, "controls": controls(frames, parity), + "scope": "Exhaustive finite evidence only; historical binary residual interface, no new kappa"} + + +def run(root=ROOT, expected=None): + check_sources(root) + with subjects(root) as (frames, parity): + receipt = audit(frames, parity) + if expected is None: + expected = json.loads((HERE / "EXPECTED.json").read_text()) + require(same_typed(receipt, expected), "Exact typed receipt mismatch") + return receipt + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="Write a verified receipt to a new file") + args = parser.parse_args() + receipt = run() + if args.output: + with args.output.open("x") as stream: + stream.write(json.dumps(receipt, indent=2) + "\n") + coverage = receipt["coverage"] + print("PASS_BINARY_RESIDUAL_EXHAUSTIVE subspaces=" + str(sum(r["subspaces"] for r in coverage)) + + " nested_pairs=" + str(sum(r["nested_pairs"] for r in coverage)) + + " phase_inputs=" + str(sum(r["phase_inputs"] for r in coverage)) + + " controls=10 kappa=unchanged") + + +if __name__ == "__main__": + main() From 1074ca98132123b1f2c88375241295b8e2be3c57 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Tue, 13 Oct 2026 05:00:28 -0700 Subject: [PATCH 2/2] Record completed independent-verification claim and PR #911 result --- research/binary-residual-exhaustive/CLAIM.json | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/research/binary-residual-exhaustive/CLAIM.json b/research/binary-residual-exhaustive/CLAIM.json index b500359c0d..ac62722a04 100644 --- a/research/binary-residual-exhaustive/CLAIM.json +++ b/research/binary-residual-exhaustive/CLAIM.json @@ -18,5 +18,16 @@ "overlap": "All-state targeted PR searches inspected binary_phase_frames, orthonormal, nonalternating and alternating residual. PR771 enumerates full-space isometry bases and invoices; PR831 studies F4 phase interfaces; PR712 checks one cold wrapper. None supplies the all-subspace/nested-pair residual census proposed here. No pending PR supplies code or inputs.", "expected_deliverable": "One standalone independent-verification package with exact census, source pins, corruption controls and written scope; no new kappa and no frontier edits.", "delegation": "One worker owns only the independent vector-set oracle; one worker performs a read-only mathematical review. Both stay within this claim.", - "status": "CLAIMED" + "status": "COMPLETED", + "completed_at_utc": "2026-10-13T11:59:58Z", + "result_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/911", + "result": { + "subspaces": 3290, + "nondegenerate_nested_pairs": 29899, + "phase_inputs_each_direction": 1634803, + "negative_controls": 10, + "new_kappa": false, + "source_defect_found": false + }, + "validation": "Seven test groups passed normally and under -O; normal and optimized complete receipts byte-identical; three targeted predecessor tests and selected-record integrity passed. See VALIDATION.json." }