From c68b405f5151940da51b3e762e8c309aefc34839 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 4 Nov 2026 12:31:44 -0800 Subject: [PATCH] Independently audit source6717 far-endpoint leakage; conditional written review, no kappa --- .../ADVERSARIAL-REVIEW.md | 145 +++++++ .../AUDIT-RECEIPT.json | 24 ++ .../p104-far-endpoint-leakage-review/NOTICE | 5 + .../README.md | 25 ++ .../REVIEW.md | 70 +++ .../SOURCE-PINS.json | 26 ++ .../TASK.json | 106 +++++ .../inputs/6717-PROOF.md | 399 ++++++++++++++++++ .../inputs/6717-README.md | 68 +++ .../inputs/6717-TASK.json | 129 ++++++ 10 files changed, 997 insertions(+) create mode 100644 research/p104-far-endpoint-leakage-review/ADVERSARIAL-REVIEW.md create mode 100644 research/p104-far-endpoint-leakage-review/AUDIT-RECEIPT.json create mode 100644 research/p104-far-endpoint-leakage-review/NOTICE create mode 100644 research/p104-far-endpoint-leakage-review/README.md create mode 100644 research/p104-far-endpoint-leakage-review/REVIEW.md create mode 100644 research/p104-far-endpoint-leakage-review/SOURCE-PINS.json create mode 100644 research/p104-far-endpoint-leakage-review/TASK.json create mode 100644 research/p104-far-endpoint-leakage-review/inputs/6717-PROOF.md create mode 100644 research/p104-far-endpoint-leakage-review/inputs/6717-README.md create mode 100644 research/p104-far-endpoint-leakage-review/inputs/6717-TASK.json diff --git a/research/p104-far-endpoint-leakage-review/ADVERSARIAL-REVIEW.md b/research/p104-far-endpoint-leakage-review/ADVERSARIAL-REVIEW.md new file mode 100644 index 0000000000..49df1d7fc7 --- /dev/null +++ b/research/p104-far-endpoint-leakage-review/ADVERSARIAL-REVIEW.md @@ -0,0 +1,145 @@ +# Adversarial static review of the far-endpoint leakage audit + +**Verdict: PASS for the stated conditional section6 audit; no unresolved +mathematical finding.** One scope qualification was raised and incorporated +before this final review: the characteristic-two control concerns the +displayed matrix hypotheses after deletion of the field restriction, not +a separately imposed genuine shortest-word condition. + +This review checks the algebra directly. It does not treat agreement with +another agent as proof. I read the coordinator derivation and the three +frozen source texts, but did not read the separate MATH-REVIEW, execute or +import mathematical code, run a proof kernel or contact the network. +Only this review file is authored by this reviewer. + +## Exact objects reviewed + +The source is thu-nmrc PR6717, current head +`3c9072b8738323dda9f9c7dfb421d578ed3fc17a`, particularly PROOF section6. + +| Object | SHA256 | +| --- | --- | +| Coordinator derivation, after characteristic-two qualification | `22e5e1fa64b2aba2a5d8d8df4f5f06c8f6313493778f33ac07f3a8d4222c6d6c` | +| 6717-PROOF.md | `9e108fdf827ffe92215be5e782f763a18968ce7613b66dfdd25a38f94958ce18` | +| 6717-README.md | `02fc8aa47e0f3b9ff042caad5f9049325f6b32dc4fff9d816136037b0402e188` | +| 6717-TASK.json | `67bce2c4caa1ff3fce659c5f7033ad1fad08c42f786efbfc749c6a3cedc20ca0` | + +The original coordinator draft is separately retained as +`COORDINATOR-DERIVATION-BEFORE-CHAR2-QUALIFICATION.md`. The correction is +scope wording, not a changed rank calculation or new computational result. + +## Kernel lemma and ordered leakage identities + +For an idempotent Q, `ker(I-Q)=im(Q)`. Therefore the retained column +subspace A0 has dimension `a-alpha`. Likewise `c=cQ` characterizes the +row space of Q, so the retained row subspace C0 has dimension `c-beta`. +The restriction of C0 to im(Q) is injective: vanishing on that image gives +`cQ=0`, and `c=cQ` then gives c=0. Consequently the map from im(Q) into +C0* has rank dim(C0). Its kernel contains A0 because every original row +in C annihilates every original column in A. Rank-nullity gives exactly + +`rank(Q) >= a+c-alpha-beta`. + +This uses actual kernels, so there is no unjustified simultaneous choice +of separately retained columns and rows. It works over arbitrary fields +and needs neither positive inner products nor simultaneous diagonalization. + +The leakage derivation also preserves matrix order. From `QU=U` and +`PQ=QP`, `PU=PQU=QPU`, hence `(I-Q)PU=0`. From `VQ=V`, +`VP=VQP=VPQ`, hence `VP(I-Q)=0`. Substituting P=E+F yields + +`(I-Q)EU=-(I-Q)FU`, `VE(I-Q)=-VF(I-Q)`. + +The two right sides each have rank at most rank(F)=e. Since the map +already vanishes on U, its image on span(U,EU) is precisely its image +on EU; there is no second q-dimensional leakage contribution. The +same argument applies to the row closure. Thus alpha,beta<=e is valid +without assuming any internal block commutation or e<=q. + +The decomposition rank(F)=rank(P)-2q remains an explicitly inherited +forced-projector premise. Given that premise, this argument makes no +additional rank-minimality assumption on P or Q. + +## Endpoint formulas, minors and all four pairings + +For the left endpoint, `v0=-tail0`. For odd i>=3, +`E_i e0=e_i+a_i` and `v0 E_i=-(e_i^T+tail_i)`. These follow directly +from `h_i e0=1`, `v_i e0=1`, `v0 e_i=-1` and `v0 a_i=1`. +The column minor on coordinates0,1 is +`[[1,1],[0,-1]]`, determinant -1. The row minor on coordinates1,i is +`[[-1,-1],[0,-1]]`, determinant1. Both are units over every field. + +The four pairings vanish separately: `v0 e0=0`, +`v0(e_i+a_i)=-1+1=0`, `(e_i^T+tail_i)e0=0`, and +`(e_i^T+tail_i)(e_i+a_i)=1-1=0`. The last row's overall minus sign +does not change zero pairing. + +For the right endpoint, `u_n=(-1,1,...,-1,1)^T` and `v_n=h`. +For odd i<=n-3, `h_i u_n=0`, `v_i u_n=-1` and `h a_i=0`, +so `E_i u_n=-a_i` and `h E_i=h_i`. The column minor of +`[u_n,-a_i]` on coordinates0,i+1 is +`[[-1,-1],[-1,0]]`, determinant -1. The row minor of `[h;h_i]` +on those coordinates is `[[1,1],[1,0]]`, also determinant -1. + +The four right pairings are `h u_n=0`, `h a_i=0`, +`h_i u_n=0`, `h_i a_i=0`: every relevant alternating sum has even +length. The dimensions and annihilation claims therefore hold with +no characteristic-zero counting assumption. Tensoring these fixed scalar +closure matrices with I_q gives dimensions2q and2q and zero pairing. +This does not tensor a scalar classification of arbitrary P or Q. + +A far endpoint exists at every allowed boundary. Odd i>=3 permits the +left endpoint; the remaining possibility i=1 permits the right because +n>=4 implies i<=n-3. In particular n=4,i=1 uses the right endpoint, +while n=4,i=3 and i=n-1 use the left. + +## Rank debt and written countercontrols + +Applying the kernel lemma gives `rank(Q)>=4q-2e`. Independently, +compatibility with a rank-q square-zero query gives rank(Q)>=2q: +its rank-q image and rank-q supported row space have zero pairing. +Writing rank(Q)=2q+f therefore gives `f>=max(0,2q-2e)`. +For e>=q, e+f>=q follows from f>=0. For 0<=e<=q, +e+f>=2q-e>=q. The remaining endpoint contributes another2q. +The sole-odd selected triple consequently has total rank at least7q. +Large e creates no sign or negative-dimension gap. + +All three written controls are valid at their stated scopes: + +1. At n=4,i=1, the left near endpoint satisfies `E_i e0=e0` + and `v0 E_i=v0`. Its two closures each have dimension1, so using + the left endpoint's supposed dimension2 here would be false. +2. Without CA=0, Q=I on K^2, A=K^2 and C=(K^2)* give + alpha=beta=0 but rank(Q)=2<4=a+c. Independent row/column + dimensions cannot simply be added without annihilation. +3. In characteristic two, five copies of `e0 e1^T` have rank1, + square zero and factors `I-2R_j=I=-I`; three copies of + `diag(1,1,0,0)` at distinct sites satisfy the displayed compatibility, + prefix and pairwise commutation conditions but have total rank6<7. + However, this five-query word is not genuinely shortest there: + the endpoint I has a zero-query realization. The amended coordinator + text correctly limits this control to deleting the field restriction + from the displayed matrix hypotheses. It is not a counterexample + to the field-independent leakage lemma or to a different theorem + imposing genuine minimality separately. + +## Scope, credit and remaining acceptance + +The coordinator accurately treats the complete shortest-query normal +form, canonical prefix formula, forced odd projector and compatibility +floor as inherited premises. This review independently checks the kernel +argument, ordered leakage application, endpoint closures and sole-odd +rank conclusion conditional on those premises. It does not certify the +source's even-interior branch, two-odd branch, normal-form derivation, +all-n attaining word, physical Gaussian/native implementation or invoice. + +The source's rank threshold and application remain thu-nmrc's work with +substantial OpenAI Codex assistance. Ali Romman's PR6398 and retained +alternating-caller-closure tools, complete coupled normal form, Cinna +Davis's query/controller lineage and all earlier notices retain credit. +The review is a classical linear-algebra audit, not invention of a new +general rank lemma. This separate AI review gives no independent human +acceptance, proof-kernel certification, κ improvement, selected-frontier +change or discharge of the five framework assumptions. + +No further correction is requested for the reviewed final derivation. diff --git a/research/p104-far-endpoint-leakage-review/AUDIT-RECEIPT.json b/research/p104-far-endpoint-leakage-review/AUDIT-RECEIPT.json new file mode 100644 index 0000000000..0d7ba1ee45 --- /dev/null +++ b/research/p104-far-endpoint-leakage-review/AUDIT-RECEIPT.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "CONDITIONAL_WRITTEN_REVIEW_NO_GAP_FOUND", + "scope": "Source6717 PROOFsection6 only; inherited canonicalnormalform/prefix/forcedprojector/floor, otherbranches/attaineroutside", + "source_head": "3c9072b8738323dda9f9c7dfb421d578ed3fc17a", + "proof_review_sha256": "22e5e1fa64b2aba2a5d8d8df4f5f06c8f6313493778f33ac07f3a8d4222c6d6c", + "adversarial_review_sha256": "4c144fea94d0b51ffe3e371b092f450b621b80af17490c6c316bc20452394cc1", + "separate_source_aware_written_review_sha256": "c9d7d0e7c1bd239d84567472d729a112a6fcb5193f0a83ca5f4df83ef86401f9", + "scientific_commands": [], + "source_or_new_program_execution": false, + "proof_kernel": false, + "finite_grid_claim": false, + "written_scope_controls": [ + "nearendpointclosurecollapses", + "zeropairingnecessary", + "char2displayedmatrixhypothesesextensionfails; notgenuinelyshortestthere" + ], + "pre_freeze_correction": "char2minimalityqualification; earlierlocaldraftretained", + "source_author_REVIEW_seen_by_scout": true, + "no_blind_or_human_acceptance": true, + "no_new_kappa": true, + "all_five_selected_assumptions_retained": true, + "frozen_at": "2026-11-04T20:30:05.241607+00:00" +} diff --git a/research/p104-far-endpoint-leakage-review/NOTICE b/research/p104-far-endpoint-leakage-review/NOTICE new file mode 100644 index 0000000000..15ee5a72e0 --- /dev/null +++ b/research/p104-far-endpoint-leakage-review/NOTICE @@ -0,0 +1,5 @@ +New external review: ToikY with substantial OpenAI Codex assistance. Apache-2.0. +Original uniform mixed-rank7q theorem, leakage application and attaining family: thu-nmrc PR6717 with substantial OpenAI Codex assistance. +Retained scalar obstruction/forced projector/closure/image-row methods and all-length alternating-caller tools: Ali Romman PR6398 and original contributors. Complete coupled normalform and Cinna Davis query/controller lineage retain their credit. +The source inputs are exact unchanged copies with their original attribution and notices; SOURCE-PINS.json binds them to source6717 head3c9072b8738323dda9f9c7dfb421d578ed3fc17a. +Kernel/annihilator/rank-nullity methods are classical. Separate AI review is not independent human or proof-kernel acceptance. diff --git a/research/p104-far-endpoint-leakage-review/README.md b/research/p104-far-endpoint-leakage-review/README.md new file mode 100644 index 0000000000..71f35650c8 --- /dev/null +++ b/research/p104-far-endpoint-leakage-review/README.md @@ -0,0 +1,25 @@ +# Independent review of the far-endpoint leakage argument + +**No gap found in PR6717 PROOF §6 under its enumerated canonical-source premises.** This external written audit answers the source README's independent-review request. It verifies only the sole-odd-interior-site plus both-endpoints case of thu-nmrc's uniform coupled stage-rank theorem at exact head `3c9072b8738323dda9f9c7dfb421d578ed3fc17a`. The theorem/construction remain predecessor credit. No new kappa or selected-frontier change. + +[REVIEW.md](REVIEW.md) supplies a direct kernel/rank-nullity proof of the zero-paired leakage inequality, including injectivity of row restriction to im(Q). Applying the two actual ordered leakage equations gives rank(Q)>=4q-2e for arbitrary coupled P,Q, without tensoring the unknown projectors or assuming rank minimality. Unit minors and all four pairings verify the far closures for every even n>=4, q>=1 over the allowed fields. The n4/i1 and n4/i3 endpoint choices are explicit; e+f>=q covers every possible extra rank. + +Three **written, unexecuted** scope controls explain why the near endpoint, omitted zero pairing and a characteristic-two extension of the displayed source matrix hypotheses cannot be silently accepted. The char2 control is not a genuinely shortest word in that characteristic, so it does not refute a different statement with an additional genuine-minimality hypothesis or the abstract leakage lemma. + +The complete coupled normalform, canonical prefix and forced odd-projector facts remain inherited premises. The even-interior and two-odd branches, all-n attaining word, executable receipts and physical/native/price/owned-return/stock/precision/tape/compiler/recursive-outer applications are outside this review. All five selected framework assumptions remain. A stage-dimension inventory is not a complete supplier or paid-call lower bound. + +## Evidence and provenance + +Exact source PROOF/README/TASK copies and Git/SHA256 bindings are included. The coordinator's derivation was followed by a separate adversarial AI algebra check. A separately prepared AI written review corroborated the kernels/minors; that reviewer had read the author's REVIEW during scouting, so this is source-aware external review, not a blind or human review. The adversarial check corrected the char2 minimality qualification before the proof was frozen; the earlier local draft is retained in session receipts. + +No scientific code, original or new checker, matrix enumeration, numerical solver, compiler or proof kernel ran. There is no VERIFY.json and no registered scientific replay. File integrity, Git byte/mode equality and an inert manual archive/readback are provenance checks only. Repository CI, if present, is likewise not a proof replay. Read [SOURCE-PINS.json](SOURCE-PINS.json), the unchanged [source proof](inputs/6717-PROOF.md), [REVIEW.md](REVIEW.md) and [ADVERSARIAL-REVIEW.md](ADVERSARIAL-REVIEW.md) to inspect the result. + +Canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision8 and authoritative selected6030 were refreshed; the priority prose still names an older record. TASK.json retains the picker card and declares the change from formal-interface-lemma to a narrower written source-bound proof review. Main/overlap/source status are refreshed again before submission. Neither absence of a matching body nor a DONE label establishes novelty or admission. + +## Open next questions + +Independently audit the normalform and prefix-to-forced-projector binding, then the other two rank-bound branches and all-n sharp attaining word at this same head. This matters because a valid §6 does not establish the complete theorem. Start with PROOF §§2–5 and7 and the retained original sources, after a new overlap checkpoint and budget. That work is unreserved. Physical supplier and complete invoice applications need their own exact caller/cost contracts; their unknown costs are not zero. + +## Credit + +thu-nmrc PR6717 supplies the uniform mixed-rank theorem, far-endpoint application and attaining family with substantial OpenAI Codex assistance. Ali Romman PR6398/alternating-caller-closure, complete coupled normalform authors, Cinna Davis's query/controller lineage and all retained contributors remain credited. The rank/kernel/annihilator tools are classical. External review: ToikY with substantial OpenAI Codex and separate AI review roles, Apache-2.0. This adds review evidence only; no human or proof-kernel acceptance. diff --git a/research/p104-far-endpoint-leakage-review/REVIEW.md b/research/p104-far-endpoint-leakage-review/REVIEW.md new file mode 100644 index 0000000000..6e323ed04f --- /dev/null +++ b/research/p104-far-endpoint-leakage-review/REVIEW.md @@ -0,0 +1,70 @@ +# Independent derivation: zero-paired leakage at a far endpoint + +External written audit of thu-nmrc PR6717, exact head `3c9072b8738323dda9f9c7dfb421d578ed3fc17a`, PROOF §6. Prepared by ToikY with substantial OpenAI Codex assistance, Apache-2.0. This is a source-bound proof review, not a new rank threshold or acceptance of the full theorem. No scientific program or proof kernel was run. + +## Contract and verdict + +**No gap found in §6 under the enumerated canonical-source premises.** The conclusion is that the sole-odd-site case contributes at least q extra stage dimensions: if the odd projector has rank 2q+e, one selected endpoint has rank 2q+f with e+f>=q. The other endpoint has rank at least 2q. This confirms this one branch of the source's 7q lower bound. The complete shortest-query normalization, canonical prefix formula, forced odd-projector fact and compatibility floor are inherited premises. We do not independently certify the even-interior branch, two-odd branch, all-n attaining word, physical realization or price. + +Let K be a commutative field with char(K) !=2, n>=4 even, q>=1, W=K^(nq). Work in the source's common canonical coefficient frame. The sole odd interior site is i in {1,3,...,n-1}. In scalar notation a_i=(1,-1,...,(-1)^i,0,...,0)^T, h=(1,...,1), h_i is the initial all-ones row through i, v_i=h_(i-1)-tail_i, E_i=e_i h_i+a_i v_i. Tensor these scalar expressions with I_q; arbitrary P,Q,F themselves need not be tensor products and their internal blocks need not commute. The inherited forced-projector statement is P=E+F, E=E_i tensor I_q, EF=FE=0, F idempotent and rank(F)=e=rank(P)-2q. The selected endpoint Q is idempotent, QU=U, VQ=V, [Q,P]=0, for its rank-q query factors U,V. All three selected stages are pairwise commuting under the source contract. + +## A general leakage lemma, proved directly + +Let Q be an idempotent on a finite-dimensional vector space W over any field. Let A<=W have dimension a and C<=W* have dimension c, with every c0 in C annihilating every a0 in A. Define + + alpha = rank((I-Q)|A), + beta = rank(C -> W*, c0 -> c0(I-Q)). + +Then + + rank(Q) >= a+c-alpha-beta. (L) + +Indeed A0=ker((I-Q)|A)=A intersect im(Q), so dim(A0)=a-alpha. Likewise C0=ker(c0->c0(I-Q))=C intersect row(Q), so dim(C0)=c-beta. Restriction C0 -> (im Q)* is injective: if c0 vanishes on im(Q), then c0=c0 Q=0. Therefore the row map im(Q) -> C0* has rank dim(C0), over every field. Its kernel contains A0 because CA=0. Rank-nullity gives rank(Q)>=dim(C0)+dim(A0), proving (L). The two retained spaces are chosen as actual kernels; no incompatible choices of 'most' columns and rows, orthogonal projection, positivity, simultaneous diagonalization or scalar classification is used. + +## Obtaining the leakage ranks from actual commutation + +For A=im[U,EU], C=row[V;VE], use QU=U and PQ=QP: + + (I-Q) P U = (I-Q) Q P U = 0. + +Substitute P=E+F to obtain (I-Q)EU=-(I-Q)FU. Similarly VP=VQP=VPQ, hence VP(I-Q)=0 and VE(I-Q)=-VF(I-Q). Each right-hand side has rank at most e. Since (I-Q)U=0, the image of (I-Q)|A is precisely the image of (I-Q)EU, not an additional q-dimensional U contribution. Thus alpha<=e. Since V(I-Q)=0, the row leakage map has image row(VE(I-Q)); beta<=e. Matrix order has been retained throughout. + +If a=c=2q and CA=0, (L) gives rank(Q)>=4q-alpha-beta>=4q-2e. This remains correct when 2q-e is negative; the exact kernel dimensions are nonnegative and the weaker displayed bound can simply be vacuous. Compatibility separately supplies rank(Q)>=2q. No assumption e<=q or rank-minimality is used here. + +## Checking the far-endpoint closure, including boundary n=4 + +All scalar indices below are zero based. The explicit formulas use unit minors, so their ranks do not depend on characteristic-zero arithmetic. + +Left endpoint: U=u0=e0 and V=v0=-tail_0. For odd i>=3, + + E_i e0=e_i+a_i, v0 E_i=-(e_i^T+tail_i). + +The columns e0 and e_i+a_i are independent by their coordinates 0 and 1: the second column has coefficient -1 at coordinate1 while e0 has zero there. The rows v0 and -(e_i^T+tail_i) are independent by coordinates1 and i, giving a determinant of absolute value1. All four pairings vanish: v0 e0=0; v0(e_i+a_i)=-1+1=0; (e_i^T+tail_i)e0=0; and (e_i^T+tail_i)(e_i+a_i)=1+(-1)=0. Thus a=c=2 and CA=0. + +Right endpoint: U=u_n=(-1,1,...,-1,1)^T and V=v_n=h. For odd i<=n-3, + + E_i u_n=-a_i, h E_i=h_i. + +The column pair u_n,-a_i has a unit minor at coordinates0,i+1; the row pair h,h_i has one at coordinates0,i+1. The four pairings are h u_n=0, h a_i=0, h_i u_n=0 and h_i a_i=0. Each vanishes by an even-length alternating sum, as n and i+1 are even. Again both closure dimensions are2 with zero pairing. + +Tensoring the verified scalar closure spaces with I_q gives dimensions2q,2q and zero pairing. This step tensors the fixed canonical U,V,E, not the arbitrary selected Q or its extra dimensions. + +A far endpoint always exists. If i>=3, use the left endpoint. Otherwise i=1 and n>=4 implies i<=n-3, so use the right. At n=4 the only odd cases are i=1 (right) and i=3 (left). This also covers i=n-1 using the left endpoint. No limiting argument or final-prefix substitution is required. + +## Rank debt and precise scope + +Write rank(Q)=2q+f. Compatibility gives f>=0 and the leakage bound gives f>=2q-2e. If e>=q, e+f>=q immediately. If 0<=e<=q, e+f>=2q-e>=q. Adding the untouched third stage floor2q gives the sole-odd selected-triple rank sum >=7q. This does not require that either of the odd and far-endpoint stages be rank-minimal. + +The lemma (L), its compatibility derivation and closure unit minors work over arbitrary fields; the stated characteristic restriction enters through the retained shortest-query/forced-prefix normalization. It must not be removed from the original theorem. + +## Written scope controls; no executable tests + +1. **Near endpoint is insufficient.** At n=4,i=1, E_i u0=e0 and v0 E_i=v0. Both left closure dimensions are only1, not2. The proof must choose the right endpoint. This prevents silently applying the far bound to the near endpoint. +2. **Zero pairing is necessary.** Let W=K^2, Q=I, A=W and C=W*. Then alpha=beta=0 and rank(Q)=2, while a+c=4. Dropping CA=0 from (L) gives a false bound. The independent row/column dimensions alone do not add. +3. **Characteristic two cannot be imported into the original theorem.** In char2 let n=4,q=1, R_j=e0 e1^T for all five queries and choose the same P=diag(1,1,0,0) at three distinct sites. Each R_j is square-zero rank1; I-2R_j=I and the five-query product is I=-I. P is compatible, each chronological prefix is I, and the selected projectors commute, but the total selected rank is6<7. The source's char!=2 hypothesis is substantive for its displayed matrix-hypothesis formulation. In characteristic two this five-query word is not genuinely shortest: -I=I already has a zero-query realization. Thus this control refutes deleting the field restriction from those displayed hypotheses; it does not refute a different theorem that separately imposes genuine minimality, nor the leakage lemma itself. This is a hand-derived boundary counterexample, not a machine-checked receipt. + +## Credit and remaining obligations + +The rank budget, far-endpoint leakage application and uniform construction belong to thu-nmrc PR6717 with substantial OpenAI Codex assistance. Ali Romman PR6398 and alternating-caller-closure supply the scalar obstruction, forced projector/closure method and retained all-length tools; the complete coupled normal form and Cinna Davis's query/controller lineage remain predecessor credit. The kernel/rank-nullity presentation is an external review of those implications using classical linear algebra, not a claim of a newly discovered general rank lemma. + +Remaining: independent review of the normal form/actual-prefix source bindings, the other two branches and all-n attaining word; native/helper physical realization, complete invoice, ownership/restoration, stock/precision/tape/compiler/recursive outer applications, and all five selected assumptions. No kappa/frontier change, supplier admission, human review or proof-kernel acceptance follows from this audit. diff --git a/research/p104-far-endpoint-leakage-review/SOURCE-PINS.json b/research/p104-far-endpoint-leakage-review/SOURCE-PINS.json new file mode 100644 index 0000000000..bff29fbc07 --- /dev/null +++ b/research/p104-far-endpoint-leakage-review/SOURCE-PINS.json @@ -0,0 +1,26 @@ +{ + "schema_version": 1, + "files": [ + { + "path": "inputs/6717-PROOF.md", + "source_path": "research/p104-coupled-three-stage-rank-budget/PROOF.md", + "commit": "3c9072b8738323dda9f9c7dfb421d578ed3fc17a", + "git_blob": "7e3b89f085f1fe1f15098b75e22e370efc6ce4ce", + "sha256": "9e108fdf827ffe92215be5e782f763a18968ce7613b66dfdd25a38f94958ce18" + }, + { + "path": "inputs/6717-README.md", + "source_path": "research/p104-coupled-three-stage-rank-budget/README.md", + "commit": "3c9072b8738323dda9f9c7dfb421d578ed3fc17a", + "git_blob": "ade3fb709f3d9cb0ba3f0d823726dfeb5ed4f18a", + "sha256": "02fc8aa47e0f3b9ff042caad5f9049325f6b32dc4fff9d816136037b0402e188" + }, + { + "path": "inputs/6717-TASK.json", + "source_path": "research/p104-coupled-three-stage-rank-budget/TASK.json", + "commit": "3c9072b8738323dda9f9c7dfb421d578ed3fc17a", + "git_blob": "919dd2a29bb1a1ddd5c9cabbb9d0f952dc37aaec", + "sha256": "67bce2c4caa1ff3fce659c5f7033ad1fad08c42f786efbfc749c6a3cedc20ca0" + } + ] +} diff --git a/research/p104-far-endpoint-leakage-review/TASK.json b/research/p104-far-endpoint-leakage-review/TASK.json new file mode 100644 index 0000000000..28e144c7df --- /dev/null +++ b/research/p104-far-endpoint-leakage-review/TASK.json @@ -0,0 +1,106 @@ +{ + "task_id": "formal-interface-lemma", + "scope_key": "e3ffea67887eeb4c396c/6717-section6-kernel-leakage", + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "priority_revision": 8, + "source_commit": "3c9072b8738323dda9f9c7dfb421d578ed3fc17a", + "scope_status": "changed", + "actual_scope": "Independent written audit of PR6717 PROOF section6 far-endpoint leakage for arbitrary coupled projectors, with endpoint/field boundary checks; normalform, forcedoddprojector and othercases/attainment remain outside.", + "scope_change_reason": "README explicit independent-review request; source quantified bridge merits an external algebraic review. Writtenproof only, no formal kernel or full supplier.", + "existing_checks": "Source own normal/O finite and independent-code checks plus authorAI REVIEW; not external unbounded review.", + "method": "Independently prove a coordinate-free zero-paired leakage lemma using kernel restrictions and injectivity, then inspect canonical endpoint closures and rank debt. Separate adversarial AI review.", + "success": "Each implication justified for all even n>=4,q>=1,char K !=2 under enumerated inherited normalform assumptions; else precise gap/counterexample.", + "stop_rule": "Stop at a failed closure/compatibility/field step or21:06:42UTC. No scientific execution or checker. Finish by21:21:42; at least15minutes verification afterfreeze.", + "milestone": "written scoped proof audit only", + "budget_minutes": 60, + "no_new_kappa": true, + "original_card": { + "task_id": "formal-interface-lemma", + "scope_key": "e3ffea67887eeb4c396c", + "handoff_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166", + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ], + "coverage_rule": "These checks have limited scopes. Empty coverage means unknown, not unstudied. Audit a missing implication or explicitly justify independent repetition.", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "method": "Audit a formal theorem-to-certificate binding independently.", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance.", + "coverage_context_matches_selected": false, + "open_handoffs": [], + "advisory_claims": [] + }, + "schema_version": 1, + "outcome": "completed", + "author": "ToikY", + "ai_assistance": "Substantial OpenAI Codex; separate source-aware AI written review and adversarial algebra review. No independent human or proof kernel.", + "evidence": "Written kernel/rank-nullity derivation, canonical endpoint unit minors, three written scope controls; no scientific commands.", + "bottleneck_link": "Independent scrutiny of one all-q causal-prefix rank implication in a pending coupled-stage inventory; side result with no physical price or frontier change.", + "open_questions": [ + { + "question": "Independently review the complete coupled normalform/prefix-to-forced-projector binding, other two lower-bound branches and all-n attaining word.", + "why_it_matters": "Section6 alone does not certify the whole7q theorem or its sharpness.", + "first_step": "At exact6717sourcehead, audit PROOF2-5 and7 against retained source pins.", + "blocked_by": "Needs its own overlap/budget and source-aware proof review; no work reserved." + } + ] +} diff --git a/research/p104-far-endpoint-leakage-review/inputs/6717-PROOF.md b/research/p104-far-endpoint-leakage-review/inputs/6717-PROOF.md new file mode 100644 index 0000000000..7e3b89f085 --- /dev/null +++ b/research/p104-far-endpoint-leakage-review/inputs/6717-PROOF.md @@ -0,0 +1,399 @@ +# A sharp all-even coupled stage-rank budget + +Prepared by **thu-nmrc with substantial OpenAI Codex assistance**. +Apache-2.0. This is a coefficient-space rank theorem, with no physical +native module, paid invoice, kappa increment, or scientific-acceptance claim. + +## 1. Statement and precise contribution + +Let K be a commutative field of characteristic different from two. +Let n>=4 be even and q>=1. On an nq-dimensional space let +R0,...,Rn be rank-q square-zero operators such that + + (I-2Rn) ... (I-2R0) = -I. + +Write T_i=I-2R_i and B_i=T_i ... T0. At three distinct selected sites +let P_i be idempotents satisfying + + P_i R_i = R_i P_i = R_i, [P_i,B_i]=0. + +Suppose the three selected P_i commute pairwise. Their ranks may exceed +the minimum2q; no rank-minimality assumption is made. + +**Theorem. The sum of the three selected ranks is at least7q. The bound +is attained for every even n>=4 and every positive q.** + +These are normalized ordinary coefficient-space operators in the shortest +query contract. The nq inputs are independent. No initialized extra main +input or discarded independent input is allowed. Arbitrary constant +ordinary basis changes mixing all nq coordinates are permitted through +the common normalization. Internal q-by-q coefficient blocks need not +commute. The prefix in the hypothesis is the actual complete chronological +query prefix, rather than merely the query at that site. + +This extends the n=4 result in PR6717. Ali Romman's PR6398 section2 already +proves the scalar local commuting-triangle obstruction for every evenn; +the scalar rank-sum-seven consequence is old. Its section3 supplies the +image/row rank inequality and the forced minimal odd projector +`A(CA)^(-1)C`, including scalar six-field closure tables. The complete +scalar and coupled shortest-query normal forms are also predecessor +results. Ali Romman's `alternating-caller-closure/PROOF.md` further treats +the fixed minimal odd interior at every evenn and everyq, with explicit +projector blocks, total curvature and a generic low-rank commutator +correction bound. Those all-length fixed-interior tools are retained as +well. None of those mechanisms is claimed as new here. + +The contribution is the **uniform all-even-n, all-q quantitative bound on +extra stage dimensions**, using odd-projector commutators and a rank-defect +estimate at a far endpoint, together with a literal all-n attaining word. +The generic low-rank commutator estimate itself is an inherited tool; +the new scope is its arbitrary-three mixed-rank threshold application +combined with endpoint leakage, rather than a fixed-interior exclusion. +The proof does not infer arbitrary coupled projectors by tensoring scalar +classifications. The q=2 rank13 compatibility-only example is retained +as a failed-prefix control, with its distinct contract made explicit. + +Original source files and notices are included unchanged in `inputs/`. +`SOURCES.json` pins their commits, Git blobs and SHA256 values, including +the exact published PR6717 proof. + +## 2. Retained normal form and rank lemma + +Factor each query as R_i=U_i V_i, with U_i of size nq byq, V_i of sizeq +by nq and V_i U_i=0. The retained complete coupled normal form gives + + V_i U_j = sign(i-j) I_q, i != j. + +Here is the source argument needed to specify its field scope. Concatenate +the factors into U,V; put G=VU and let L be its strict block-lower part. +Chronological expansion gives + + product_i (I-2R_i) = I-2U(I+2L)^(-1)V. + +Thus U(I+2L)^(-1)V=I. The matrix `(I+2L)^(-1)VU` is a rank-nq +projector, so Z=I+2L-G has rankq and diagonal blocks I_q. Write Z=AB +with inner dimensionq. Each A_i B_i=I_q makes both square blocks +invertible. Replacing U_i by U_i A_i and V_i by A_i^(-1)V_i gives the +displayed Gram. No matrix blocks are commuted. The leading even skew +sign matrix is invertible, yielding a common basis in which the full +tuple is the scalar canonical tuple tensored with I_q: + + u_i=e_i (0<=i= a+c-g. (1) + +Indeed the row map on im(P) has rank at leastc, and its kernel contains +an (a-g)-dimensional subspace of A. In particular a projector compatible +with a rank-q square-zero query has rank at least2q. + +All subsequent calculations take place in the canonical common basis. +They are unchanged by conjugating back to the original ordinary frames. +The symbol tensor I_q refers to coupling of coefficient ports, not to a +physical column-width or Gaussian phase lift. + +## 3. Uniform chronological prefixes + +For i= 4q. (3) + +Any selected triple containing such a site already has rank sum at +least8q, since every other compatible projector has rank at least2q. +It remains to treat odd interior sites and the two endpoints. + +## 5. Forced minimal odd projectors and extra dimensions + +For odd i, define the scalar rank-two projector + + E_i=e_i h_i+a_i v_i. + +Put A_i=(e_i,a_i) and C_i=(h_i;v_i). Since +`C_i A_i=I2`, E_i=A_i C_i is an idempotent of rank2. This is the +uniform expression for the predecessor's forced odd minimal projector. +The all-length fixed odd projector and explicit block mechanism is also +retained from `alternating-caller-closure`; this formula is not claimed +as a newly discovered minimal projector. + +Formula (2) gives + + B_i e_i=-e_i+2a_i, v_i B_i=2h_i-v_i. + +Thus compatibility and prefix commutation force P_i to contain A_i and +support C_i. Consequently, after tensoring with I_q, + + P_i E_i=E_i P_i=E_i, + F_i=P_i-E_i is an idempotent, + rank(F_i)=e_i^extra := rank(P_i)-2q >=0. (4) + +To avoid confusion, e_i without a superscript continues to mean the +standard basis column; an extra dimension is denoted by e_i^extra. +The minimal projector itself commutes with B_i: on A_i and C_i the +prefix acts through the same matrix `[[-1,0],[2,-1]]`. + +### Two odd sites force at leastq extra dimensions + +For odd i= q. (7) + +Any selected triple with two odd interior sites therefore has rank sum +at least7q. This argument permits fully noncommuting internal block +coefficients; no exchange of E_i,F_j or other matrices has occurred. + +## 6. A sole odd site leaks extra rank to a far endpoint + +The remaining selected triple consists of the two endpoints0,n and one +odd interior sitei. Write P=E_i+F, with rank(F)=e. At least one endpoint +has the following zero-paired closure under E_i. + +For the left endpoint, if i>=3, canonical substitution gives + + E_i u0=e_i+a_i, v0 E_i=-(e_i^T+tail_i). + +The columns `(u0,E_i u0)` and rows `(v0;v0 E_i)` both have rank2, +and their pairing is zero. The ranks use a coordinate strictly between +0 andi, which exists because i>=3. + +For the right endpoint, if i<=n-3, substitution gives + + E_i u_n=-a_i, v_n E_i=h_i. + +The columns `(u_n,-a_i)` and rows `(h;h_i)` both have rank2 and pairing +zero. The ranks use a coordinate afteri. Since n>=4 andi is odd, at +least one of i>=3 and i<=n-3 holds. Thus a **far endpoint always exists**, +including i=1 and i=n-1. At widthq the two closure spaces have dimensions +2q,2q and still have zero pairing. + +Let Q be the selected far-endpoint projector and write its query factors +as U,V. It is compatible, so QU=U and VQ=V. Since Q commutes with P, + + (I-Q)E_i U = -(I-Q)F U, + V E_i(I-Q) = -V F(I-Q). (8) + +The right sides have rank at moste. For the column closure +`A=span(U,E_i U)`, equation (8) implies + + dim(A intersect im(Q)) >= 2q-e. + +For the row closure `C=span(V,V E_i)`, it similarly implies + + dim(C intersect row(Q)) >= 2q-e. + +The inherited zero pairing C A=0 persists on these subspaces. Applying +(1) to Q gives the quantitative rank-defect bound + + rank(Q) >= 4q-2e. (9) + +This bound is for arbitrary Q and P of the given ranks, not scalar +projector classifications tensored with I_q. It follows from ranks of +the actual leakage maps in (8). + +Write rank(Q)=2q+f. Compatibility also gives f>=0. Therefore + + f >= max(0,2q-2e), + e+f >= e+max(0,2q-2e) >= q. (10) + +The last step has two elementary cases: if e>=q it is immediate; +if e<=q, the left side is at least2q-e>=q. The third selected projector +has rank at least2q. This proves the total rank bound7q in the sole-odd +case without a separate boundary-pair or nesting argument. + +The cases (3), (7), and (10) exhaust all triples: without even interior +sites, a triple either has at least two odd interior sites or consists +of both endpoints and one odd interior site. The theorem is proved for +every evenn>=4 and everyq>=1. + +## 7. Exact all-n attainment + +Here is one ordinary unimodular basis giving equality, rather than a +finite search for small dimensions. In the first four coordinates define + + c0=(1,1,0,0), c1=(1,2,1,0), + c2=(1,2,2,0), t=(0,1,1,1). + +Let H have first four entries of columns0,1,2 equal to c0,c1,c2; +every columnj>=3 has first four entries t. In the remaining coordinates, +for3<=j<=n-2 let columnj have the unit entry in rowj+1, and let the last +column have the negative alternating sum + + -sum_(j=3)^(n-2) (-1)^(j+1) e_(j+1). + +All other extra entries are zero. There are n-4 terms in this sum, an +even number. Add their indicated alternating columns to the last column: +its extra entries cancel and its first four entries remain t. Subtract +this last column from each columnj=3,...,n-2. After an even column +permutation, the result is + + H4 direct-sum I_(n-4), + H4=[[1,1,1,0],[1,2,2,1],[0,1,2,1],[0,0,0,1]]. + +H4 has determinant1, so H has determinant1 over the integers. In +particular this is valid over every allowed field. + +Conjugate all n+1 canonical query matrices by H. The selected sites0,1,n +then have the same columns and rows in the first four coordinates as +the prior n=4 attaining control: + + u0=(1,1,0,0), v0=(1,-1,0,0), + u1=(1,2,1,0), v1=(1,0,-1,0), + u_n=(-1,0,0,1), v_n=(1,0,0,1), + +with zeros elsewhere. The remaining coordinates of these selected +columns and rows vanish by the alternating-column construction. Put + + P0=diag(1,1,0,0,0,...), + P1=diag(1,1,1,0,0,...), + Pn=diag(1,0,0,1,0,...). + +Their ranks are(2,3,2). They commute and are compatible. P1 supports +both R0,R1, so it commutes with B1; the endpoint prefix conditions are +automatic. Make all other sites thin. Give the selected stages three +independent central variables A,B,C and use their literal full-site +operators + + (I+(D_i-1)P_i)(I+(S-1)R_i), S^2=I. + +At S=+1 the full chronological word equals +`diag(ABC,AB,B,C,I_(n-4))`. At S=-1 it is its negative, using the +prefix conditions and the full shortest-query endpoint. Since2 is +invertible, these two characters establish the exact formal identity + + S diag(ABC,AB,B,C,I_(n-4)). (11) + +Tensoring these coefficient-space matrices with I_q proves attainment +with ranks(2q,3q,2q) for everyq. All nq input fields remain arbitrary +and independent. A zero stage selector on an extra coordinate means +that the stage does not act there; it does **not** initialize that input +to zero. Such extra outputs receive the central factor S in (11). + +This is an abstract exact query/stage word. It supplies no physical +native routing, absolute Gaussian phase, helper interface, operation +allowance, or price by itself. No scalar attainment mechanism is claimed +as new; the all-n extension is included as a sharpness construction. + +## 8. Failed-prefix controls and the n=6 next gate + +The frozen rational q=2 compatibility-only tuple in +`inputs/LOCAL13.json` has three commuting projectors of ranks(4,4,5), +both selected U/V ranks6, and a full five-query product-I8. Its prefix +commutator ranks are(0,4,4). Thus compatibility without the actual +prefix hypothesis genuinely permits a rank sum below7q. + +There is also a direct next-gate check at n=6. Cyclically order its +three local queries as old(1,2,0) and apply factor signs(1,1,-1), so +their canonical chronological sites are0,3,6 and the rank5 projector +is the middle one. With x=(1,0), the actual target local data have + + P_middle (U0+U6)x=0. + +But the canonical seven-query source has + + V3 B3 U0=I2, V3 B3 U6=I2, + V3 B3(U0+U6)x=2x !=0. + +If P_middle commuted with B3, and V3 P_middle=V3, the last expression +would equal `V3 B3 P_middle(U0+U6)x=0`, a contradiction. Adding four +extra independent coordinates with zero selected-stage projectors +does not change this equation. This source-prefix invariant blocks +all completion choices for that fixed local model before a GL search. +It is not inferred from a scalar-history span or from the old n=4 +adjacency lemma. The universal theorem above separately covers all +rank13 candidates satisfying its full hypotheses, not only this model. + +## 9. Verification and limits + +`python3.12 -I -B verify.py` and +`python3.12 -I -B -O verify.py` are read-only standard-library checks. +`--write` authors the receipt. The verifier authenticates every included +source byte and notice; retains the prior n=4 sharp and failed-prefix +controls; checks the uniform prefix, odd projector, ordered product and +far-endpoint closure formulas; checks an ordered free-word commutator +identity; and verifies the all-n attaining word by literal multiplication +with three independent stage variables at S=+1,-1. The finite fixtures +are n=4,6,8,10,12 with several coupled widths, includingq=3. They +corroborate conventions. The proof, rather than a finite grid, supplies +alln/allq and the characteristic scope. + +The hypothesis is a shortest n+1-query tuple with rank-q square-zero +queries, nq independent fields, ordinary constant normalization, +selected compatibility, actual prefix commutation and selected pairwise +commutation. More query calls, different query ranks, initialized or +discarded main fields, stage-dependent ordinary maps, or different +central/output conditions change the model. Arbitrary pre-normalization +frame commutation is not the hypothesis. No general noncommuting-stage +thin-call bound is proved. + +This theorem gives a coefficient-space stage-dimension inventory, not +a minimum number of physical Gaussian calls or a cost lower bound for +every implementation. There is no native supplier, complete invoice, +kappa increment, integer-multiplication theorem, discharge of the +inherited framework assumptions, or frontier selection in this note. +These are AI-assisted author proofs and checks, not human review or +proof-kernel verification. + +Ali Romman's scalar obstruction, forced minimal odd projector/closure +method, image/row rank lemma, complete coupled normal form, and +all-length fixed alternating-interior/curvature/low-rank commutator tools retain +their original credit, including Cinna Davis's query/controller lineage +and all retained contributors. The prior n=4 result in PR6717 remains +credited to thu-nmrc with substantial OpenAI Codex assistance. New +uniform extra-rank commutator/leakage extension and all-n sharp controls: +thu-nmrc with substantial OpenAI Codex assistance. All copied original +notices remain unchanged. Apache-2.0. diff --git a/research/p104-far-endpoint-leakage-review/inputs/6717-README.md b/research/p104-far-endpoint-leakage-review/inputs/6717-README.md new file mode 100644 index 0000000000..ade3fb709f --- /dev/null +++ b/research/p104-far-endpoint-leakage-review/inputs/6717-README.md @@ -0,0 +1,68 @@ +# A sharp stage-rank budget in every shortest coupled root + +For every even n>=4 and q>=1, consider a shortest n+1-query tuple on nq +independent fields, over a commutative field of characteristic different +from two. Any three commuting compatible full-stage projectors satisfying +the actual chronological-prefix conditions have total rank **at least7q**. +The individual ranks may differ and internal coefficient blocks may fail +to commute. An explicit unimodular ordinary frame attains(2q,3q,2q) at +every n,q, with literal endpoint S diag(ABC,AB,B,C,1,...,1). + +This rules out a coupled three-stage shortcut: two parallel copies cannot +reduce the total stage rank from14 to13 while retaining the actual stage +endpoint. In particular, if two full stages have the minimum rank2q, every other +full stage needs rank at least3q. An exact q2 rank13 compatible shortest +tuple is included as a +scope control; it fails the required prefix identities. This is an +algebraic rank-inventory result. It does not provide a new native caller, +paid-call count, kappa, multiplication theorem or scientific admission. + +[PROOF.md](PROOF.md) gives the uniform argument. An even internal full +site already needs rank4q. Each odd internal site contains a forced +rank2q projector. Two such forced projectors have commutator rank2q, +so making the actual stages commute requires at leastq extra dimensions +between them. If the triple contains only one odd site and both endpoints, +a zero-paired image/row calculation imposes the same extra-rank debt. +These cases cover every triple at every even n; no fixed-dimension +coefficient enumeration establishes the theorem. + +Ali Romman PR6398 already proves the scalar q1 obstruction; its scalar +consequence, basic rank/closure method, unique minimal odd projectors and +the complete coupled normal form are +credited predecessor results. The all-length fixed alternating-interior, +curvature and generic low-rank correction tools are retained from +`alternating-caller-closure`. The new scope is the all-even, arbitrary-width +quantitative mixed-rank budget under actual chronological conditions. Full source +bytes and notices are retained and authenticated. Targeted repository +review found no matching coupled mixed-rank statement; no world priority +claim is made. Prepared by thu-nmrc with substantial OpenAI Codex assistance. + +## Reproduce + +Python3.12, standard library only; no network or Git is needed by the +mathematical checks. Run from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/p104-coupled-three-stage-rank-budget +``` + +In a Git-free package export, run `python3.12 -I -B verify.py` and +`python3.12 -I -B independent.py` from the package directory. + +The registered normal/optimized checks are read-only. verify.py checks +source identities, dimension controls, the exact sharp formal stage word, +and the rank13 missing-prefix example. independent.py is a separately +written implementation with no import of the author verifier; it checks +the canonical and attaining words, ranks and rejected controls. +The written proof establishes unbounded q, while finite exact checks +corroborate its conventions. These are author-side AI-assisted checks, +not human or proof-kernel verification. VALIDATION.json records actual runs. + +## Open next questions + +- What sharper aggregate rank budgets hold for larger collections of full + stages, and which patterns attain them? +- Can a different coupled mixed-rank geometry improve a complete source-bound + productive/paid invoice? Supply the actual stage identity and all costs. +- Independently audit the uniform proof and attaining word. Archive intake + or passing CI alone does not establish scientific acceptance. diff --git a/research/p104-far-endpoint-leakage-review/inputs/6717-TASK.json b/research/p104-far-endpoint-leakage-review/inputs/6717-TASK.json new file mode 100644 index 0000000000..919dd2a29b --- /dev/null +++ b/research/p104-far-endpoint-leakage-review/inputs/6717-TASK.json @@ -0,0 +1,129 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. 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", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove and sharply attain a uniform7q total-stage-rank lower bound for any three commuting prefix-compatible full stages in every shortest n+1-query tuple on nq independent fields, at every even n>=4 and arbitrary coupled width q; individual stage ranks may differ.", + "scope_change_reason": "The continuing explicit user objective requests original frontier mathematics. A coupled q2 compatibility-only rank13 model appears profitable before its missing chronological stage obligations; this source-contract change isolates and resolves that loophole by an all-width rank theorem.", + "selection_method": "Continuing explicit user-assigned research objective; the originating catalogue card is retained for provenance, not a fresh random assignment.", + "bottleneck_link": "Actual chronological prefix constraints force canonical odd projectors and quantitative extra-rank debts. Exact odd-pair commutator and far-endpoint leakage inequalities rule out a coupled rank13 shortcut at all even dimensions; compatibility alone is insufficient.", + "stop_rule": "Reject if a complete tuple satisfies every stated hypothesis below7q, a copied source changes bytes, the sharp full polynomial endpoint fails, or the scope is enlarged to a physical/cost/kappa claim without evidence.", + "outcome": "completed", + "evidence": "PROOF.md; uniform prefix/commutator/leakage identities; exact all-even sharp family; RESULT.json; independent verifier and normal/optimized registered replays.", + "author": "thu-nmrc", + "ai_assistance": "Substantial OpenAI Codex assistance including parallel discovery, overlap, mathematical review, independent exact verification and writing. All checks are author-side, not external scientific review.", + "open_questions": [ + { + "question": "What sharper total rank budgets hold for larger collections of full stages?", + "why_it_matters": "The seven-q bound covers every triple but need not be the best aggregate inventory bound.", + "first_step": "Combine actual prefix conditions and quantitative extra-rank debts for a specified full-site pattern, and give an attaining construction or complete obstruction.", + "blocked_by": "No global optimum for every collection of full stages is supplied." + }, + { + "question": "Can coupled mixed-rank roots with more stages improve a complete source-bound invoice?", + "why_it_matters": "This result excludes one optimistic three-stage escape, not all coupled callers.", + "first_step": "First exhibit all independent-stage identities and count every paid/idle/productive direction before a physical replay.", + "blocked_by": "No new native supplier or complete paid invoice is part of this proof." + }, + { + "question": "Will an independent scientific reviewer admit the uniform mixed-rank extension?", + "why_it_matters": "Author-side proof review and CI establish neither external priority nor scientific admission.", + "first_step": "Audit the prefix-to-intersection lemma, middle-site rank floor and literal sharp endpoint; compare the credited predecessor.", + "blocked_by": "External scientific review remains pending." + } + ] +}