Count 2,880 five-request binary threshold headers; refute 2 k! (no new κ)

research/binary-threshold-five-headers/PROOF.md

@@ -0,0 +1,155 @@
+# The five-request threshold is not row/column rigid
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement
+
+Let U_1,...,U_5 be pairwise orthogonal rank-one idempotents on F_2^6.
+Set P_t = I - U_t. Give every complete header G in GL_6(F_2) equal weight.
+A header passes P_t when every leading principal minor of G P_t G^-1
+of orders 1,...,5 is nonzero.
+
+There are exactly 2,880 headers passing all five requests, a fraction
+1/6,999,552 of GL_6(F_2). The exact count is a finite certificate supplied
+by the exhaustive enumerator. The algebraic reduction and the explicit
+counterexample below are scoped proofs. No all-k count is asserted.
+
+This answers Open next question 1 of
+[#4275](https://github.com/CrocSwap/integer-mult-bounds/pull/4275)
+negatively. Its observations at k = 3,4 suggested 2 k! passing headers at
+m = k+1. At k = 5 there are 24 unordered decompositions, giving
+24*5! = 2,880 headers instead of 2*5! = 240.
+
+## The header/decomposition bijection
+
+We use the partial-Gram reduction and binary threshold argument of #4275,
+produced by Nick Petalas. The following specialization makes the finite
+certificate self-contained. Pairwise orthogonality permits one fixed basis
+change taking U_t to e_t e_t^T. This change permutes the complete header
+domain, so it preserves the count.
+
+Let X be the first five columns of G and Y the first five rows of G^-1.
+Then YX = I_5. Write x_i for row i of X, y_i for column i of Y, and
+A_j = sum_(i<=j) y_i x_i. The determinant identity gives
+
+```text
+det((G P_t G^-1)[1..j,1..j]) = 1 - (A_j)_tt.
+```
+
+Over F_2 every guard passes precisely when every A_j has zero diagonal
+for j = 1,...,5. Consequently each of the first five increments has zero
+diagonal, and its factors have disjoint supports S_i and T_i. Since
+A_6 = I_5, the last increment has all diagonal entries one. A binary
+rank-one matrix with unit diagonal has both factors equal to the all-ones
+vector, so it is J. Thus
+
+```text
+sum_(i=1)^5 1_(S_i) 1_(T_i)^T = J - I_5,
+S_i intersect T_i = empty.
+```
+
+Conversely any such ordered decomposition defines X and Y by those factors
+in their first five coordinates and by all ones in coordinate six. Their
+product is YX = (J-I)+J = I. Hence both have rank five. The one-dimensional
+kernel of Y has a unique nonzero vector z. The matrix G = [X,z] is
+invertible, and its inverse has first five rows Y. This gives exactly one
+header per ordered decomposition. Its full guard chain passes because all
+five intermediate diagonals vanish. These constructions are inverse.
+
+## Why only distinct nonzero rectangles need enumeration
+
+Write E = J-I_5. It has rank four and E^2 = E over F_2. Suppose it were the
+sum of n <= 4 disjoint-support rank-one matrices, E = BC, with B having n
+columns and C having n rows. Rank forces n = 4, B injective and C
+surjective. Idempotence gives B(CB-I)C = 0, so CB = I_4. But every diagonal
+entry of CB is the scalar product of a disjoint-support pair, hence zero.
+This contradicts CB = I_4.
+
+A zero increment in a five-term decomposition would leave at most four
+nonzero terms. A repeated rectangle cancels in characteristic two and
+would leave at most three terms. Both are impossible. Every decomposition
+therefore consists of five distinct nonzero rectangles, in any order.
+There are
+
+```text
+3^5 - 2*2^5 + 1 = 180
+```
+
+possible nonzero rectangles with disjoint supports. A nonzero binary
+rectangle has a unique support pair, so distinct support pairs are distinct
+matrices.
+
+## Exhaustive certificate and its coverage
+
+The verifier encodes a 5 by 5 binary matrix as a 25-bit integer, with cell
+(i,j) at bit 5*i+j, using zero-based indices. Matrix addition is XOR.
+It lists all 180 support pairs in increasing order of S, then T.
+
+For every pair of distinct indices a<b it stores the pair and the XOR of
+its rectangles. There are 16,110 pairs. For every triple c<d<e, of which
+there are 955,860, it looks up the complementary XOR needed to reach E.
+It retains a match exactly when b<c.
+
+Every five-element subset has exactly one split into its first two and
+last three indices. Thus the strict inequality counts every admissible
+subset once and excludes repeated indices. Every match has XOR E by
+construction. The exhaustive run finds 24 subsets, and prints every one
+as five integer support-mask pairs. Each has 120 distinct orderings.
+
+The verifier constructs all 2,880 corresponding complete matrices G,
+inverts each, forms all five full conjugated request matrices by generic
+binary matrix multiplication, and checks every full guard chain by literal
+no-pivot elimination. It also checks that all 2,880 headers are distinct.
+It does not enumerate all of GL_6. Exhaustiveness follows from the
+bijection and the exhaustive five-subset enumeration, rather than from a
+sampling argument.
+
+Finally,
+
+```text
+|GL_6(F_2)| = product_(i=0)^5 (64-2^i) = 20,158,709,760,
+2880 / 20,158,709,760 = 1 / 6,999,552.
+```
+
+## A counterexample that can be checked by hand
+
+Use one-based coordinate labels in this display:
+
+```text
+S             T
+{1,2}         {3,4}
+{2,3}         {1,5}
+{1,4}         {2,5}
+{3,5}         {2,4}
+{4,5}         {1,3}
+```
+
+Each rectangle avoids the diagonal. In each row their column supports
+partition the other four coordinates, so their sum is exactly J-I_5,
+even before reducing modulo two. Every source and target support has size
+two, so this is neither a row-star nor a column-star decomposition. In
+least-significant-bit support notation, it is
+
+```text
+(3,12), (6,17), (9,18), (20,10), (24,5).
+```
+
+The verifier prints its literal 6 by 6 passing header and requires this
+specific decomposition to occur in the exhaustive list. Only two of the
+24 subsets are the row-star and column-star subsets. The other 22 produce
+2,640 additional headers.
+
+## Limits
+
+The exact count is for five requests in dimension six over F_2, with the
+complete equally weighted GL header domain and fixed orthogonal kernel
+lines. No count at k >= 6, arbitrary nonorthogonal kernels, odd fields or
+restricted header families follows. The explicit counterexample refutes
+the proposed all-k pattern. It does not alter any theorem proved in #4275.
+
+Header generation, selection, emission, dispatch, dirty restoration,
+stock, precision and the full physical caller remain unpriced. Binary
+algebra alone does not enter an odd-prime executable normalizer. There is
+no supplier admission, selected-frontier change, new kappa or complete
+multiplication theorem here. Independent human and formal proof-kernel
+review are unclaimed.

research/binary-threshold-five-headers/README.md

@@ -0,0 +1,119 @@
+# Five binary shared-header requests have 2,880 threshold headers
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Claim type: finite certificate with a scoped algebraic proof and explicit
+counterexample.** For five corank-one requests I-U_t on F_2^6 with pairwise
+orthogonal rank-one kernel projectors, exactly **2,880** complete GL_6(F_2)
+headers pass every leading-principal-minor guard through rank five. Their
+exact fraction is **1/6,999,552**.
+
+This answers Open next question 1 of
+[#4275](https://github.com/CrocSwap/integer-mult-bounds/pull/4275)
+negatively. The proposed threshold pattern 2 k! would give only 240
+headers at k = 5. There are 24 unordered five-rectangle decompositions of
+J-I_5, rather than the two row-star and column-star decompositions. The
+22 other subsets give 2,640 additional headers. Only the k = 5 case and
+the counterexample to the all-k pattern are new claims.
+
+[PROOF.md](PROOF.md) gives the exact header/decomposition bijection, proves
+that zero and repeated rectangles cannot occur, and explains why the
+finite enumeration is exhaustive. An explicit counterexample uses these
+source and target support masks, with bit zero denoting coordinate one:
+
+```text
+(3,12), (6,17), (9,18), (20,10), (24,5).
+```
+
+Every support has size two. These rectangles partition the off-diagonal
+cells, so this counterexample can also be checked by hand.
+
+## Evidence and reproduction
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/binary-threshold-five-headers/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/binary-threshold-five-headers/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/binary-threshold-five-headers
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/binary-threshold-five-headers --check-source-history
+```
+
+Replace the interpreter path with another CPython 3.12 installation where
+needed. The last command requires a publication commit with full history.
+
+Expected marker: `PASS_BINARY_THRESHOLD_FIVE_HEADERS`. The verifier prints
+the 24 decompositions, exact counts and fractions, the explicit witness
+header, and a receipt bound to all six package-file hashes. It writes no
+files. No receipt is handwritten or stored in this package.
+
+The five-request census visits all 180 disjoint-support nonzero binary
+rectangles, 16,110 pairs and 955,860 triples. Splitting each sorted
+five-element set after its first two indices counts it exactly once.
+The verifier completes all 24*120 decompositions to distinct full headers,
+inverts them, conjugates every request by ordinary binary matrix
+multiplication, and checks every full guard chain by no-pivot elimination.
+This supplies 2,880 literal header checks without enumerating all
+20,158,709,760 elements of GL_6.
+
+The same new enumerator uses k = 3,4 as small positive controls. They give
+12 and 48 headers, matching the cited predecessor observations. They are
+not a separate audit deliverable. Five corruptions are rejected: a wrong
+rectangle sum, a diagonal rectangle, the identity header's failing guard
+chain, a header passing every first guard but failing a later guard, and
+a singular header. The explicit nonstar witness must occur,
+and a row/column-only enumeration demonstrably undercounts by a factor 12.
+Checks use explicit exceptions and also run with Python optimization.
+
+## Scope and credit
+
+The partial-Gram reduction and minimal-dimension argument come from the
+counting package produced by Nick Petalas in #4275. The new five-request
+enumeration and counterexample answer its open question; no predecessor
+code is imported or replayed. Exact Git blob and SHA256 provenance pins
+for that proof and question are in [SOURCES.json](SOURCES.json), together
+with the original card and selected record. There are no live external
+proof inputs or third-party Python dependencies. Cinna Davis supplied the
+BIT request context in #4100; source527, commdata2338 and Jose Manuel
+retain the normalizer lineage credit.
+
+The original card is `uniform-transfer-audit`, priority revision 7. Its
+scope changes to original counting work, as recorded in [TASK.json](TASK.json).
+The result addresses a shared-header counting question. A fully paid
+producer/consumer protocol would still be needed to turn it into a
+physical saving. The family expansion decision is to stop at this finite
+result and leave larger classifications as open questions.
+
+Only five orthogonal kernel lines over F_2 in dimension six, with a
+complete equally weighted GL header domain, are counted. This gives no
+all-k formula, odd-field count, restricted-header guarantee or
+nonorthogonal classification. Physical header generation, selection,
+emission, dispatch, dirty return, stock, precision and caller costs remain
+unknown. There is no supplier admission, new kappa or selected-frontier
+change. Independent human and formal proof-kernel review are unclaimed.
+The selected cold replay, Lean and Docker were not run.
+
+The verifier uses bounded loops, no recursion and functions below 60
+physical lines. The largest subset traversal has 955,860 iterations; the
+pair table has 16,110 entries before grouping, and at most 2,880 six-row
+headers are retained. CPython dynamic integer/container allocation is a
+managed-runtime deviation from fixed allocation, bounded by these finite
+domains. Warnings are errors in both registered modes. No shared runtime
+or repository-wide diagnostic configuration changes are needed.
+
+## Open next questions
+
+1. Classify the 24 five-request subsets structurally. This would explain
+   the first failure of row/column rigidity rather than just count it.
+   Start by grouping the emitted support pairs under coordinate
+   permutations and transposition. No such orbit classification is
+   claimed here.
+2. Determine the threshold count at k >= 6, or a family of nonstar
+   decompositions for general k. This would replace the refuted 2 k!
+   pattern with a useful statement. Start by asking whether the displayed
+   five-request partition extends when a coordinate is added. The larger
+   census and an all-k argument remain unrun.
+3. Find an actual producer whose orthogonal kernel family can use a paid
+   shared header. Pin its request and charge selection, emission,
+   dispatch, restoration and stock before treating density as a gain.
+   No producer or complete physical invoice is supplied.

research/binary-threshold-five-headers/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40",
+      "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/corankone-triple-header-law/README.md",
+      "usage": "provenance",
+      "git_blob": "830650a2a4f954d0170e138c17eed5967d21a824",
+      "sha256": "b7a6cf666e30a4ef135aa7190fe545dd7203cd1ffcc175138bd3dda7484155f2"
+    },
+    {
+      "path": "research/corankone-triple-header-law/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "c36c3137027fe71f52ccf7c94add1758c39123a8",
+      "sha256": "1490daed4867cd92539f85538b81d8e3469bace39a16b7d4b6582745d5bc1e4f"
+    }
+  ]
+}

research/binary-threshold-five-headers/TASK.json

@@ -0,0 +1,86 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Finite exact count of passing complete binary GL_6 headers for five corank-one requests with orthogonal rank-one kernels, and an explicit counterexample to the proposed 2 k! threshold pattern in PR4275.",
+  "scope_change_reason": "The assignment asks for original successor work rather than an audit. This answers Open next question 1 of PR4275 by enumerating the first uncovered case k=5. It is a scoped counting side result, not a universal transfer audit.",
+  "bottleneck_link": "Joint guard counts matter for shared-header selection. This corrects the proposed minimal-header pattern but supplies no producer or physical caller; their costs remain unknown and kappa is unchanged.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified original improvement: a nonstar k=5 threshold decomposition and its exhaustive finite count. Do not extend to k>=6.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the header/decomposition bijection and explicit counterexample. verify.py enumerates all 16,110 pairs and 955,860 triples from 180 rectangles, obtains 24 unordered decompositions, completes all 2,880 ordered cases to distinct headers, and checks every full conjugated guard chain. Normal and optimized registered modes retain all checks.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What structural classification explains the 24 unordered five-request threshold decompositions?",
+      "why_it_matters": "It would explain why row/column rigidity first fails.",
+      "first_step": "Group the emitted support pairs under coordinate permutations and transposition.",
+      "blocked_by": "No orbit classification is claimed or run here."
+    },
+    {
+      "question": "What is the threshold count for k>=6, or an all-k nonstar family?",
+      "why_it_matters": "A new statement is needed in place of the refuted 2 k! pattern.",
+      "first_step": "Test whether the explicit five-request partition can be extended by one coordinate.",
+      "blocked_by": "The larger census and an all-k argument are unrun."
+    },
+    {
+      "question": "Can an actual producer use a fully paid shared header for orthogonal kernel lines?",
+      "why_it_matters": "A joint density alone does not supply a physical saving.",
+      "first_step": "Pin a request producer and charge selection, emission, dispatch, dirty return and stock.",
+      "blocked_by": "No producer or complete physical invoice is supplied."
+    }
+  ]
+}