Certify eight-query minimum for the saved binary two-burst schedule

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.

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.

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

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

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