[JosieElliston]

Change and mathematical scope

This PR adds an independent audit of #6122 (Nick Petalas, head e4fb5699c1) in
research/four-block-query-capacity-audit/, plus two proved extensions. It makes no κ claim, and the
supplier and selected record are unchanged. The model is #6122's throughout. K has characteristic two, Q is a
central involution, free maps are constant GL_n(K), and each paid call is I + QN with N² = 0 and rank N ≤ r.
There is no workspace, and the target is Q I_n.

• Prove exact four-query capacity 2 floor(4r/3) (no new κ) #6122's theorem holds. I re-derived the normalization, the trace parity, the Gram factorization, the block
  idempotents and the rank count, and found no gap.

• Its finite check never reached the new step. Prove exact four-query capacity 2 floor(4r/3) (no new κ) #6122 exhausts n ≤ 4. Every case it decides there is already
  settled by parity or by the elementary bound n ≤ 3r. The first case that needs the new bound 3n ≤ 2S is
  n = 6, r = 2: "four rank-two queries cannot twist six." This package decides it by stdlib exhaustion over F2.

• Exhaustion over F2, n = 2..6, all 75 cap profiles. For per-call caps (c1..c4), a witness exists exactly
  when n is even and Σ min(c_j, n/2) ≥ 3n/2. The decider does not use the Gram argument. It puts R1 in
  conjugation normal form, enumerates every R2, applies a rank filter, and tests membership in {R3 + R4} once per
  similarity class, using the complete invariant rank p(Y)^k.

• Corollary, proved for all fields: heterogeneous caps. Four calls with caps c_j reach Q I_n iff n is even
  and Σ min(c_j, n/2) ≥ 3n/2. The omission schedule takes unequal omission counts; 16,559 such words are replayed.

• Extension, proved for all fields: every call count k ≥ 3. This answers Prove exact four-query capacity 2 floor(4r/3) (no new κ) #6122's Open next question 2. Let
  m_k = 2⌊(k−1)/2⌋. Then k calls of rank ≤ r reach Q I_n iff

  n is even and n + ⌈n/m_k⌉ ≤ k r
  

  The least total rank is n + ⌈n/m_k⌉.

  • Lower bound: Prove exact four-query capacity 2 floor(4r/3) (no new κ) #6122's Gram lemma with K summands, padding odd k with a zero call. For odd k the elementary
    bound already gives the same inequality, so the new step matters exactly for even k.
  • Construction: the explicit n + 1 rank-one simplex, R_i = e_i(1 − e_i)^T plus J, in blocks, placed on calls
    by wrap-around. 353 words are replayed for k = 3..9 and r = 1..6.
  • Consequences: five rank-two calls twist eight coordinates, against four with four calls. The paid rank per
    coordinate falls from 3/2 (k = 4) to 5/4 (k = 5, 6) and toward 1 as k grows.
  • Agreement checks: the k = 4 case equals 2⌊4r/3⌋, and rank-one calls reproduce the n + 1 minimum.
  • Predecessor: the extreme odd case n = (k−1)r is Ali Romman's block simplex at the shortest count (Prove stage-reuse and intersection cuts for complete callers #5617 §9).

Not covered: exhaustion beyond F2 or beyond n = 6, workspace, non-square-zero paid matrices, mixed caps for k ≠ 4,
and any native realization, invoice or κ.

Task and overlap

The drawn track was independent-verification. Following the coordinator's advice to audit a fresh, unreviewed
open PR, this package keeps #6122's card, joint-query-controller. TASK.json records the scope change.
Base: 721c03822c421b7f7fcbb2598993b947c4d88419. At submission, #6122 had no comments or reviews, and the
refreshed overlap cache and open PRs showed no other audit of it. The merged square-zero packages use different
alphabets or targets. Concurrent sessions are working on #6097 and other areas, which do not overlap this one.

Validation

python3.12 -B research/four-block-query-capacity-audit/verify.py
python3.12 -B scripts/research_package.py --package research/four-block-query-capacity-audit

• The verifier uses only the standard library, imports nothing from Prove exact four-query capacity 2 floor(4r/3) (no new κ) #6122 or the repository, and takes about
  30 s.
• It passes on Python 3.10, 3.12 and 3.14, in normal and -O modes. RESULT.json is compared in full.
• There are 13 positive and negative controls: false witnesses, an odd-trace target, dropped or swapped layers, a
  rank-cap violation, missing constants, and constructor refusals.
• Prove exact four-query capacity 2 floor(4r/3) (no new κ) #6122's own verifier was read and run, and it passes.
• Local SAT searches (python-sat in a research venv, not submitted) agree on the positive cases.
• An independent read-only OpenAI Codex review found no error in either proof. It found one verifier defect: the
  non-identity-target path wrongly fixed R1 in normal form. That is fixed, and the controls were moved.
• No selected-result replay was run, because nothing selected changes.

Open next questions

1. Do five or more calls pay in a real invoice? Price the k = 5, n = 8, r = 2 word under a per-call cost rule.
2. Can workspace or non-square-zero paid matrices beat n + ⌈n/m_k⌉? The Gram step starts from Σ R_i = I_n
   exactly.

Credit

The four-call theorem, its proof and the omission schedule are by Nick Petalas (#6122). The n + 1 simplex is
from Cinna Davis / 1337isnot1337 (research/productive-controller-basis-search/GLOBAL-PROOF.md). The Gram
framework and the block simplex at the shortest count are by Ali Romman (#5617). The source question is
Matarener's #6114. The audit and extensions are by Josie Elliston, prepared with Claude Code (Opus 5.5).
Apache-2.0.

🤖 Generated with Claude Code