From c80f445e8c3c22d341d467254b89245fbddb9eb2 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 10:22:04 +0100 Subject: [PATCH] feat(research): count five-request binary threshold headers --- .../binary-threshold-five-headers/PROOF.md | 155 +++++++++++ .../binary-threshold-five-headers/README.md | 119 +++++++++ .../SOURCES.json | 30 +++ .../binary-threshold-five-headers/TASK.json | 86 ++++++ .../binary-threshold-five-headers/VERIFY.json | 32 +++ .../binary-threshold-five-headers/verify.py | 247 ++++++++++++++++++ 6 files changed, 669 insertions(+) create mode 100644 research/binary-threshold-five-headers/PROOF.md create mode 100644 research/binary-threshold-five-headers/README.md create mode 100644 research/binary-threshold-five-headers/SOURCES.json create mode 100644 research/binary-threshold-five-headers/TASK.json create mode 100644 research/binary-threshold-five-headers/VERIFY.json create mode 100644 research/binary-threshold-five-headers/verify.py diff --git a/research/binary-threshold-five-headers/PROOF.md b/research/binary-threshold-five-headers/PROOF.md new file mode 100644 index 0000000000..dfc695f0fd --- /dev/null +++ b/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= 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. diff --git a/research/binary-threshold-five-headers/README.md b/research/binary-threshold-five-headers/README.md new file mode 100644 index 0000000000..ad53f5100f --- /dev/null +++ b/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. diff --git a/research/binary-threshold-five-headers/SOURCES.json b/research/binary-threshold-five-headers/SOURCES.json new file mode 100644 index 0000000000..a1f972ea07 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/binary-threshold-five-headers/TASK.json b/research/binary-threshold-five-headers/TASK.json new file mode 100644 index 0000000000..e1cff933e4 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/binary-threshold-five-headers/VERIFY.json b/research/binary-threshold-five-headers/VERIFY.json new file mode 100644 index 0000000000..32d5fb340b --- /dev/null +++ b/research/binary-threshold-five-headers/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact 24-set five-request census, 2,880 literal complete-header guard checks, smaller positive controls, five semantic rejection controls and source-bound stdout receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same exhaustive finite result and controls with Python assertions disabled." + } + ] +} diff --git a/research/binary-threshold-five-headers/verify.py b/research/binary-threshold-five-headers/verify.py new file mode 100644 index 0000000000..e7c67a920c --- /dev/null +++ b/research/binary-threshold-five-headers/verify.py @@ -0,0 +1,247 @@ +#!/usr/bin/env python3 +"""Exact five-request binary threshold census, produced by Nick Petalas. + +Standard library only. Apache-2.0. No imported predecessor code. +""" +from collections import defaultdict +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations, permutations +from math import comb, factorial, prod +from pathlib import Path +import json + + +WITNESS = ((3, 12), (6, 17), (9, 18), (20, 10), (24, 5)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def target(k): + require(3 <= k <= 5, "supported request count is 3..5") + return sum((((1 << k) - 1) ^ (1 << i)) << (k * i) for i in range(k)) + + +def rectangle(k, s, t): + require(3 <= k <= 5 and 0 < s < 1 << k and 0 < t < 1 << k, + "rectangle domain") + require(s & t == 0, "rectangle must avoid the diagonal") + return sum(t << (k * i) for i in range(k) if s >> i & 1) + + +def alphabet(k): + require(3 <= k <= 5, "supported request count is 3..5") + result = [(rectangle(k, s, t), s, t) + for s in range(1, 1 << k) for t in range(1, 1 << k) + if not s & t] + require(len(result) == 3 ** k - 2 ** (k + 1) + 1, "alphabet size") + require(len({r[0] for r in result}) == len(result), "unique factors") + return result + + +def xor_bits(values): + require(len(values) <= 6, "at most six factors") + result = 0 + for value in values: + result ^= value + return result + + +def enumerate_sets(k, candidates): + """Unique increasing sets, split before the last ceil(k/2) indices.""" + require(3 <= k <= 5 and k <= len(candidates) <= 180, "census bounds") + left_size = k // 2 + table = defaultdict(list) + left_work = 0 + for indices in combinations(range(len(candidates)), left_size): + bits = xor_bits([candidates[i][0] for i in indices]) + table[bits].append(indices) + left_work += 1 + found = [] + right_work = 0 + for suffix in combinations(range(len(candidates)), k - left_size): + needed = target(k) ^ xor_bits([candidates[i][0] for i in suffix]) + for prefix in table.get(needed, ()): + if prefix[-1] < suffix[0]: + found.append(prefix + suffix) + right_work += 1 + require(left_work == comb(len(candidates), left_size), "left coverage") + require(right_work == comb(len(candidates), k - left_size), "right coverage") + require(len(found) == len(set(found)), "each set counted once") + return sorted(found), {"left_subsets": left_work, "right_subsets": right_work} + + +def matrix_product(a, b): + n = len(a) + require(1 <= n <= 6 and len(b) == n, "matrix dimensions") + require(all(len(row) == n for row in a + b), "square matrices") + return [[sum(a[i][h] * b[h][j] for h in range(n)) % 2 + for j in range(n)] for i in range(n)] + + +def identity(n): + require(1 <= n <= 6, "identity domain") + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def inverse(a): + n = len(a) + require(1 <= n <= 6 and all(len(row) == n for row in a), "inverse domain") + rows = [row[:] + unit for row, unit in zip(a, identity(n))] + for j in range(n): + pivots = [i for i in range(j, n) if rows[i][j]] + require(bool(pivots), "singular header") + p = pivots[0] + rows[j], rows[p] = rows[p], rows[j] + for i in range(n): + if i != j and rows[i][j]: + rows[i] = [x ^ y for x, y in zip(rows[i], rows[j])] + require([row[:n] for row in rows] == identity(n), "inverse elimination") + return [row[n:] for row in rows] + + +def full_guards(a): + """Literal no-pivot elimination through rank n-1 over F2.""" + n = len(a) + require(2 <= n <= 6 and all(len(row) == n for row in a), "guard domain") + rows = [row[:] for row in a] + for j in range(n - 1): + if rows[j][j] != 1: + return False + for i in range(j + 1, n): + if rows[i][j]: + rows[i] = [x ^ y for x, y in zip(rows[i], rows[j])] + return True + + +def passing_header(g): + n = len(g) + gi = inverse(g) + for t in range(n - 1): + request = identity(n) + request[t][t] = 0 + conjugate = matrix_product(matrix_product(g, request), gi) + if not full_guards(conjugate): + return False + return True + + +def complete_header(k, factors): + require(3 <= k <= 5 and len(factors) == k, "completion domain") + require(xor_bits([rectangle(k, s, t) for s, t in factors]) == target(k), + "wrong rectangle sum") + full = (1 << k) - 1 + x = [[t >> j & 1 for j in range(k)] for _, t in factors] + x.append([1] * k) + columns = [s for s, _ in factors] + [full] + kernel = [z for z in range(1, 1 << (k + 1)) + if xor_bits([columns[i] for i in range(k + 1) if z >> i & 1]) == 0] + require(len(kernel) == 1, "unique nonzero kernel vector") + z = kernel[0] + g = [row + [z >> i & 1] for i, row in enumerate(x)] + gi = inverse(g) + require([row[:] for row in gi[:k]] == + [[column >> j & 1 for column in columns] for j in range(k)], + "completed inverse has prescribed rows") + return g + + +def header_census(k, candidates, found): + seen = set() + for indices in found: + factors = tuple((candidates[i][1], candidates[i][2]) for i in indices) + for ordered in permutations(factors): + g = complete_header(k, ordered) + require(passing_header(g), "literal full guards reject a constructed header") + encoded = tuple(sum(bit << j for j, bit in enumerate(row)) for row in g) + require(encoded not in seen, "duplicate full header") + seen.add(encoded) + require(len(seen) == len(found) * factorial(k), "header fiber count") + return len(seen) + + +def row_column_only(k, candidates, found): + full = (1 << k) - 1 + rows = {(1 << i, full ^ (1 << i)) for i in range(k)} + columns = {(t, s) for s, t in rows} + return sum({(candidates[i][1], candidates[i][2]) for i in inds} + in (rows, columns) for inds in found) + + +def expect_rejection(k, factors): + try: + complete_header(k, factors) + except ValueError: + return + raise ValueError("corrupted factor fixture was accepted") + + +def controls(candidates, found): + require(row_column_only(5, candidates, found) == 2, "row/column baseline") + require(len(found) > 2, "row/column-only conjecture must fail") + require(all(s.bit_count() == t.bit_count() == 2 for s, t in WITNESS), + "witness is outside both star classes") + witness_indices = tuple(sorted(candidates.index((rectangle(5, s, t), s, t)) + for s, t in WITNESS)) + require(witness_indices in found, "explicit counterexample missing") + changed = list(WITNESS) + changed[0] = (3, 4) + expect_rejection(5, changed) + changed[0] = (3, 13) + expect_rejection(5, changed) + require(not passing_header(identity(6)), "identity fails full guard chain") + late_failure = [identity(6)[-1]] + identity(6)[:-1] + gi = inverse(late_failure) + for t in range(5): + request = identity(6) + request[t][t] = 0 + conjugate = matrix_product(matrix_product(late_failure, request), gi) + require(conjugate[0][0] == 1, "late-failure fixture passes every first guard") + require(not passing_header(late_failure), "later guards must reject the fixture") + broken = complete_header(5, WITNESS) + broken[-1] = broken[0][:] + try: + inverse(broken) + except ValueError: + pass + else: + raise ValueError("singular header admitted") + return {"row_column_sets": 2, "nonstar_sets": len(found) - 2, + "rejected_corruptions": 5, "witness_membership": True} + + +def main(): + report = {"claim_type": "finite certificate", "censuses": []} + five_candidates = five_found = None + for k in range(3, 6): + candidates = alphabet(k) + found, work = enumerate_sets(k, candidates) + expected = {3: 2, 4: 2, 5: 24}[k] + require(len(found) == expected, "exact decomposition count") + count = header_census(k, candidates, found) + gl_order = prod((1 << (k + 1)) - (1 << j) for j in range(k + 1)) + report["censuses"].append({"k": k, "m": k + 1, + "rectangles": len(candidates), "unordered_decompositions": len(found), + "passing_headers": count, "GL_order": gl_order, + "density": str(Fraction(count, gl_order)), **work}) + if k == 5: + five_candidates, five_found = candidates, found + require(five_candidates is not None and five_found is not None, "five-case executed") + report["controls"] = controls(five_candidates, five_found) + report["five_decompositions"] = [ + [[five_candidates[i][1], five_candidates[i][2]] for i in indices] + for indices in five_found] + report["explicit_witness_header_rows"] = complete_header(5, WITNESS) + package = Path(__file__).resolve().parent + files = sorted(p for p in package.iterdir() if p.is_file()) + require(len(files) == 6, "expected six package files") + report["package_sha256"] = {p.name: sha256(p.read_bytes()).hexdigest() for p in files} + print("PASS_BINARY_THRESHOLD_FIVE_HEADERS") + print(json.dumps(report, indent=2)) + + +if __name__ == "__main__": + main()