From fc3647b48d02bb8aab2d2f9460db39d276497ed1 Mon Sep 17 00:00:00 2001 From: apoursh <8867770+apoursh@users.noreply.github.com> Date: Tue, 27 Oct 2026 23:48:30 -0400 Subject: [PATCH] Prove the exact partitioned-walk readout frontier --- .../partitioned-walk-exact-frontier/PROOF.md | 304 ++++++++++++++++++ .../partitioned-walk-exact-frontier/README.md | 134 ++++++++ .../SOURCES.json | 48 +++ .../partitioned-walk-exact-frontier/TASK.json | 62 ++++ .../VERIFY.json | 34 ++ .../partitioned-walk-exact-frontier/oracle.py | 133 ++++++++ .../partitioned-walk-exact-frontier/verify.py | 301 +++++++++++++++++ 7 files changed, 1016 insertions(+) create mode 100644 research/partitioned-walk-exact-frontier/PROOF.md create mode 100644 research/partitioned-walk-exact-frontier/README.md create mode 100644 research/partitioned-walk-exact-frontier/SOURCES.json create mode 100644 research/partitioned-walk-exact-frontier/TASK.json create mode 100644 research/partitioned-walk-exact-frontier/VERIFY.json create mode 100644 research/partitioned-walk-exact-frontier/oracle.py create mode 100644 research/partitioned-walk-exact-frontier/verify.py diff --git a/research/partitioned-walk-exact-frontier/PROOF.md b/research/partitioned-walk-exact-frontier/PROOF.md new file mode 100644 index 0000000000..3c3f30af7d --- /dev/null +++ b/research/partitioned-walk-exact-frontier/PROOF.md @@ -0,0 +1,304 @@ +# Exact readout frontier for partitioned independent walks + +The result is a scoped theorem in the five-source abstract model of Wentao Li's +[PR #2779](https://github.com/CrocSwap/integer-mult-bounds/pull/2779), using +Nick Petalas's extension to arbitrary labels and any number of walks in +[PR #6036](https://github.com/CrocSwap/integer-mult-bounds/pull/6036). +It supplies no physical supplier or new kappa. The proof is elementary counting; +the bounded finite checks corroborate it rather than replace an unbounded step. + +## 1. Model and theorem + +A restored walk is a slot list + +``` +w = (s_0, ..., s_(n-1)), s_0 = 0, s_i in F2^5, +``` + +whose closed completion has no zero edge: consecutive labels differ, including +the last label and the initial zero. Labels may repeat at nonadjacent slots, +and zero may be revisited. Necessarily n >= 2. Its even-subset table e_w(x) +is the minimum cardinality of a subset of slots whose XOR is x and whose +cardinality is even, or infinity if there is no such subset. In particular +e_w(0)=0 by the empty subset. + +For k >= 2 independent walks of lengths n_1,...,n_k, let Q=sum_i n_i and +define the cost of a mask x by the min-plus XOR convolution + +``` +c(x) = min { sum_i e_(w_i)(x_i) : x_1 XOR ... XOR x_k = x }. +``` + +A family covers if every x in F2^5 has finite cost. Its readout is +R=sum_(x != 0) c(x). For k=2 this is PR #2779's two-port model; the k>=3 +extension is the one explicitly defined in PR #6036. + +**Theorem.** No covering family exists at Q<7. For every integer Q>=7 the +minimum readout over all covering families, all walk counts k>=2 and all +permitted label repetitions is + +| Q | Minimum R | +|---:|---:| +| 7 | 112 | +| 8 | 92 | +| 9 | 80 | +| 10 | 72 | +| 11 | 66 | +| >=12 | 62 | + +The first three values are retained predecessor results. The new ingredients +are sharp pair-difference bounds for eight and nine points in F2^5, which +settle the open Q=10 and Q=11 cases, and an explicit saturation construction +with a valid padding rule for every Q>=12. + +## 2. Even-subset costs and difference sets + +For a support set A in F2^5 write + +``` +D(A) = { a XOR b : a,b in A, a != b }. +``` + +The table lemma of PR #6036 also follows directly from the definition. +An arbitrary subset of slots has the same XOR after toggling slot 0, so an +even subset exists precisely for the masks in the span of the walk labels. +For a nonzero mask every finite cost is an even integer at least two, and +cost two is equivalent to membership in D(A). Repeated labels do not change +this equivalence: two equal labels produce zero, not a new nonzero difference. + +Consequently, if P is the union of all walk difference sets, exactly the masks +in P have combined cost two. Every other nonzero mask of a covering family +costs at least four. Thus + +``` +R >= 124 - 2|P|, R >= 62. (1) +``` + +These are lower bounds: the masks outside P need not all have cost four. +Attaining families below are checked with their full even-subset tables. + +Coverage is equivalent to the sum of the walk spans being F2^5. Since each +walk starts with zero, its span has dimension at most n_i-1. Therefore + +``` +5 <= sum_i (n_i-1) = Q-k <= Q-2, (2) +``` + +which proves the nonexistence statement for Q<7. + +## 3. Two sharp finite-geometry bounds, proved without a census + +**Lemma 1.** If A is a subset of F2^5 with at most eight points, then +|D(A)|<=25. + +**Proof.** It suffices to consider eight distinct points: smaller sets can +be enlarged to size eight, and enlargement cannot remove a difference. +Write A={a_1,...,a_8}. The kernel over F2 of the matrix whose columns are +(1,a_i) in F2^6 has dimension at least two. Choose a two-dimensional subspace +C of this kernel. Every nonzero vector of C has even weight, and its weight +cannot be two because the points a_i are distinct. Thus its three nonzero +vectors have weights at least four. + +At each coordinate, either every vector of C is zero or exactly two vectors +are one. The sum of the three nonzero weights is therefore at most 2*8=16. +They cannot all have weight at least six. There is a weight-four vector, or +four distinct points whose XOR is zero. + +Those four points produce three different pairings into equal-difference +pairs. The three corresponding nonzero differences are distinct. Among the +C(8,2)=28 unordered pairs, there are therefore at least three excess +occurrences beyond the first occurrence of each difference. Hence +|D(A)|<=28-3=25. QED. + +**Lemma 2.** If A is a subset of F2^5 with at most nine points, then +|D(A)|<=28. + +**Proof.** Again enlarge to nine distinct points if needed. The same +six-row matrix now has a kernel of dimension at least three. Choose a +three-dimensional subspace C of the kernel. Its seven nonzero vectors +have even weights at least four, and their total weight is at most 4*9=36. +If at most two had weight four, the total would be at least +2*4+5*6=38. Thus A has at least three distinct four-point subsets with +zero XOR. + +For each nonzero d let m_d be the number of unordered pairs from A with +difference d. Two distinct pairs with the same difference cannot share a +point. If N_4 is the number of zero-XOR four-point subsets, double counting +the three pairings of each such subset gives + +``` +sum_(d != 0) C(m_d,2) = 3 N_4 >= 9. (3) +``` + +If every m_d<=2, then C(m_d,2)=max(m_d-1,0). Since sum_d m_d=36, +equation (3) gives 36-|D(A)|>=9, and in fact |D(A)|<=27. + +Otherwise one difference b occurs in at least three pairs. Take six points +B from three of these disjoint pairs. They form three cosets of the +two-element subgroup {0,b}. Their internal differences consist of b and +at most two differences for each pair of distinct cosets. Hence + +``` +|D(B)| <= 1 + 2*C(3,2) = 7. +``` + +The remaining set C=A\B has three points. There are at most 6*3=18 +cross differences and at most C(3,2)=3 differences inside C. Every +difference of A belongs to one of these three classes, so +|D(A)|<=7+18+3=28. QED. + +Both bounds are sharp. The supports + +``` +A8 = {0,1,2,4,8,16,30,31}, +A9 = {0,1,2,4,8,16,29,30,31} +``` + +have respectively 25 and 28 differences, with integers denoting their +five-bit vectors. These claims are small direct XOR checks. The verifier +also corroborates the bounds by normalizing a full-rank support to contain +{0,1,2,4,8,16} and enumerating the C(26,2)=325 or C(26,3)=2600 possible +extra-point sets. Supports of rank at most four have at most 15 nonzero +differences. This normalization is independent of the kernel-weight proof. + +## 4. The Q=7,8,9 predecessor cases + +At Q=7, (2) forces k=2, with lengths (2,5) or (3,4), up to interchange. +The five noninitial slot labels must be linearly independent. Thus their +two walk spans form a direct sum of dimensions d_1=n_1-1 and d_2=n_2-1, +with d_1+d_2=5 and each d_i>=1. Every mask has a unique expression using +these five labels. In a given walk, if that expression uses h noninitial +slots, the even-subset cost is h when h is even and h+1 when h is odd, +because the only possible adjustment is to include slot 0. + +Summed over all 32 masks, the selected-label contribution is 32*5/2=80. +For each of the two nonempty blocks, exactly half of its coefficient vectors +have odd weight, contributing 16 more. The zero mask contributes zero. +Therefore every covering Q=7 family has R=80+16+16=112. Independent basis +labels give valid restored walks, so the bound is attained. This rederives +the PR #2779 value in the arbitrary-label scope of PR #6036. + +For general lengths, |D(A_i)|<=C(n_i,2), so (1) implies + +``` +R >= 124 - 2 sum_i C(n_i,2). +``` + +For fixed Q with n_i>=2 and k>=2, moving slots from a smaller part to a +largest part can only increase the sum of these binomial coefficients. +Its maximum is 1+C(Q-2,2), at the two-part partition (2,Q-2). +This is PR #6036's pair-sum bound. It gives R>=92 at Q=8 and R>=80 at Q=9. +The same predecessor supplies attaining valid walks: + +``` +Q=8: (0,10), (0,22,5,31,24,20), +Q=9: (0,3), (0,18,1,5,11,20,27). +``` + +The present verifier recomputes their complete readout tables as calibration +fixtures. Their origin and the established values remain credited to PR #6036. + +## 5. The exact Q=10 and Q=11 minima + +The preceding geometry bounds apply to supports of walks, regardless of +repetition or slot order. The union of difference sets is bounded by the +sum of their sizes; overlap can only make the union smaller. + +For two walks the complete lists of length partitions and resulting bounds +on |P| are: + +| Q | Lengths | Bound on size of P | +|---:|:---|---:| +| 10 | (2,8) | 1+25=26 | +| 10 | (3,7) | 3+21=24 | +| 10 | (4,6) | 6+15=21 | +| 10 | (5,5) | 10+10=20 | +| 11 | (2,9) | 1+28=29 | +| 11 | (3,8) | 3+25=28 | +| 11 | (4,7) | 6+21=27 | +| 11 | (5,6) | 10+15=25 | + +For k>=3, convexity bounds sum_i C(n_i,2) by +C(Q-2k+2,2)+(k-1). For feasible k>=3 this is at most its k=3 value: +17 at Q=10 and 23 at Q=11. These are smaller than 26 and 29 respectively. +This treats every walk count and every permitted repetition pattern. + +Equation (1) therefore gives + +``` +Q=10: R >= 124-2*26 = 72, +Q=11: R >= 124-2*29 = 66. +``` + +The following explicit families attain these bounds: + +``` +Q=10: (0,7), (0,1,2,4,8,16,30,31), +Q=11: (0,7), (0,1,2,4,8,16,29,30,31). +``` + +Each closed walk has nonzero edges because its slots are distinct. Their +long walks contain all five basis vectors, so both families cover. +Direct enumeration of their even subsets and XOR convolution gives +26 masks of cost two and five of cost four at Q=10, and 29 masks of +cost two and two of cost four at Q=11. Thus R=72 and R=66 respectively. + +## 6. Saturation at every Q>=12 + +At Q=12 take + +``` +(0,1), (0,1,2,4,8,16,3,5,6,31). +``` + +The ten-point long support has all 31 nonzero differences. This finite +identity is checked by direct XOR enumeration. Thus every nonzero mask +can be read with cost two, attaining the universal floor R=62. + +To increase Q by one, choose any edge (a,b) of the long walk and insert +an existing support label c distinct from both a and b. There is such a +label because the support has ten points. Both new edges (a,c),(c,b) +are nonzero. The initial zero and the closed completion are retained, +and the support is unchanged. In particular its 31 differences remain. +Repeat this operation for any desired number of added slots. This proves +attainment at every integer Q>=12, including both parities. Adjacent +duplication of a label would create a zero edge and is not the padding rule. + +## 7. Tariff consequence and scope + +In the retained abstract tariff T=38Q+2R+2X with X>=0, the exact readout +frontier gives the following lower bounds, without claiming that X=0 is +attainable together with the readout minimum: + +| Q | Lower bound on T | +|---:|---:| +| 7 | 490 | +| 8 | 488 | +| 9 | 502 | +| 10 | 524 | +| 11 | 550 | +| >=12 | 38Q+124>=580 | + +Hence every covering partitioned independent-walk family in this model has +T>=488, strictly above the six-query endpoint tariff 436. This is a consistency +corollary, not a new tariff obstruction: it already follows by combining +PR #6036's exact Q=7 value with its older readout floors. It does not identify +the exact minimum of T: path cost X and its possible tradeoff with readout remain. + +The theorem concerns the five-source alphabet, independent restored walks, +and the stated even-subset/min-plus billing rule. It does not cover same-walk, +transfer-coupled, shared-dirt or changed-output contracts. No native supplier, +compiler, precision, stock, restoration implementation or outer multiplication +transfer is supplied or priced by this abstract result. No selected-frontier +change, proof-kernel acceptance or independent human review is claimed. + +## Credit + +The model and two-port readout rule are due to Wentao Li, PR #2779, building +on Arham Tahir's PR1898 and the lineage retained in those packages. Nick +Petalas, PR #6036, supplies the arbitrary-label and multiple-walk scope, +pair-sum floor, prior exact Q=7,8,9 conclusions and Q=8,9 witnesses, and +the open questions resolved here. New geometry proof, exact frontier completion +and verification were prepared by **apoursh**, with substantial OpenAI Codex +assistance, including independent subagent derivation and checking. +Apache-2.0. diff --git a/research/partitioned-walk-exact-frontier/README.md b/research/partitioned-walk-exact-frontier/README.md new file mode 100644 index 0000000000..072a663008 --- /dev/null +++ b/research/partitioned-walk-exact-frontier/README.md @@ -0,0 +1,134 @@ +# Exact readout frontier for partitioned independent walks + +**Elementary scoped proof with independent finite corroboration; no new κ.** +This resolves the Q=10,11 question in Nick Petalas's +[PR #6036](https://github.com/CrocSwap/integer-mult-bounds/pull/6036) and identifies +exactly when the absolute readout floor is attained. In the five-source binary +model, allow any number k >= 2 of restored walks, independent dirt, arbitrary +repeated labels and interior zero revisits. For total query count Q, the least +sum R of even-parity readout costs over all 31 nonzero masks is: + +| Q | Minimum R | Status | +|---:|---:|---| +| <7 | no covering system | rank obstruction, retained | +| 7 | 112 | retained #2779/#6036 | +| 8 | 92 | retained #2851/#6036 | +| 9 | 80 | retained #2883/#6036 | +| **10** | **72** | **new exact minimum** | +| **11** | **66** | **new exact minimum** | +| **>=12** | **62** | **new saturation threshold and extension** | + +The predecessor's pair-count floor was 66 at Q=10 and 62 at Q=11, while its +best searches found 72 and 66. The [proof](PROOF.md) shows that those witnesses +are optimal. It proves sharp pair-sum bounds: eight points of F2^5 produce at +most 25 distinct nonzero pair sums, and nine points produce at most 28. +The argument uses affine relation codes, Hamming-weight counting and a +three-parallel-pair decomposition. It does not depend on the computer census. + +At Q=12 one ten-label walk covers every nonzero pair sum. Inserting an existing +label distinct from both endpoints into an edge preserves support and avoids +zero edges, so the floor remains attainable at every larger Q. This closes the +readout sharpness question in this model; it neither changes the alphabet nor +prices a new physical supplier. The no-undercut tariff conclusion was already +known. Path cost X is not minimized here, and readout-optimal witnesses need +not minimize 38Q+2R+2X. + +## Reproduction and evidence + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -W error -B research/partitioned-walk-exact-frontier/verify.py +python3.12 -I -O -W error -B research/partitioned-walk-exact-frontier/verify.py +python3.12 -B scripts/research_package.py --package research/partitioned-walk-exact-frontier +python3.12 -B scripts/check_research_commit.py --package research/partitioned-walk-exact-frontier --check-source-history +``` + +The verifier imports no predecessor executable and needs neither Git nor network. +VERIFY.json registers normal and optimized replays. SOURCES.json records exact +predecessor bytes as historical provenance; there are no external live inputs. + +Two different finite representations corroborate the geometric bounds: + +- **Point normalization.** A full-span support containing zero can take a basis + to 1,2,4,8,16. The remaining two or three labels give just 325 and 2,600 + configurations. This is a covering family, not one representative per orbit. + Lower-span sets have at most 15 differences. The size-eight histogram is + {20:90, 22:160, 25:75}; size nine gives + {21:60, 22:60, 23:810, 25:660, 27:750, 28:260}. +- **Kernel codes.** oracle.py independently represents the nonzero point columns + by their binary relation code, and counts weight-one/two error cosets. It + enumerates 120 and 6,435 generator-column multiplicity vectors, retaining 31 + and 827 admissible vectors. Orbit weights recover 2,430,400 and 7,689,240 + full-span point sets containing zero. Four tiny-domain literal censuses check + the weighted counts. This oracle shares neither the point normalization nor + the walk cost computation. + +The replay also checks all query-count partitions at the boundary, literal +restored witnesses, direct even-subset readouts, support-preserving padding and +semantic failure controls. The proof establishes the unbounded-Q statement; +finite padding checks corroborate its implementation. Final coverage and a +canonical result digest are printed by the verifier. + +Both registered modes passed on CPython 3.12.14 (macOS arm64), with identical +canonical reports: 2,925 normalized supports, six witnesses checked by literal +even-subset enumeration, twenty padding witnesses checked by parity dynamic +programming, and seven rejection controls. The latter reject a corrupted +histogram, a missing basis direction, incorrect claimed Q=10/11 witness costs, +a zero edge, a changed witness and relaxed per-port parity. The result SHA256 +(sorted compact JSON, UTF-8) is +`b35ef32a08d40076719f57d88fb56863383667f65da7cddc01d4ec379f225b2d`. +No selected construction, native supplier, Lean or full cold replay was run. + +## Scope and contribution process + +Base: canonical main `721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision +8, selected conditional κ=0.003125804. TASK.json retains the original +`connector-alphabet-change` card verbatim and explicitly marks the scope +**changed**: this is a released sharpness question in a fixed alphabet. The +selected-source baseline passed. The handoff's literal walk model replaces the +card's unrelated changed-alphabet experiment; no physical budget is inferred. + +Family-expansion decision: + +1. Sources are #6036 at `1cf36dd5f4d484a6c764f2b73f4f1e21c3eb3108`, + Wentao Li's #2779 at `1f2a413f9e27ce9609924f7ab196548c4cbe43d8`, and the + retained Q=8/9 packages #2851/#2883. Merged status is not mathematical acceptance. +2. Boundary is independent dirt and per-walk even parity over F2^5; no shared + dirt, transfer-coupled schedules or same-walk replacement is covered. +3. R is an exact readout cost. Path cost is reported for witnesses but not + optimized. Native realization, routing, restoration outside this abstract + contract, precision, stock, compiler and outer costs are not supplied. +4. The result decides the predecessor's explicit sharpness question and first + saturation threshold. The prior tariff obstruction is retained. +5. The paired-stage growth and chain-multiplicity handoffs require harder + structural steps; this question admitted a short proof and a clear stop. + A further construction round needs an actual changed caller and its full bill. + +The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19232829) +replies to the released #6036 handoff. Live all-state PR title/body searches, +recent handoffs and the retained Q=7/8/9 notes were inspected. The overlap helper +had no remote cache and only partial local coverage in this sparse checkout; +live connector/browser checks supplied targeted coverage, not a historical +census or a novelty certificate. Existing packages and shared code are unchanged. + +## Open next questions + +Can a transfer-coupled or shared-dirt interface outperform its complete charged +boundary? First specify one producer/consumer, shared-prefix billing, restoration +and path costs, then compare the full tariff against the retained six-query +endpoint. The missing changed caller and complete billing contract are blockers; +this exact independent-dirt frontier does not supply them. No larger search in +the same readout model is needed to settle its query-count frontier. + +## Credit + +New proof and checker by **apoursh**, with substantial OpenAI Codex assistance +in derivation, implementation, independent subagent review and verification. +Apache-2.0. Nick Petalas #6036 supplies the question, pair-sum reduction, +arbitrary-label/multiple-walk extension and Q=8/9 witnesses. Wentao Li +#2779/#2851/#2883 supplies the independent-walk model and earlier exact minima; +Arham Tahir #1898 supplies the tariff. Retain their mutable-source lineage, +including Ross Richardson #943 and TennisBowling #1524. Elementary binary-code +counting is used without a worldwide-priority claim. AI-assisted review is not +independent human or proof-kernel acceptance. diff --git a/research/partitioned-walk-exact-frontier/SOURCES.json b/research/partitioned-walk-exact-frontier/SOURCES.json new file mode 100644 index 0000000000..116787d45b --- /dev/null +++ b/research/partitioned-walk-exact-frontier/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/independent-walks-7q-obstruction/README.md", + "usage": "provenance", + "git_blob": "39f9e7c00906e259f56f5de008cbeff1e12b1138", + "sha256": "5b78726aa573340a5b18f762de769e027c3862623d33181dc7d84943d861de6d" + }, + { + "path": "research/independent-walks-7q-obstruction/model.py", + "usage": "provenance", + "git_blob": "49809a4fa0641bfea0b87b2f85e4c08cc23f0bfd", + "sha256": "8e68f12143bb4392ec4473eed65c0db5a156bf0c60d39dec998abcc840f57e0e" + }, + { + "path": "research/partitioned-walk-pair-sum-floor/README.md", + "usage": "provenance", + "git_blob": "fe2464992fc65a7803212a48e9ef38a93def591b", + "sha256": "2a25f0f0c28f0697c2b84a8b477976d9b1eec313bfef57d21067f86b7994fc9d" + }, + { + "path": "research/independent-walks-8q-obstruction/README.md", + "usage": "provenance", + "git_blob": "31ea4c9795bdb1d67f830777f1a2216a494ab351", + "sha256": "799a98a0dd9ef38c438caa2fd437e10427679dd644025e78a7691f4abc41fd34" + }, + { + "path": "research/independent-walks-9q/README.md", + "usage": "provenance", + "git_blob": "ff1a287a4e2605fdf6b4d1025841b0a6d397db64", + "sha256": "8c15540728934f11bfac360c087e5a8ca79e5ee4f7b87ba6f793026008f24ad3" + } + ] +} diff --git a/research/partitioned-walk-exact-frontier/TASK.json b/research/partitioned-walk-exact-frontier/TASK.json new file mode 100644 index 0000000000..849e9f21c7 --- /dev/null +++ b/research/partitioned-walk-exact-frontier/TASK.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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": "Resolve PR6036 open question 1 and complete the exact readout frontier for five-source partitioned independent-dirt walks at every query count, including arbitrary repeated labels and any number of walks.", + "scope_change_reason": "Handoff-first side result in the unchanged alphabet, not an added operation or physical supplier. The predecessor leaves the Q=10 and Q=11 readout minima open; a sharp pair-sum theorem closes those cases and identifies the first Q attaining the absolute readout floor.", + "bottleneck_link": "Side result: settles sharpness of the abstract readout relaxation; the predecessor already excludes tariff gains for this family. No supplier, selected assumption or kappa improvement follows.", + "budget_minutes": 60, + "stop_rule": "Stop after elementary pair-sum proofs, complete query-count frontier, independent bounded checks and publication. Do not expand to physical realization or another source-count census.", + "outcome": "completed", + "evidence": "Elementary affine-relation-code proofs establish the complete readout frontier. Independent normalized point and kernel-code censuses corroborate the sharp bounds; literal even-parity witnesses, padding checks and seven failure controls pass in normal and optimized Python.", + "author": "apoursh", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation, independent subagent audit and verification.", + "open_questions": [ + { + "question": "Can a transfer-coupled or shared-dirt interface outperform its complete charged boundary?", + "why_it_matters": "The exact independent-dirt frontier closes the current readout relaxation; improvements require a different contract or a physical caller.", + "first_step": "Specify one producer/consumer with shared-prefix billing, restoration and path costs, then compare its full tariff against the retained six-query endpoint.", + "blocked_by": "No changed physical caller or complete shared-prefix billing contract is supplied here." + } + ] +} diff --git a/research/partitioned-walk-exact-frontier/VERIFY.json b/research/partitioned-walk-exact-frontier/VERIFY.json new file mode 100644 index 0000000000..5ee0ff8196 --- /dev/null +++ b/research/partitioned-walk-exact-frontier/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Elementary bound corroboration by normalized point sets and independent kernel-code oracle; exact even-parity attaining witnesses, all partitions, padding and failure controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Elementary bound corroboration by normalized point sets and independent kernel-code oracle; exact even-parity attaining witnesses, all partitions, padding and failure controls." + } + ] +} diff --git a/research/partitioned-walk-exact-frontier/oracle.py b/research/partitioned-walk-exact-frontier/oracle.py new file mode 100644 index 0000000000..790bd3a3f0 --- /dev/null +++ b/research/partitioned-walk-exact-frontier/oracle.py @@ -0,0 +1,133 @@ +"""Independent kernel-code census for binary five-dimensional pair sums. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +The partitioned-walk model and question retain Li/Petalas predecessor credit; +this module checks the separate finite point-set extremum without walk code. +""" + +from collections import Counter +from fractions import Fraction +from itertools import combinations +from math import comb, factorial, prod + + +def check(condition, message): + if not condition: + raise ValueError(message) + + +def compositions(total, parts): + """Every weak composition once, via its unique separator positions.""" + for bars in combinations(range(total + parts - 1), parts - 1): + ends = (-1,) + bars + (total + parts - 1,) + yield tuple(ends[i + 1] - ends[i] - 1 for i in range(parts)) + + +def gl_order(d): + return prod((1 << d) - (1 << i) for i in range(d)) + + +def kernel_census(n, d): + """Count n-point nonzero full-span sets through their relation codes. + + If H lists their columns, C=ker(H) has dimension k=n-d. Distinct, + nonzero columns mean C has no word of weight one or two. Pair sums of + {0} union columns(H) are the cosets represented by errors of weight + one or two. An ordered generator basis of C is a k-by-n binary matrix; + coordinate permutations let us enumerate its column multiplicities. + + For multiplicities a, there are n!/prod(a!) coordinate orderings. + Divide by |GL(k,2)| generator bases and multiply by |GL(d,2)| quotient + identifications, then divide by n! column orderings. This gives weight + |GL(d,2)|/(|GL(k,2)| prod(a!)) for the unordered point-set histogram. + Individual weights can be fractional; every final histogram bin is not. + """ + check((n, d) in {(7, 5), (8, 5), (3, 2), (4, 3), (5, 3), (6, 3)}, + "kernel census outside its declared bounded domains") + k = n - d + errors = [1 << i for i in range(n)] + errors += [(1 << i) | (1 << j) for i, j in combinations(range(n), 2)] + histogram = Counter() + weighted = Counter() + examined = 0 + for multiplicities in compositions(n, 1 << k): + examined += 1 + columns = [x for x, count in enumerate(multiplicities) + for _ in range(count)] + code = tuple(sum(((x & u).bit_count() % 2) << i + for i, x in enumerate(columns)) + for u in range(1 << k)) + if len(set(code)) != 1 << k: + continue + if min(x.bit_count() for x in code[1:]) < 3: + continue + representatives = {min(error ^ word for word in code) + for error in errors} + size = len(representatives) + histogram[size] += 1 + denominator = gl_order(k) * prod(factorial(a) for a in multiplicities) + weighted[size] += Fraction(gl_order(d), denominator) + check(examined == comb(n + (1 << k) - 1, (1 << k) - 1), + "weak-composition inventory incomplete") + check(weighted and all(count.denominator == 1 for count in weighted.values()), + "kernel orbit weights do not count integral point sets") + return { + "generator_multiplicities": examined, + "admissible_multiplicities": sum(histogram.values()), + "multiplicity_histogram": dict(sorted(histogram.items())), + "point_set_histogram": {size: int(count) + for size, count in sorted(weighted.items())}, + "maximum": max(weighted), + } + + +def literal_histogram(n, d): + """Tiny calibration by every point subset, with no code or orbit weights.""" + check((n, d) in {(3, 2), (4, 3), (5, 3), (6, 3)}, + "literal calibration outside its declared bounded domains") + histogram = Counter() + examined = 0 + for points in combinations(range(1, 1 << d), n): + examined += 1 + span = {0} + for point in points: + span = span | {v ^ point for v in span} + if len(span) != 1 << d: + continue + differences = {x ^ y for x, y in combinations((0,) + points, 2)} + histogram[len(differences)] += 1 + check(examined == comb((1 << d) - 1, n), "point inventory incomplete") + return dict(sorted(histogram.items())) + + +def run_oracle(): + """Return corroboration; the package's analytic proof needs no census.""" + rows = {str(n + 1): kernel_census(n, 5) for n in (7, 8)} + expected = { + "8": {20: 833280, 22: 1180480, 25: 416640}, + "9": {21: 234360, 22: 267840, 23: 2812320, + 25: 1874880, 27: 1874880, 28: 624960}, + } + for size, row in rows.items(): + check(row["point_set_histogram"] == expected[size], + "kernel histogram differs at point-set size " + size) + + # A rank-four subspace has 15 nonzero points. At n=7, remove its + # 15 rank-three sets, then count those 155 three-spaces separately. + # At n=8 no smaller subspace can hold the nonzero points. + totals = {"8": comb(31, 7) - 31 * (comb(15, 7) - 15) - 155, + "9": comb(31, 8) - 31 * comb(15, 8)} + for size, row in rows.items(): + check(sum(row["point_set_histogram"].values()) == totals[size], + "full-span point-set total differs at size " + size) + + calibration = [] + for n, d in ((3, 2), (4, 3), (5, 3), (6, 3)): + kernel = kernel_census(n, d) + literal = literal_histogram(n, d) + check(kernel["point_set_histogram"] == literal, + f"independent literal calibration differs at n={n}, d={d}") + calibration.append({"nonzero_points": n, "dimension": d, + "point_set_histogram": literal}) + return {"maxima": {size: row["maximum"] for size, row in rows.items()}, + "kernel_censuses": rows, "literal_calibrations": calibration} diff --git a/research/partitioned-walk-exact-frontier/verify.py b/research/partitioned-walk-exact-frontier/verify.py new file mode 100644 index 0000000000..3ce340ea22 --- /dev/null +++ b/research/partitioned-walk-exact-frontier/verify.py @@ -0,0 +1,301 @@ +#!/usr/bin/env python3 +"""Exact checks for the complete five-source partitioned readout frontier. + +New checker by apoursh with substantial OpenAI Codex assistance, Apache-2.0. +The even-per-port model, path tariff and Q7--Q9 values retain Wentao Li +(PR2779), Nick Petalas (PR6036) and their credited predecessor lineage. +The all-size result rests on PROOF.md; these finite checks corroborate it. +""" +from __future__ import annotations + +from collections import Counter +from itertools import combinations +from math import comb +from pathlib import Path +from types import ModuleType +import hashlib +import json + +INF = 10 ** 6 +BASIS = (0, 1, 2, 4, 8, 16) +EXPECTED_HISTOGRAMS = { + 8: {20: 90, 22: 160, 25: 75}, + 9: {21: 60, 22: 60, 23: 810, 25: 660, 27: 750, 28: 260}, +} +WITNESSES = { + 7: ((0, 1), (0, 2, 4, 8, 16)), + 8: ((0, 10), (0, 22, 5, 31, 24, 20)), + 9: ((0, 3), (0, 18, 1, 5, 11, 20, 27)), + 10: ((0, 7), (0, 1, 2, 4, 8, 16, 30, 31)), + 11: ((0, 7), (0, 1, 2, 4, 8, 16, 29, 30, 31)), + 12: ((0, 1), (0, 1, 2, 4, 8, 16, 3, 5, 6, 31)), +} +FRONTIER = {7: 112, 8: 92, 9: 80, 10: 72, 11: 66, 12: 62} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def span(values): + result = {0} + for value in values: + result |= {x ^ value for x in result} + return result + + +def pair_counts(points): + return Counter(a ^ b for a, b in combinations(points, 2) if a != b) + + +def kernel_words(points): + """Literal dependencies of nonzero columns; no Gaussian elimination.""" + words = [] + for bits in range(1 << len(points)): + value = 0 + for i, point in enumerate(points): + if bits >> i & 1: + value ^= point + if value == 0: + words.append(bits) + return words + + +def normalized_census(n, basis=BASIS): + need(len(basis) == 6 and basis[0] == 0 and len(span(basis)) == 32, + "normalization must retain zero and a full five-dimensional basis") + need(n in (8, 9), "normalized census outside declared domains") + candidates = tuple(x for x in range(32) if x not in basis) + histogram = Counter() + multiplicity_cases = Counter() + for extra in combinations(candidates, n - 6): + points = basis + extra + counts = pair_counts(points) + histogram[len(counts)] += 1 + quadruples = sum(a ^ b ^ c ^ d == 0 + for a, b, c, d in combinations(points, 4)) + need(sum(comb(m, 2) for m in counts.values()) == 3 * quadruples, + "pair-collision/parallelogram identity failed") + code = kernel_words(tuple(point | 32 for point in points)) + need(len(code) == 1 << (n - 6), "affine kernel dimension changed") + need(all(word.bit_count() >= 4 and word.bit_count() % 2 == 0 + for word in code[1:]), "affine kernel has forbidden weight") + need(sum(word.bit_count() for word in code) <= n * (1 << (n - 7)), + "affine-code total-weight bound failed") + need(sum(word.bit_count() == 4 for word in code) == quadruples, + "affine weight-four words do not count parallelograms") + if n == 8: + need(quadruples >= 1 and len(counts) <= 25, "eight-point cap failed") + else: + largest = max(counts.values()) + if largest >= 3: + multiplicity_cases["three_pairs"] += 1 + difference = next(d for d, m in counts.items() if m >= 3) + pairs = [(a, b) for a, b in combinations(points, 2) + if a ^ b == difference][:3] + six = tuple(x for pair in pairs for x in pair) + need(len(set(six)) == 6 and len(pair_counts(six)) <= 7, + "three translated pairs violate their seven-difference cap") + else: + multiplicity_cases["at_most_two_pairs"] += 1 + need(quadruples >= 3 and 36 - len(counts) == 3 * quadruples, + "nine-point low-multiplicity argument failed") + need(len(counts) <= 28, "nine-point cap failed") + need(sum(histogram.values()) == comb(26, n - 6), "incomplete basis census") + need(dict(histogram) == EXPECTED_HISTOGRAMS[n], "normalized histogram changed") + return {"representatives": sum(histogram.values()), + "histogram": dict(sorted(histogram.items())), + "proof_cases": dict(sorted(multiplicity_cases.items()))} + + +def parity_tables(slots): + """Chronological include/exclude DP, with separate parity in this port.""" + table = [[INF] * 32 for _ in range(2)] + table[0][0] = 0 + for point in slots: + nxt = [row[:] for row in table] + for parity in range(2): + for mask, cost in enumerate(table[parity]): + nxt[parity ^ 1][mask ^ point] = min( + nxt[parity ^ 1][mask ^ point], cost + 1) + table = nxt + return table + + +def subset_oracle(slots): + """Every subset, visited in Gray order; independent of the DP recurrence.""" + out = [INF] * 32 + out[0] = 0 + mask = weight = 0 + for i in range(1, 1 << len(slots)): + bit = i & -i + mask ^= slots[bit.bit_length() - 1] + gray = i ^ (i >> 1) + weight += 1 if gray & bit else -1 + if weight % 2 == 0 and weight < out[mask]: + out[mask] = weight + return out + + +def convolve(tables): + acc = [INF] * 32 + acc[0] = 0 + for table in tables: + nxt = [INF] * 32 + for a, ca in enumerate(acc): + for b, cb in enumerate(table): + nxt[a ^ b] = min(nxt[a ^ b], ca + cb) + acc = nxt + return acc + + +def pair_port_oracle(left, right): + """Literal two-port minimization, not the chronological convolution.""" + return [min(left[a] + right[a ^ target] for a in range(32)) + for target in range(32)] + + +def valid_walk(slots): + return (isinstance(slots, tuple) and len(slots) >= 2 and slots[0] == 0 + and all(type(x) is int and 0 <= x < 32 for x in slots) + and all(a != b for a, b in zip(slots, slots[1:] + (0,)))) + + +def witness_receipt(q, walks, expected_r, brute=True): + need(len(walks) >= 2 and sum(map(len, walks)) == q, "witness partition") + need(all(valid_walk(walk) for walk in walks), "zero edge or invalid walk") + tables = [parity_tables(walk)[0] for walk in walks] + if brute: + direct = [subset_oracle(walk) for walk in walks] + need(tables == direct, "literal even-subset oracle disagrees with DP") + need(convolve(tables) == pair_port_oracle(*direct), + "independent port minimization disagrees") + values = convolve(tables) + need(all(value < INF for value in values), "witness does not cover") + r = sum(values[1:]) + need(r == expected_r, f"wrong readout: Q={q}, actual={r}, claimed={expected_r}") + pairs = set().union(*(pair_counts(walk) for walk in walks)) + need({m for m in range(1, 32) if values[m] == 2} == pairs, + "cost-two union differs from literal readout") + x = sum(2 * ((a ^ b).bit_count() - 1) for walk in walks + for a, b in zip(walk, walk[1:] + (0,))) + return {"walks": walks, "R": r, "path_X": x, "tariff": 38 * q + 2 * r + 2 * x, + "readout_histogram": dict(sorted(Counter(values[1:]).items()))} + + +def partitions(total, cap=None): + if cap is None: + cap = total + if total == 0: + yield () + for first in range(min(total, cap), 1, -1): + for rest in partitions(total - first, first): + yield (first,) + rest + + +def difference_cap(n): + if n == 8: + return 25 + if n == 9: + return 28 + return min(31, comb(n, 2)) + + +def partition_receipts(): + result = {} + for q in range(4, 13): + rows = [parts for parts in partitions(q) if len(parts) >= 2] + covering = [parts for parts in rows if sum(n - 1 for n in parts) >= 5] + if q < 7: + need(not covering, "below-seven cover violates dimension bound") + result[q] = {"partitions": len(rows), "covering_by_rank": 0} + continue + cap = max(min(31, sum(difference_cap(n) for n in parts)) for parts in covering) + pair_floor = max(62, 124 - 2 * cap) + if q == 7: + need(set(covering) == {(5, 2), (4, 3)}, "Q7 rank-tight partitions changed") + for parts in covering: + # A covering Q7 word has five independent nonzero labels in + # disjoint port spans. GL normalization sends them to this basis. + start = 0 + walks = [] + for n in parts: + walks.append((0,) + tuple(1 << i for i in range(start, start + n - 1))) + start += n - 1 + need(sum(convolve([parity_tables(w)[0] for w in walks])[1:]) == 112, + "rank-tight Q7 structural identity") + need(sum(16 * n for n in parts) == 112, "Q7 binomial weight identity") + else: + need(pair_floor == FRONTIER[q], "partition floor disagrees with sharp frontier") + result[q] = {"partitions": len(rows), "covering_by_rank": len(covering), + "pair_sum_cap": cap, "pair_floor": pair_floor, + "sharp_R": FRONTIER[q]} + return result + + +def rejected(action): + try: + action() + except ValueError: + return True + return False + + +def controls(censuses): + damaged = dict(EXPECTED_HISTOGRAMS[8]) + damaged[25] -= 1 + controls = { + "corrupted_histogram": rejected(lambda: need( + censuses[8]["histogram"] == damaged, "forged histogram")), + "dropped_basis_axis": rejected(lambda: normalized_census(8, BASIS[:-1])), + "false_Q10_readout_66": rejected(lambda: witness_receipt(10, WITNESSES[10], 66, False)), + "false_Q11_readout_62": rejected(lambda: witness_receipt(11, WITNESSES[11], 62, False)), + "zero_edge_padding": rejected(lambda: witness_receipt( + 13, ((0, 1, 1), WITNESSES[12][1]), 62, False)), + "changed_witness": rejected(lambda: witness_receipt( + 10, ((0, 1), WITNESSES[10][1]), 72, False)), + } + relaxed = [] + for walk in WITNESSES[7]: + even, odd = parity_tables(walk) + relaxed.append([min(a, b) for a, b in zip(even, odd)]) + need(sum(convolve(relaxed)[1:]) != 112, "odd-parity control failed to discriminate") + controls["odd_parity_mixing"] = rejected(lambda: need( + sum(convolve(relaxed)[1:]) == 112, "independent port dirt not restored")) + need(len(controls) == 7 and all(controls.values()), "one failure control did not reject") + return controls + + +def main(): + censuses = {n: normalized_census(n) for n in (8, 9)} + # Source-load the checked sibling, including under -I/-B/-O, so stale pyc + # files and the caller's module search path cannot replace the oracle. + path = Path(__file__).with_name("oracle.py") + module = ModuleType("partitioned_walk_kernel_oracle") + exec(compile(path.read_bytes(), str(path), "exec"), module.__dict__) + oracle = module.run_oracle() + need(oracle["maxima"] == {"8": 25, "9": 28}, "kernel-code maxima disagree") + witnesses = {q: witness_receipt(q, ws, FRONTIER[q]) for q, ws in WITNESSES.items()} + padding = {} + long = WITNESSES[12][1] + for q in range(13, 33): + # Insert an existing support label unequal to both ends of the first + # edge. This is the proof's padding rule, with no zero edge or new point. + inserted = 1 if long[1] != 1 else 2 + long = (0, inserted) + long[1:] + need(set(long) == set(WITNESSES[12][1]), "padding changed support") + padding[q] = witness_receipt(q, ((0, 1), long), 62, brute=False) + report = {"normalized_censuses": censuses, "kernel_oracle": oracle, + "partitions": partition_receipts(), "witnesses": witnesses, + "padding_witnesses": padding, "controls": controls(censuses), + "scope": "finite corroboration of the written all-Q proof; no new kappa"} + print(json.dumps(report, sort_keys=True)) + canonical = json.dumps(report, sort_keys=True, separators=(",", ":")).encode("utf-8") + print("RESULT_SHA256=" + hashlib.sha256(canonical).hexdigest()) + print("PASS_PARTITIONED_WALK_EXACT_FRONTIER normalized_supports=2925" + " witnesses=26 controls=7 Q10_R=72 Q11_R=66 Q_ge_12_R=62 no_new_kappa") + + +if __name__ == "__main__": + main()