From 8448d0552496963f4cd02ee7abec89c6fb649690 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 12:11:18 +0000 Subject: [PATCH] feat(research): certify fixed two-burst query minimum --- research/two-burst-thin-rank/PROOF.md | 115 ++++++++++++++++ research/two-burst-thin-rank/README.md | 90 +++++++++++++ research/two-burst-thin-rank/SOURCES.json | 36 +++++ research/two-burst-thin-rank/TASK.json | 89 +++++++++++++ research/two-burst-thin-rank/VERIFY.json | 38 ++++++ research/two-burst-thin-rank/algebra.py | 155 ++++++++++++++++++++++ research/two-burst-thin-rank/verify.py | 150 +++++++++++++++++++++ 7 files changed, 673 insertions(+) create mode 100644 research/two-burst-thin-rank/PROOF.md create mode 100644 research/two-burst-thin-rank/README.md create mode 100644 research/two-burst-thin-rank/SOURCES.json create mode 100644 research/two-burst-thin-rank/TASK.json create mode 100644 research/two-burst-thin-rank/VERIFY.json create mode 100644 research/two-burst-thin-rank/algebra.py create mode 100644 research/two-burst-thin-rank/verify.py diff --git a/research/two-burst-thin-rank/PROOF.md b/research/two-burst-thin-rank/PROOF.md new file mode 100644 index 0000000000..cda6f98d03 --- /dev/null +++ b/research/two-burst-thin-rank/PROOF.md @@ -0,0 +1,115 @@ +# Fixed-schedule rank certificate + +## Statement + +Work over `F2[x0,x1,x2,e]/(e^2)`. The six full calls are the first six +records in the pinned `SOURCE-WORD.json` of PR #5699, inherited from Ali +Romman's PR #5673. Call i is + +`Fi = I + x_stage(i) Pi + e Ri + e x_stage(i) Ri`. + +The full-call order is exactly `(1,3,2,4,0,5)`. A gap numbered k is after k +full calls. Thin queries may occur only in gaps 2 and 4, and each is `I+e Q` +with Q a constant binary rank-one matrix. Legal source thin queries also have +`Q^2=0`. The intended endpoint is `(1+e) A`, where + +`A = product_(j=0..2) (I + xj (P_(2j)+P_(2j+1)))`. + +The minimum number of thin queries in this schedule is eight. The lower +bound allows arbitrary rank-one Q, so it also applies when square zero is +required. This is a finite binary certificate with a mathematical reduction. + +## Reduction to two aggregate matrices + +Since `e^2=0`, a consecutive burst satisfies + +`product_i (I+e Qi) = I+e sum_i Qi`. + +Let Z1 and Z2 be the sums at the two gaps. Let `A+e B` be the product of +the six full calls, with later calls multiplying on the left. Let Lg and Rg +be its e-free suffix and prefix at gap g. Contributions containing two e +factors vanish. Thus the complete endpoint is correct exactly when + +`L2 Z1 R2 + L4 Z2 R4 = A+B`. + +This equation has no products of unknown entries. Every xj occurs in two +full calls, so all exponents lie in `{0,1,2}^3`. Comparing all 27 monomials +and all 64 matrix entries produces exactly 1,728 equations on 128 unknown +binary entries. Zero equations are retained. No coefficient is discarded. + +`algebra.build_system` constructs each column by substituting a single +matrix unit into one aggregate. It constructs A independently from the three +stage projectors, checks the e-free endpoint, and computes the discrepancy +A+B from the six calls. Every matrix is represented by eight packed binary +rows; no floating arithmetic is used. + +## Complete finite domain + +Binary row elimination on the augmented system finds 104 pivots and 24 free +coordinates. Back substitution constructs one particular solution z0 and +one homogeneous vector vj for each free coordinate. The verifier checks the +particular and all homogeneous vectors in the original coefficient system. +Each vj has free coordinate j equal to one and every other free coordinate +zero, as follows directly from its construction. Consequently every solution +has a unique representation + +`z = z0 + sum_(j=0..23) bj vj`, with `bj in F2`. + +The loop runs through all 24-bit reflected Gray words. At step i>0 the bit +that changes is the least significant set-bit position of i, so XORing the +corresponding vj visits every assignment once. It visits exactly `2^24` +solutions. Eight-row binary elimination computes both aggregate ranks at +every step. The resulting complete histogram has no pair with rank sum below +eight and has pairs of ranks `(4,4)`. Stdout includes that histogram and the +reconstructed affine basis rather than trusting a saved search verdict. + +The finite calculation therefore certifies + +`rank(Z1)+rank(Z2) >= 8` + +for every feasible binary aggregate pair. It says nothing about assigning +nonbinary extension-field values to the free coordinates. + +## Query count and attainment + +If burst i contains ki rank-one queries, matrix rank subadditivity gives +`rank(Zi) <= ki`. Thus `k1+k2 >= 8` for every complete word in this schedule. +This implication permits repeated factors, any number of factors and any +binary entries; it does not assume that either aggregate is square zero. + +PR #5699 supplies four rank-one square-zero factors in each burst. The new +verifier reads those cited factors, checks each rank and square, checks their +aggregate sums, and substitutes the two sums into every endpoint coefficient. +They give eight queries, proving attainment. The construction and its credit +remain with the predecessor. The new contribution is the exhaustive lower +bound for the fixed schedule, not an audit of its earlier gap optimum. + +## Implementation bounds and verification limits + +All loops have fixed finite bounds: matrices have eight rows, polynomials at +most 27 monomials, the coefficient system has 1,728 rows and 128 columns, and +the exhaustive loop has exactly 16,777,216 iterations. Row elimination is +iterative. Functions are below 60 physical lines. Checks use explicit failures +and remain enabled under `-O`. + +Python's managed allocation is a documented Power of Ten deviation. The +enumeration holds one 128-bit solution, 24 basis vectors, two eight-row rank +bases, and an 81-entry histogram. It never retains the solution list. Polynomial +and system storage are bounded by the fixed dimensions above. Each source +input is bounded by one MiB. The standard-library JSON parser and Python +runtime allocate internally; no claim of allocation-free execution is made. +The one local module is loaded by its explicit sibling path so isolated and +Git-free execution use the same code. No recursion, external solver, subprocess +or network call occurs in the verifier. Warning-strict normal and optimized +registered runs provide the available runtime diagnostics; no Python static +type-checker certification is claimed. + +Controls cover invalid row encoding, changed full order and gaps, a damaged +aggregate, a rank-one factor that is not square zero, an inconsistent system, +an altered endpoint, a constant-only false positive and a small Gray-domain +enumeration. All 512 three-by-three binary matrices also receive an independent +kernel-cardinality rank check with five identity coordinates. + +This does not establish a field-uniform obstruction, a new native word, +physical restoration, a favorable supplier invoice or any multiplication +theorem. All five selected framework assumptions remain separate. diff --git a/research/two-burst-thin-rank/README.md b/research/two-burst-thin-rank/README.md new file mode 100644 index 0000000000..9e744af158 --- /dev/null +++ b/research/two-burst-thin-rank/README.md @@ -0,0 +1,90 @@ +# Eight thin queries are necessary in the saved two-burst schedule + +**Finite certificate over F2; no new kappa.** Fix the six full matrices from +Ali Romman's PR #5673, in order `(1,3,2,4,0,5)`, and permit constant thin +queries only after two and four full calls. Every complete word requires at +least eight rank-one thin queries. The eight square-zero queries in +[theon199's PR #5699](https://github.com/CrocSwap/integer-mult-bounds/pull/5699) +attain this minimum. + +The new result is the lower bound for that fixed schedule. PR #5699 proved +that two occupied gaps are optimal and explicitly left the thin-query count +open. This answers its first next question on its saved gap pair, not on every +two-gap schedule. Coefficient changes at these gaps cannot produce seven queries. + +## Evidence and scope + +Consecutive thin queries aggregate to two arbitrary binary matrices Z1,Z2. +The complete polynomial endpoint gives 1,728 binary equations on their 128 +entries. Exact elimination has rank 104 and leaves 24 free coordinates. The +verifier enumerates all **16,777,216** solutions and finds + +`min(rank(Z1) + rank(Z2)) = 8`. + +Subadditivity of matrix rank makes this a lower bound on the number of +rank-one factors, even without imposing square zero. The cited construction +attains it with legal square-zero factors. [PROOF.md](PROOF.md) explains the +reduction, completeness and finite claim. No predecessor verifier is imported. + +The computation includes every coefficient of every matrix entry, not only +constant or first mixed coefficients. It checks the attaining source data, +512 independent kernel/rank cases, and nine boundary, rejection or enumeration +controls. Stdout is a generated receipt with the affine basis, complete rank-pair +histogram, and SHA256 hashes of package files and live inputs. It writes nothing. + +This is neither a search failure nor a complete multiplication theorem. +Extension fields, changed full matrices, other full-call orders, other gaps, +additional gaps, stage-dependent thin entries, native lifts and physical +implementation are outside the certificate. No current supplier, complete +invoice, selected frontier or framework assumption changes. The predecessor's +optimistic invoice remains a separate cited limitation; it is not replayed here. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/two-burst-thin-rank/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/two-burst-thin-rank/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/two-burst-thin-rank +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/two-burst-thin-rank --check-source-history +``` + +Use the corresponding CPython 3.12 path on another machine. Both registered +commands enumerate the entire domain. Expected status is +`PASS_TWO_BURST_THIN_RANK`, with 16,777,216 solutions and minimum rank sum eight. +The registered runner also checks metadata and pins. Publication-byte and +source-history checks require a committed package and full Git history. +The standalone verifier also works in a source export without Git or network. + +## Open next questions + +- Can different gaps, another full-call order or more occupied gaps admit seven + binary queries? Start from the changed full coefficient system. A positive + word needs every coefficient, not a sampled endpoint. No broader search is + included, and a favorable complete invoice must precede supplier expansion. +- Does the rank-sum bound persist over characteristic-two extension fields? + The same affine equations define a symbolic problem, but the enumeration here + assigns binary values only. A field-uniform rank argument remains open. + +## Credit and provenance + +This result was produced by Nick Petalas. New work is Apache-2.0. Independent +human and formal proof-kernel review are unclaimed. + +Credit GitHub contributor **theon199** for PR #5699's two-burst construction, +saved witness and explicit question. Credit **Ali Romman** for +[PR #5673](https://github.com/CrocSwap/integer-mult-bounds/pull/5673), its full +matrices, normalized escape-word model and original construction. Retain +**Cinna Davis** and the PR #5617/#5631/#5649 controller lineage, P104/native/helper/ +compiler contributors and every unchanged predecessor notice. Classical binary +elimination, rank subadditivity and Gray enumeration are not claimed as new. + +[SOURCES.json](SOURCES.json) pins the exact retained main inputs at +`de5ec2e7a6074068452f45b1a191b5c72832df4a`. The catalogue and selected record +are historical provenance. The three explicit predecessor files are live +inputs; the verifier checks their hashes without importing predecessor code. +[TASK.json](TASK.json) records the changed card scope and overlap coverage. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216167) +and [finite-field clarification](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216231) +record the bounded assignment and result. diff --git a/research/two-burst-thin-rank/SOURCES.json b/research/two-burst-thin-rank/SOURCES.json new file mode 100644 index 0000000000..d42642df19 --- /dev/null +++ b/research/two-burst-thin-rank/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/connector-single-burst/CERTIFICATES.json", + "usage": "input", + "git_blob": "7bf2a4c2c3a290479e32ae45c9be4f79a901ae35", + "sha256": "d33ebf9171c45a4e164cab5040acca7621ea6dea4f8890fd696977b42d788cab" + }, + { + "path": "research/connector-single-burst/README.md", + "usage": "input", + "git_blob": "24763c2abafb87d6539e4da84dd8b1f3c312e23b", + "sha256": "3485cca5df60b34686e9c8783d41f7a69168551c90a9f708f66ac65aba9d614b" + }, + { + "path": "research/connector-single-burst/SOURCE-WORD.json", + "usage": "input", + "git_blob": "aae71c6ad294d6bc9ca5e2216a7785b9e6611afd", + "sha256": "20285745b7a6c4bfefcccc365caacefaf982d30adb60fea29ffa14f0ea6b639c" + } + ] +} diff --git a/research/two-burst-thin-rank/TASK.json b/research/two-burst-thin-rank/TASK.json new file mode 100644 index 0000000000..204a06c53d --- /dev/null +++ b/research/two-burst-thin-rank/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Determine the minimum binary rank-one thin-query count at the saved PR5699 full order (1,3,2,4,0,5), with bursts only after two and four full calls.", + "scope_change_reason": "The card asks for a new connector operation. The explicit open question in PR5699 instead asks whether its fixed full matrices can use fewer than eight thin queries. This package isolates the saved two-burst schedule and proves a finite binary obstruction, rather than expanding an operation alphabet.", + "bottleneck_link": "Scoped chronological budget result. Coefficient changes alone at these fixed gaps cannot reduce the thin-query count from eight to seven; a proposed improvement must change the schedule or another stated premise. No complete supplier or kappa improvement follows.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original fixed-schedule improvement; do not enumerate other full orders, gaps or fields.", + "outcome": "completed", + "evidence": "The verifier reconstructs all 1728 coefficient equations, derives rank 104 and 24 free binary coordinates, enumerates all 16777216 solutions and obtains minimum aggregate rank sum eight. The cited eight-query square-zero construction attains the bound.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a different gap pair, full-call order or additional occupied gap use seven binary rank-one thin queries with these full matrices?", + "why_it_matters": "Those changes are necessary to evade this fixed-schedule certificate.", + "first_step": "Construct the changed complete coefficient system and seek an attaining word; preserve all original input columns.", + "blocked_by": "No changed-schedule result is supplied here. A favorable complete invoice is required before any supplier expansion." + }, + { + "question": "Does the rank-sum bound eight persist over characteristic-two extension fields?", + "why_it_matters": "The binary exhaustive certificate does not decide this stronger algebraic question.", + "first_step": "Use the two aggregate matrices and exact coefficient system as a symbolic rank-minimization problem.", + "blocked_by": "The 24 free parameters are enumerated over F2 only." + } + ], + "claim_type": "finite certificate", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216167", + "scope_update_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216231", + "predecessors": [ + { + "pr": 5699, + "author": "theon199", + "role": "two-burst construction and explicit open question" + }, + { + "pr": 5673, + "author": "Ali Romman", + "role": "six full matrices, normalized escape-word model and original eight-query word" + } + ], + "freshness": { + "canonical_main": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "priority_revision": 8, + "checked_utc": "2026-10-27T11:59:22Z", + "coverage": "448 open PR bodies and 5381 Discussion records, with complete remote pagination; sparse local overlap searched 219 of 7845 HEAD notes. Separate distinctive all-main README and merged-PR searches were also used. Unpublished work is outside this coverage." + } +} diff --git a/research/two-burst-thin-rank/VERIFY.json b/research/two-burst-thin-rank/VERIFY.json new file mode 100644 index 0000000000..a8ce9328df --- /dev/null +++ b/research/two-burst-thin-rank/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/connector-single-burst/CERTIFICATES.json", + "research/connector-single-burst/README.md", + "research/connector-single-burst/SOURCE-WORD.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "All 16777216 binary aggregate pairs, all endpoint coefficients, rank lower bound, cited attaining word and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "The same complete finite domain and contracts with assertions disabled." + } + ] +} diff --git a/research/two-burst-thin-rank/algebra.py b/research/two-burst-thin-rank/algebra.py new file mode 100644 index 0000000000..adb2dc87bf --- /dev/null +++ b/research/two-burst-thin-rank/algebra.py @@ -0,0 +1,155 @@ +"""Bounded binary coefficient algebra for the fixed two-burst question.""" + +from itertools import product + +SIZE = 8 +MASK = (1 << 64) - 1 +IDENTITY = sum(1 << (9 * i) for i in range(SIZE)) +EXPONENTS = tuple(product(range(3), repeat=3)) +ZERO = (0, 0, 0) +VARIABLES = 128 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def pack(rows): + require(isinstance(rows, list) and len(rows) == SIZE, "matrix row count") + require(all(type(r) is int and 0 <= r < 256 for r in rows), "binary row") + return sum(r << (8 * i) for i, r in enumerate(rows)) + + +def multiply(left, right): + result = 0 + for i in range(SIZE): + row = 0 + for j in range(SIZE): + if (left >> (8 * i + j)) & 1: + row ^= (right >> (8 * j)) & 255 + result |= row << (8 * i) + return result + + +def rank(word): + basis = [0] * SIZE + result = 0 + for i in range(SIZE): + row = (word >> (8 * i)) & 255 + for _ in range(SIZE): + if row == 0: + break + pivot = row.bit_length() - 1 + if basis[pivot] == 0: + basis[pivot] = row + result += 1 + break + row ^= basis[pivot] + return result + + +def add_polynomials(left, right): + require(len(left) <= 27 and len(right) <= 27, "polynomial capacity") + out = dict(left) + for exponent, value in right.items(): + out[exponent] = out.get(exponent, 0) ^ value + return {exponent: value for exponent, value in out.items() if value} + + +def multiply_polynomials(left, right): + require(len(left) <= 27 and len(right) <= 27, "polynomial capacity") + out = {} + for x, a in left.items(): + for y, b in right.items(): + exponent = tuple(x[i] + y[i] for i in range(3)) + require(all(v <= 2 for v in exponent), "coefficient degree") + out[exponent] = out.get(exponent, 0) ^ multiply(a, b) + return {exponent: value for exponent, value in out.items() if value} + + +def encode(polynomial): + require(set(polynomial) <= set(EXPONENTS), "coefficient domain") + return sum(polynomial.get(e, 0) << (64 * i) for i, e in enumerate(EXPONENTS)) + + +def full_gate(call): + stage = call["stage"] + require(type(stage) is int and 0 <= stage < 3, "full stage") + p, r = pack(call["p"]), pack(call["r"]) + exponent = tuple(int(i == stage) for i in range(3)) + return {ZERO: IDENTITY, exponent: p}, {ZERO: r, exponent: r} + + +def full_product(calls, order): + base, error = {ZERO: IDENTITY}, {} + for index in order: + a, b = full_gate(calls[index]) + error = add_polynomials(multiply_polynomials(a, error), + multiply_polynomials(b, base)) + base = multiply_polynomials(a, base) + return base, error + + +def build_system(calls, order, gaps): + require(len(calls) == 6, "six full calls") + require(order == [1, 3, 2, 4, 0, 5], "fixed full order") + require(gaps == [2, 4], "fixed occupied gaps") + base, error = full_product(calls, order) + wanted = {ZERO: IDENTITY} + for stage in range(3): + p = pack(calls[2 * stage]["p"]) ^ pack(calls[2 * stage + 1]["p"]) + exponent = tuple(int(i == stage) for i in range(3)) + wanted = multiply_polynomials({ZERO: IDENTITY, exponent: p}, wanted) + require(base == wanted, "pure stage endpoint") + columns = [] + for gap in gaps: + prefix, _ = full_product(calls, order[:gap]) + suffix, _ = full_product(calls, order[gap:]) + for j in range(64): + column = multiply_polynomials(suffix, multiply_polynomials( + {ZERO: 1 << j}, prefix)) + columns.append(encode(column)) + return columns, encode(add_polynomials(wanted, error)) + + +def linear_image(columns, vector): + require(len(columns) == VARIABLES and 0 <= vector < (1 << VARIABLES), + "linear image domain") + result = 0 + for j in range(VARIABLES): + if (vector >> j) & 1: + result ^= columns[j] + return result + + +def affine_space(columns, target): + require(len(columns) == VARIABLES, "system width") + require(all(0 <= c < (1 << 1728) for c in columns), "system column") + require(0 <= target < (1 << 1728), "system target") + basis = [0] * VARIABLES + for i in range(1728): + row = sum(((c >> i) & 1) << j for j, c in enumerate(columns)) + row |= ((target >> i) & 1) << VARIABLES + for j in range(VARIABLES): + if (row >> j) & 1: + if basis[j]: + row ^= basis[j] + else: + basis[j] = row + break + else: + require(row == 0, "inconsistent coefficient system") + for j in range(VARIABLES - 1, -1, -1): + if basis[j]: + for k in range(j): + if (basis[k] >> j) & 1: + basis[k] ^= basis[j] + free = [j for j, row in enumerate(basis) if row == 0] + particular = sum(((row >> VARIABLES) & 1) << j for j, row in enumerate(basis)) + null = [(1 << f) | sum(((row >> f) & 1) << j + for j, row in enumerate(basis)) for f in free] + require(linear_image(columns, particular) == target, "particular solution") + for vector in null: + require(linear_image(columns, vector) == 0, "homogeneous solution") + return particular, null, free diff --git a/research/two-burst-thin-rank/verify.py b/research/two-burst-thin-rank/verify.py new file mode 100644 index 0000000000..66ecfaab28 --- /dev/null +++ b/research/two-burst-thin-rank/verify.py @@ -0,0 +1,150 @@ +#!/usr/bin/env python3 +"""Enumerate the complete fixed-schedule binary aggregate solution space.""" + +import hashlib +import importlib.util +import json +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +SPEC = importlib.util.spec_from_file_location("two_burst_algebra", PACKAGE / "algebra.py") +ALGEBRA = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(ALGEBRA) +a = ALGEBRA + + +def authenticated_inputs(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + result = {} + for row in manifest["files"]: + if row["usage"] != "input": + continue + path = ROOT / row["path"] + a.require(path.stat().st_size <= 1024 * 1024, "input size") + raw = path.read_bytes() + a.require(hashlib.sha256(raw).hexdigest() == row["sha256"], "input digest") + result[path.name] = raw + a.require(len(result) == 3, "declared source inventory") + return result + + +def check_upper(calls, witness, columns, target): + a.require(witness["order"] == [1, 3, 2, 4, 0, 5], "upper full order") + a.require(witness["gaps"] == [2, 4], "upper gaps") + matrices = witness["matrices"] + groups = witness["rank_one_queries"] + a.require(len(matrices) == len(groups) == 2, "upper burst inventory") + aggregate = 0 + for i in range(2): + matrix, total = a.pack(matrices[i]), 0 + a.require(len(groups[i]) == 4, "four attaining queries") + for rows in groups[i]: + query = a.pack(rows) + a.require(a.rank(query) == 1, "query rank") + a.require(a.multiply(query, query) == 0, "query square zero") + total ^= query + a.require(total == matrix, "attaining aggregate sum") + a.require(a.rank(matrix) == 4, "attaining aggregate rank") + aggregate |= matrix << (64 * i) + a.require(a.linear_image(columns, aggregate) == target, "all endpoint coefficients") + return aggregate + + +def check_rank(): + # Independent kernel cardinalities for every 3-by-3 matrix, with five + # identity coordinates. These cover all ranks and every pivot location. + for word in range(512): + rows = [(word >> (3 * i)) & 7 for i in range(3)] + kernel = sum(all((r & x).bit_count() % 2 == 0 for r in rows) + for x in range(8)) + expected = 8 - (kernel.bit_length() - 1) + embedded = rows + [1 << i for i in range(3, 8)] + a.require(a.rank(a.pack(embedded)) == expected, "kernel/rank control") + return 512 + + +def reject(function): + try: + function() + except ValueError: + return + raise ValueError("negative control accepted") + + +def controls(calls, witness, columns, target, particular, null): + reject(lambda: a.pack([0] * 7 + [256])) + reject(lambda: a.build_system(calls, list(reversed(witness["order"])), [2, 4])) + reject(lambda: a.build_system(calls, witness["order"], [1, 4])) + broken = json.loads(json.dumps(witness)) + broken["matrices"][0][0] ^= 1 + reject(lambda: check_upper(calls, broken, columns, target)) + broken = json.loads(json.dumps(witness)) + broken["rank_one_queries"][0][0] = [1] + [0] * 7 + reject(lambda: check_upper(calls, broken, columns, target)) + reject(lambda: a.affine_space([0] * 128, 1)) + a.require(a.linear_image(columns, particular ^ 1) != target, + "changed aggregate must lose endpoint") + # A constant-only screen accepts this altered pair; higher coefficients reject it. + changed = particular ^ 1 ^ (1 << 64) + discrepancy = a.linear_image(columns, changed) ^ target + a.require(discrepancy != 0 and discrepancy & a.MASK == 0, + "constant-only false positive") + small = [0] + value = 0 + for i in range(1, 8): + value ^= null[(i & -i).bit_length() - 1] + small.append(value) + a.require(len(set(small)) == 8, "Gray enumeration control") + return 9 + + +def enumerate_pairs(particular, null): + a.require(len(null) == 24, "complete 24-dimensional domain") + histogram = [[0] * 9 for _ in range(9)] + current = particular + for index in range(1 << 24): + if index: + current ^= null[(index & -index).bit_length() - 1] + left = a.rank(current & a.MASK) + right = a.rank(current >> 64) + a.require(left + right >= 8, "rank-sum lower bound failed") + histogram[left][right] += 1 + a.require(sum(map(sum, histogram)) == (1 << 24), "complete enumeration count") + a.require(histogram[4][4] > 0, "attaining rank pair") + return {f"{i},{j}": count for i, row in enumerate(histogram) + for j, count in enumerate(row) if count} + + +def main(): + a.require(sys.version_info >= (3, 12), "Python 3.12 required") + inputs = authenticated_inputs() + source = json.loads(inputs["SOURCE-WORD.json"]) + calls = source["calls"][:6] + witness = json.loads(inputs["CERTIFICATES.json"])["two_burst"] + columns, target = a.build_system(calls, witness["order"], witness["gaps"]) + particular, null, free = a.affine_space(columns, target) + a.require(len(free) == 24, "coefficient rank 104") + check_upper(calls, witness, columns, target) + rank_cases = check_rank() + control_count = controls(calls, witness, columns, target, particular, null) + histogram = enumerate_pairs(particular, null) + hashes = {path.name: hashlib.sha256(path.read_bytes()).hexdigest() + for path in sorted(PACKAGE.iterdir()) if path.is_file()} + result = {"status": "PASS_TWO_BURST_THIN_RANK", "field": "F2", + "full_order": witness["order"], "gaps": witness["gaps"], + "coefficient_equations": 1728, "coefficient_rank": 104, + "free_coordinates": free, "particular": hex(particular), + "null_basis": [hex(v) for v in null], "solutions": 1 << 24, + "minimum_rank_sum": 8, "attaining_square_zero_queries": 8, + "rank_pair_histogram": histogram, "rank_controls": rank_cases, + "negative_and_enumeration_controls": control_count, + "package_sha256": hashes, + "input_sha256": {name: hashlib.sha256(raw).hexdigest() + for name, raw in sorted(inputs.items())}} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()