Independent verification: exhaustive binary residual and phase-interface census (no new kappa)

research/binary-residual-exhaustive/CLAIM.json

@@ -0,0 +1,33 @@
+{
+  "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": "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."
+}

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"
+}

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.

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.