From 0c3ff8236c103c5960ef15c45b26432ad1603f8d Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 09:19:47 +0000 Subject: [PATCH] feat(research): sharpen balanced connector source capacity --- .../README.md | 246 +++++++++ .../SOURCES.json | 36 ++ .../TASK.json | 86 +++ .../VERIFY.json | 38 ++ .../WITNESS.json | 519 ++++++++++++++++++ .../connector.py | 88 +++ .../verify.py | 240 ++++++++ 7 files changed, 1253 insertions(+) create mode 100644 research/connector-balanced-walk-threshold/README.md create mode 100644 research/connector-balanced-walk-threshold/SOURCES.json create mode 100644 research/connector-balanced-walk-threshold/TASK.json create mode 100644 research/connector-balanced-walk-threshold/VERIFY.json create mode 100644 research/connector-balanced-walk-threshold/WITNESS.json create mode 100644 research/connector-balanced-walk-threshold/connector.py create mode 100644 research/connector-balanced-walk-threshold/verify.py diff --git a/research/connector-balanced-walk-threshold/README.md b/research/connector-balanced-walk-threshold/README.md new file mode 100644 index 0000000000..1956daebfc --- /dev/null +++ b/research/connector-balanced-walk-threshold/README.md @@ -0,0 +1,246 @@ +# Balanced closed walks improve unsigned connector capacity + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped written proof with an exact finite construction certificate.** In the +unsigned dirty-connector interface of PR4231/PR4248, define + +```text +C(k) = 2 ceil(2^(k-1)/k), +L(c) = max { k >= 1 : C(k) <= c }. +``` + +For every integer characteristic `c >= 2`, the source capacity satisfies + +```text +N(c) >= L(c) floor(c/2) + 2(c mod 2). +``` + +Moreover, `C(k)` is the exact maximum-coordinate-flip threshold among **closed +binary-cube covering walks** on `k` coordinates. This is a classical Gray-code +consequence applied here to the connector construction. It is not a lower bound +for arbitrary depth-two connector words. + +For `c >= 8`, put `b = floor(log2 c)` and `m = floor(log2 b)`. Then + +```text +b + m <= L(c) <= b + m + 2. +``` + +Thus the explicit lower bound gains the `log2 log2 c` source term missing from +PR6071's reflected-Gray specialization. At `c = 256`, it gives `N(256) >= 1408`; +PR6071's displayed reflected-Gray guarantee is 1152. This comparison concerns +those two guarantees, not a claim to know the best construction on main. + +The new part is the explicit optimized connector threshold, its source-capacity +consequence, and a literal realization. Balanced Gray cycles are classical. +PR6071 supplies the covering-walk split; PR6107 explicitly suggests the balanced +direction without deriving this bound. Neither predecessor is audited here. +There is no new kappa or change to the selected frontier. + +## Interface and proof + +Let `R` be any nonzero unital ring of characteristic `c >= 2`. Sources `x_j`, +the borrowed connector `z`, and outputs `y_m` begin arbitrarily dirty. The only +complete calls are `B_j: z += B_j x_j` and `A_m: y_m += A_m z`, for compatible +linear maps. Each call restores its private scratch and heads, preserves every +other row, and has fixed ports. Sources and coefficients are immutable. Outputs +are unobserved until completion. There are no negative calls, extra connectors, +free copies, scalings, direct product calls, or mutable-source operations. + +The desired action is `y_m += sum_(j in m) A_m B_j x_j`, with `z` restored. +The identity specialization forces every used operator to occur a positive +multiple of `c` times. A complete-call floor word uses each exactly `c` times. +PR4248's depth-two block criterion asks for every binary mask to be the sum +modulo `c` of at most two prefixes of a source word containing each source +exactly `c` times. Repeated read boundaries are allowed. + +### Exact closed-walk threshold + +Consider any finite closed single-coordinate walk that starts at zero and +visits every vertex of `{0,1}^k`, allowing repeated vertices. Let its length be +`s`, and let `f_j` count flips of coordinate `j`. Since it returns to its start, +each `f_j` is even. Its `s` distinct time slots before the repeated endpoint +must cover `2^k` vertices, so `s >= 2^k`. Consequently + +```text +max_j f_j >= 2 ceil(s/(2k)) >= 2 ceil(2^(k-1)/k) = C(k). +``` + +The classical balanced cyclic Gray-code theorem supplies a Hamilton cycle +whose even coordinate flip counts differ by at most two. Their sum is `2^k`, +so their largest value is precisely `C(k)`. The two-step walk treats `k = 1`. +This attains the lower bound for every `k`. Existence is a cited classical +theorem, not a conclusion inferred from the finite witness. + +Primary reference: G. S. Bhat and C. D. Savage, [Balanced Gray Codes, Theorem 1](https://doi.org/10.37236/1249), +Electronic Journal of Combinatorics 3, R25, 1996, pages 8-10. +Their [2005 historical comment](https://www.combinatorics.org/ojs/index.php/eljc/article/download/v3i1r25/comment/) +credits the earlier Bakos construction recorded by A. Adam in 1968. The +Robinson-Cohn construction and Bhat-Savage subsequence selection also produced +the supplied literal cycle. No new Gray-code existence theorem is claimed. + +### Positive calls from a closed walk + +Take a balanced cycle with `C(k) <= c`. In the notation of Armin Pourshafeie's +PR6071, let `U(t)` and `D(t)` count upward and downward flips through time `t`. +Then `U(t)-D(t)=g_t`, the visited binary vertex. Let `A` and `B` be the label +subsequences of upward and downward flips. Form the positive source word + +```text +W = A · product_j j^(c-f_j) · reverse(B). +``` + +Each source occurs `c` times. At the two actual boundaries + +```text +a(t) = |U(t)|, s(t) = kc - |D(t)|, +``` + +the integer prefix vectors are `U(t)` and `c*1-D(t)`. Their sum is `c*1+g_t`. +Both boundaries exist, lie in chronological order, and represent `g_t` modulo +`c`. The compiler retains the first occurrence of each mask. All executable +calls are positive, including those designed using downward flips. + +Two output reads at these boundaries deliver the requested contribution. +Add `c-2` output reads at boundary zero to cancel the arbitrary connector +baseline. Every output is called exactly `c` times, including its padding. +Every source is also called exactly `c` times, restoring `z`. This uses only +linearity and characteristic `c`; neither primality nor commutation of the +operators is required. It is PR6071's split applied to a better walk. + +### Capacity and the second-order term + +Concatenate `floor(c/2)` disjoint `L(c)`-source blocks. Completed blocks have +zero prefix modulo `c`, so any global binary mask uses at most two reads per +nonzero block. If `c` is odd, add PR4248's depth-one two-source block +`a b a^(c-1) b^(c-1)`. Its prefixes at `1,2,c+1` give the three nonzero masks. +The total depth is at most `c`; pad each output with boundary-zero reads to +exactly `c`. This proves the displayed lower bound on `N(c)`. It does not +materialize the exponentially many outputs of a large composed batch. + +For the lower estimate on `L(c)`, take `k=b+m`, with `b>=3`. Then +`2^k <= cb`, `k>=b+1`, and `c>=2^b>=2(b+1)`. Hence + +```text +C(k) < 2^k/k + 2 <= cb/(b+1) + 2 <= c. +``` + +For the upper estimate, any allowed `k` obeys `2^k <= ck`. The function +`2^k/k` increases for integer `k>=2`. At `k=2b+2` it is at least `2^(b+1)>c`, +so `k<=2b+1`. Since `2b+1<2^(m+2)`, this yields +`2^k <= ck < 2^(b+m+3)`, and therefore `k<=b+m+2`. + +These are bounds on the closed-walk subclass capacity `L(c)`. They do not +close PR6107's gap for unrestricted depth-two words or improve its leading +constant `1/2` for depth-at-most-two concatenations. + +## Literal certificate and complete invoice + +[WITNESS.json](WITNESS.json) contains one nine-coordinate Hamilton cycle. +Independent traversal finds 512 distinct vertices and coordinate counts +`56,56,56,56,56,58,58,58,58`. At characteristic 58, [connector.py](connector.py) +constructs a 522-call source word and two prefix boundaries for all 511 +nonzero masks. Its complete interleaved word has exactly **30,160 calls**, +with each of the nine source operators and 511 output operators called 58 +times. All padding reads are present. The 27 executed fixtures include every +source-coordinate basis vector, both connector basis vectors, zero, and six +mixed dirty inputs over `Z/58Z`, with dirty outputs and singular matrices. + +Let `I` pay admission and layout, `P_F` pay coefficient preparation, `D_W` pay +the actual word's dispatch and instruction storage, and `c_F` be the complete +fixed-port call price, including private restoration and head return. For a +batch on `n` sources, the conditional bill is + +```text +I + sum_F P_F + D_W + c sum_j c_Bj + c sum_(m != 0) c_Am. +``` + +No physical price is set to zero. Full-row storage, output layout, instruction +volume, compiler closure, native frame compatibility, precision, routing and +the outer caller remain uninstantiated. This abstract call-floor construction +does not supply a favorable physical supplier bill. The selected PR6030 and +all five framework assumptions retain their status. + +The values `N(58)>=261`, `N(64)>=288`, `N(256)>=1408`, and `N(512)>=3072` +are evaluations of the proved formula. The complete composed batches at +these source counts were not executed. The literal executed batch has nine +sources and 511 outputs. + +## Reproduction and verification scope + +From the repository root, using CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/connector-balanced-walk-threshold/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/connector-balanced-walk-threshold/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/connector-balanced-walk-threshold +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/connector-balanced-walk-threshold --check-source-history +``` + +Expected marker: `PASS_CONNECTOR_BALANCED_WALK_THRESHOLD`. The verifier emits a +generated receipt bound to package hashes. Use `--output /absolute/scratch/result.json` +to retain it outside the checkout. The replay requires only the standard library. +Local interpreter: CPython 3.12.15, macOS, Clang 23.1.3. Hosted CI is recorded +separately in the PR body. + +The finite corroboration checks 120 closed covering walks: dimension one at +lengths 2 through 4, and dimension two at lengths 2 through 8. Their compiled +blocks supply 356 mask checks. It also checks the literal nine-source cycle, +all 511 prefix pairs, 27 complete dirty-input executions, 1,023 exact capacity +rows for `c=2..1024`, and ten rejecting controls. These controls cover malformed +walks, insufficient characteristic, changed source pins, wrong reads and an +unpaid source or output call. No predecessor scientific verifier is imported. + +The infinite result uses the written proof and the cited classical theorem. +It is not a proof-kernel result. Independent human and formal proof-kernel +review are unclaimed. No selected cold replay, Lean, Docker, physical native +supplier, rounded multiplier or complete multiplication theorem was run. + +### Code limits + +The literal compiler accepts dimension at most ten, characteristic at most +512, and at most `2^(dimension+1)` walk steps. Its largest complete word has +528,896 calls. The arithmetic-only threshold API accepts dimension through +4096. Every traversal is bounded by these inputs or the fixed replay domain; +there is no recursion or subprocess execution in the verifier. + +Python and its standard containers allocate dynamically. This is a managed +runtime deviation from fixed steady-state allocation, with the explicit +limits above bounding live objects. Python also has no pointer-depth or +compile-time warning equivalent. Runtime checks remain active under `-O`; +warning-as-error replay and in-memory syntax/function-size checks cover the +kept code. No claim of a constant-workspace implementation follows. + +## Open next questions + +1. Does an open cube-covering path improve the threshold at dimensions where + only one coordinate has the largest flip count? This could reduce the + characteristic for the same split. First delete each edge of one balanced + cycle and price the resulting path counts. General path balancing is open + here, and no open-path optimality is claimed. +2. Can an unrestricted depth-two source word beat this closed-walk capacity by + more than a constant number of coordinates? First compare literal prefix + geometry with PR6107's weight-count obstruction. This package supplies no + unrestricted upper bound beyond the credited predecessor. +3. Can a named characteristic-c consumer use the extra sources at a favorable + complete price? First specify its immutable sources, physical endpoints, + output layout and complete `I,P,D,c_F` ledger. No such consumer is supplied. + +## Sources and credit + +The scope comes from Josie Elliston / [PR6107](https://github.com/CrocSwap/integer-mult-bounds/pull/6107), +Open next question 3. The main construction is Armin Pourshafeie / apoursh's +[PR6071](https://github.com/CrocSwap/integer-mult-bounds/pull/6071). +Nick Petalas's PR4231/PR4248 supplies the unsigned interface, prefix criterion, +concatenation and the depth-one pair, with Ross Richardson's PR934/PR943 and +Riquelme Soares's retained lineage. Josie Elliston's PR6061 and zxv's PR6057 +supply earlier finite blocks. Bakos, Robinson-Cohn, and Bhat-Savage retain +credit for the classical Gray-code mathematics and construction. Source +READMEs and all predecessor credit lines remain unchanged. + +[SOURCES.json](SOURCES.json) pins the canonical base, task card, selected record +and three live predecessor READMEs. [TASK.json](TASK.json) records the changed +card premise and structured next questions. Live overlap checking preceded +the [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19370235). +Sparse local notes and unpublished work remain coverage limitations. diff --git a/research/connector-balanced-walk-threshold/SOURCES.json b/research/connector-balanced-walk-threshold/SOURCES.json new file mode 100644 index 0000000000..5d1e5c0cee --- /dev/null +++ b/research/connector-balanced-walk-threshold/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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/connector-bounded-depth-cap/README.md", + "usage": "input", + "git_blob": "0127ee20090453b48024f8a1b279427a6612b0bf", + "sha256": "9e8800a27375b92b77b20cf3594f647a507bf17fd9bff2c4da1be10db2db98fa" + }, + { + "path": "research/connector-depth-blocks/README.md", + "usage": "input", + "git_blob": "5d5b4a5b96e05f3818ff454d4dfdc5dc2959f6b4", + "sha256": "0ce59767f249b24d65d7d14b466115858d82c0bbfaaa8eab46b7406f4e975331" + }, + { + "path": "research/connector-gray-growth/README.md", + "usage": "input", + "git_blob": "0c9041011c12aa1f617b624c721482a3817f62ec", + "sha256": "8129752acb681528f734ff6f1b95a127948bfcf8817ae5d7500ccf46523e042a" + } + ] +} diff --git a/research/connector-balanced-walk-threshold/TASK.json b/research/connector-balanced-walk-threshold/TASK.json new file mode 100644 index 0000000000..5f1dada24c --- /dev/null +++ b/research/connector-balanced-walk-threshold/TASK.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "Exact closed-cube-covering-walk flip threshold C(k)=2 ceil(2^(k-1)/k), balanced unsigned connector source-capacity lower bound, and one literal nine-source certificate.", + "scope_change_reason": "The operation alphabet stays fixed. This takes PR6107 Open next question 3 and builds on PR6071 rather than adding an operation. It is a scoped local interface side result, not a completed supplier or a scientific audit.", + "bottleneck_link": "Larger immutable-source batches can improve the productive side of an interface only after a physical consumer and complete invoice are supplied; this theorem improves an abstract source-capacity guarantee and makes no selected budget claim.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified balanced-walk threshold and literal connector improvement; leave other walks and unrestricted words open.", + "outcome": "completed", + "evidence": "README.md written proof; WITNESS.json literal Hamilton cycle; verify.py independent prefixes, 27 complete dirty-input executions, 120 small closed walks, capacity bounds and rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an open cube-covering path improve this characteristic threshold?", + "why_it_matters": "Removing closure can lower a maximum coordinate count without changing the positive split interface.", + "first_step": "Delete each edge of a balanced cycle and compare maximum flip counts.", + "blocked_by": "No all-dimension optimal path theorem or full connector-optimality claim is supplied." + }, + { + "question": "Can unrestricted depth-two words exceed this closed-walk capacity by an unbounded additive amount?", + "why_it_matters": "The closed-walk optimum does not settle the full prefix geometry.", + "first_step": "Combine literal prefix constraints with PR6107 weight counting.", + "blocked_by": "The predecessor upper bound and the new lower bound do not match." + }, + { + "question": "Can one named physical consumer use the larger batches at a favorable complete bill?", + "why_it_matters": "Source capacity by itself changes no admitted supplier or kappa.", + "first_step": "Specify endpoints and price admission, preparation, dispatch, every complete call and output layout.", + "blocked_by": "No physical consumer or complete price assignment is supplied." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19370235", + "upstream_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "priority_revision": 8, + "checked_utc": "2026-11-03T09:09:00Z", + "coverage": "Live open PRs and recent handoffs; merged distinctive/general-family searches; current-main README search; cached overlap has sparse local notes. Unpublished work and arbitrary historical diffs are not covered." + }, + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS", + "dependencies": "standard library only" + } +} diff --git a/research/connector-balanced-walk-threshold/VERIFY.json b/research/connector-balanced-walk-threshold/VERIFY.json new file mode 100644 index 0000000000..a94ae43c51 --- /dev/null +++ b/research/connector-balanced-walk-threshold/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/connector-bounded-depth-cap/README.md", + "research/connector-depth-blocks/README.md", + "research/connector-gray-growth/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete literal construction, independent prefix and dirty-input checks, exact capacities, source pins and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same checks with Python assertions disabled; validation uses explicit runtime guards." + } + ] +} diff --git a/research/connector-balanced-walk-threshold/WITNESS.json b/research/connector-balanced-walk-threshold/WITNESS.json new file mode 100644 index 0000000000..24443f87d2 --- /dev/null +++ b/research/connector-balanced-walk-threshold/WITNESS.json @@ -0,0 +1,519 @@ +{ + "dimension": 9, + "characteristic": 58, + "transition_sequence": [ + 6, + 7, + 8, + 2, + 4, + 1, + 2, + 0, + 3, + 0, + 4, + 1, + 2, + 0, + 4, + 2, + 3, + 2, + 1, + 4, + 1, + 2, + 3, + 1, + 3, + 0, + 2, + 3, + 0, + 4, + 0, + 1, + 2, + 3, + 5, + 4, + 6, + 4, + 5, + 3, + 5, + 6, + 2, + 6, + 5, + 1, + 5, + 6, + 0, + 6, + 5, + 4, + 5, + 6, + 0, + 6, + 5, + 3, + 5, + 6, + 2, + 6, + 5, + 0, + 8, + 0, + 5, + 6, + 2, + 6, + 5, + 3, + 5, + 6, + 0, + 6, + 5, + 4, + 5, + 6, + 0, + 6, + 5, + 1, + 5, + 6, + 2, + 6, + 5, + 3, + 5, + 4, + 6, + 4, + 5, + 3, + 2, + 1, + 0, + 4, + 0, + 3, + 2, + 0, + 3, + 1, + 3, + 2, + 1, + 4, + 1, + 2, + 3, + 2, + 4, + 0, + 2, + 1, + 4, + 0, + 3, + 0, + 2, + 1, + 4, + 7, + 4, + 1, + 2, + 0, + 3, + 0, + 4, + 1, + 2, + 0, + 4, + 2, + 3, + 2, + 1, + 4, + 1, + 2, + 3, + 1, + 3, + 0, + 2, + 3, + 0, + 4, + 0, + 1, + 2, + 3, + 5, + 4, + 6, + 4, + 5, + 3, + 5, + 6, + 2, + 6, + 5, + 1, + 5, + 6, + 0, + 6, + 5, + 4, + 5, + 6, + 0, + 6, + 5, + 3, + 5, + 6, + 2, + 6, + 5, + 0, + 5, + 6, + 3, + 7, + 3, + 6, + 8, + 6, + 3, + 6, + 8, + 7, + 5, + 1, + 3, + 7, + 3, + 1, + 8, + 1, + 3, + 5, + 8, + 7, + 3, + 7, + 8, + 6, + 8, + 7, + 3, + 7, + 8, + 2, + 8, + 7, + 6, + 7, + 8, + 5, + 1, + 4, + 1, + 8, + 1, + 4, + 1, + 7, + 1, + 4, + 1, + 5, + 7, + 8, + 1, + 4, + 8, + 4, + 7, + 4, + 6, + 7, + 8, + 4, + 8, + 7, + 1, + 7, + 8, + 2, + 8, + 7, + 3, + 7, + 8, + 6, + 8, + 7, + 3, + 7, + 8, + 5, + 8, + 7, + 3, + 7, + 8, + 2, + 8, + 7, + 4, + 0, + 7, + 0, + 8, + 0, + 2, + 8, + 7, + 1, + 7, + 8, + 4, + 0, + 8, + 0, + 7, + 0, + 3, + 7, + 8, + 0, + 8, + 7, + 2, + 7, + 8, + 1, + 8, + 7, + 5, + 7, + 8, + 1, + 8, + 7, + 2, + 7, + 8, + 0, + 8, + 7, + 3, + 7, + 8, + 0, + 8, + 7, + 4, + 7, + 8, + 1, + 8, + 7, + 2, + 7, + 8, + 0, + 8, + 7, + 4, + 7, + 8, + 6, + 8, + 7, + 4, + 7, + 8, + 0, + 8, + 7, + 2, + 7, + 8, + 1, + 8, + 7, + 4, + 7, + 8, + 0, + 8, + 7, + 3, + 7, + 8, + 0, + 8, + 7, + 2, + 7, + 8, + 1, + 8, + 7, + 4, + 7, + 8, + 6, + 8, + 7, + 5, + 7, + 2, + 8, + 2, + 7, + 5, + 6, + 4, + 1, + 2, + 0, + 3, + 0, + 4, + 1, + 2, + 0, + 4, + 6, + 4, + 0, + 2, + 1, + 4, + 0, + 3, + 0, + 2, + 1, + 5, + 1, + 2, + 0, + 3, + 0, + 4, + 1, + 2, + 0, + 4, + 2, + 3, + 5, + 3, + 6, + 3, + 2, + 1, + 4, + 6, + 4, + 1, + 5, + 1, + 4, + 1, + 5, + 6, + 2, + 3, + 6, + 3, + 5, + 3, + 1, + 5, + 6, + 3, + 6, + 5, + 0, + 5, + 6, + 2, + 6, + 5, + 3, + 5, + 6, + 0, + 6, + 5, + 4, + 5, + 6, + 0, + 6, + 5, + 1, + 5, + 6, + 2, + 6, + 5, + 3, + 5, + 4, + 6, + 4, + 5, + 3, + 2, + 1, + 0, + 4, + 0, + 3, + 2, + 0, + 3, + 1, + 3, + 2, + 1, + 4, + 1, + 2, + 3, + 2, + 4, + 0, + 2, + 1, + 4, + 0, + 3, + 0, + 2, + 1, + 4, + 2, + 6, + 8 + ], + "construction": "Robinson-Cohn construction with Bhat-Savage subsequence quotas; literal sequence is independently checked, not trusted." +} diff --git a/research/connector-balanced-walk-threshold/connector.py b/research/connector-balanced-walk-threshold/connector.py new file mode 100644 index 0000000000..faf6dd7037 --- /dev/null +++ b/research/connector-balanced-walk-threshold/connector.py @@ -0,0 +1,88 @@ +"""Bounded literal compiler for the balanced closed-walk connector theorem.""" + +from collections import Counter +from dataclasses import dataclass + +MAX_DIMENSION = 10 +MAX_CHARACTERISTIC = 512 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def threshold(dimension: int) -> int: + """Exact closed-covering-walk threshold; arithmetic API stops at 4096.""" + require(type(dimension) is int and 1 <= dimension <= 4096, "dimension") + half = 1 << (dimension - 1) + return 2 * ((half + dimension - 1) // dimension) + + +def closed_walk(dimension: int, transitions: tuple[int, ...]) -> tuple[int, ...]: + require(type(dimension) is int and 1 <= dimension <= MAX_DIMENSION, "dimension") + require(2 <= len(transitions) <= 2 ** (dimension + 1), "walk length") + require(all(type(j) is int and 0 <= j < dimension for j in transitions), "label") + vertices = [0] + for j in transitions: + vertices.append(vertices[-1] ^ (1 << j)) + require(vertices[-1] == 0, "walk is not closed") + require(len(set(vertices)) == 1 << dimension, "walk does not cover the cube") + counts = Counter(transitions) + require(all(counts[j] % 2 == 0 for j in range(dimension)), "odd closed count") + require(max(counts.values()) >= threshold(dimension), "closed-walk lower bound") + return tuple(vertices) + + +@dataclass(frozen=True) +class Block: + dimension: int + characteristic: int + sources: tuple[int, ...] + reads: tuple[tuple[int, ...], ...] + + +def compile_block(dimension: int, characteristic: int, + transitions: tuple[int, ...]) -> Block: + require(type(characteristic) is int and 2 <= characteristic <= MAX_CHARACTERISTIC, + "characteristic") + vertices = closed_walk(dimension, transitions) + counts = Counter(transitions) + require(max(counts.values()) <= characteristic, "insufficient characteristic") + upward: list[int] = [] + downward: list[int] = [] + first = {0: (0, 0)} + for index, j in enumerate(transitions): + if vertices[index] & (1 << j): + downward.append(j) + else: + upward.append(j) + first.setdefault(vertices[index + 1], (len(upward), len(downward))) + middle = tuple(j for j in range(dimension) + for _ in range(characteristic - counts[j])) + sources = tuple(upward) + middle + tuple(reversed(downward)) + total = dimension * characteristic + require(len(sources) == total, "source count") + reads = [()] + for mask in range(1, 1 << dimension): + a, down = first[mask] + reads.append((a, total - down)) + return Block(dimension, characteristic, sources, tuple(reads)) + + +def complete_events(block: Block) -> tuple[tuple[str, int], ...]: + """Materialize every positive call, including all dirty-cancelling padding.""" + total = len(block.sources) + buckets: list[list[int]] = [[] for _ in range(total + 1)] + for mask in range(1, 1 << block.dimension): + for boundary in block.reads[mask]: + buckets[boundary].append(mask) + buckets[0].extend([mask] * (block.characteristic - 2)) + events: list[tuple[str, int]] = [] + for boundary in range(total + 1): + events.extend(("A", mask) for mask in buckets[boundary]) + if boundary < total: + events.append(("B", block.sources[boundary])) + expected = block.characteristic * (block.dimension + (1 << block.dimension) - 1) + require(len(events) == expected, "complete call count") + return tuple(events) diff --git a/research/connector-balanced-walk-threshold/verify.py b/research/connector-balanced-walk-threshold/verify.py new file mode 100644 index 0000000000..722af7db69 --- /dev/null +++ b/research/connector-balanced-walk-threshold/verify.py @@ -0,0 +1,240 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration, independent prefixes, and literal dirty calls.""" + +import argparse +from collections import Counter +import hashlib +from itertools import product +import json +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +sys.path.insert(0, str(PACKAGE)) +from connector import closed_walk, compile_block, complete_events, require, threshold + + +def check_sources(root: Path, manifest: dict) -> int: + rows = [row for row in manifest["files"] if row["usage"] == "input"] + require(len(rows) == 3, "live source inventory") + for row in rows: + actual = hashlib.sha256((root / row["path"]).read_bytes()).hexdigest() + require(actual == row["sha256"], "changed source: " + row["path"]) + return len(rows) + + +def check_prefixes(block) -> int: + """Rebuild literal integer prefixes without using the walk/compiler logic.""" + k, c = block.dimension, block.characteristic + require(Counter(block.sources) == Counter({j: c for j in range(k)}), "floor") + prefixes = [[0] * k] + for j in block.sources: + current = prefixes[-1].copy() + current[j] += 1 + prefixes.append(current) + for mask in range(1, 1 << k): + boundaries = block.reads[mask] + require(len(boundaries) == 2, "depth two") + for j in range(k): + coefficient = sum(prefixes[t][j] for t in boundaries) % c + require(coefficient == (mask >> j) & 1, "wrong read coefficient") + return (1 << k) - 1 + + +def small_walks() -> tuple[int, int]: + admitted = checks = 0 + for k in (1, 2): + for length in range(2, min(8, 2 ** (k + 1)) + 1): + for labels in product(range(k), repeat=length): + vertex = 0 + visited = {0} + counts = Counter(labels) + for j in labels: + vertex ^= 1 << j + visited.add(vertex) + if vertex or len(visited) != 1 << k: + continue + require(max(counts.values()) >= threshold(k), "independent lower bound") + block = compile_block(k, max(counts.values()), labels) + checks += check_prefixes(block) + admitted += 1 + return admitted, checks + + +def capacity_table() -> list[dict]: + rows = [] + for c in range(2, 1025): + allowed = [k for k in range(1, 25) if threshold(k) <= c] + k = max(allowed) + require(threshold(k + 1) > c, "threshold inversion") + b = c.bit_length() - 1 + if c >= 8: + lower = b + b.bit_length() - 1 + require(lower <= k <= lower + 2, "second-order capacity bound") + rows.append({"c": c, "k": k, "sources": k * (c // 2) + 2 * (c % 2)}) + selected = {r["c"]: r for r in rows if r["c"] in (58, 64, 256, 512)} + require([selected[c]["sources"] for c in (58, 64, 256, 512)] == + [261, 288, 1408, 3072], "displayed capacities") + return list(selected.values()) + + +def matvec(matrix: tuple[int, ...], vector: tuple[int, int], c: int) -> tuple[int, int]: + a, b, d, e = matrix + x, y = vector + return ((a * x + b * y) % c, (d * x + e * y) % c) + + +def add(left: tuple[int, int], right: tuple[int, int], c: int) -> tuple[int, int]: + return ((left[0] + right[0]) % c, (left[1] + right[1]) % c) + + +def matrices(k: int, c: int) -> tuple[tuple, tuple]: + sources = tuple((1, j + 2, j % 3, (j + 2) % c) for j in range(k)) + sources = ((1, 2, 0, 0),) + sources[1:] + outputs = tuple((m % c, 1, (m // c) % c, 1 + m % 7) for m in range(1 << k)) + return sources, outputs + + +def execute(events: tuple, c: int, sources: tuple, dirty: tuple[int, int], + targets: tuple, operators: tuple) -> tuple: + bmaps, amaps = operators + z = dirty + y = list(targets) + for kind, index in events: + if kind == "B": + z = add(z, matvec(bmaps[index], sources[index], c), c) + else: + require(kind == "A", "event kind") + y[index] = add(y[index], matvec(amaps[index], z, c), c) + return z, tuple(y) + + +def expected(c: int, sources: tuple, dirty: tuple, targets: tuple, operators: tuple) -> tuple: + bmaps, amaps = operators + result = list(targets) + for mask in range(1, len(targets)): + combined = (0, 0) + for j, source in enumerate(sources): + if mask & (1 << j): + combined = add(combined, matvec(bmaps[j], source, c), c) + result[mask] = add(targets[mask], matvec(amaps[mask], combined, c), c) + return dirty, tuple(result) + + +def fixtures(k: int, c: int) -> list[tuple]: + zero = ((0, 0),) * k + cases = [(zero, (0, 0))] + for j in range(k): + for component in range(2): + values = list(zero) + values[j] = (1, 0) if component == 0 else (0, 1) + cases.append((tuple(values), (0, 0))) + cases.extend(((zero, (1, 0)), (zero, (0, 1)))) + for seed in range(1, 7): + values = tuple(((seed * (j + 3)) % c, (seed + j * j) % c) for j in range(k)) + cases.append((values, ((3 * seed) % c, (seed + 1) % c))) + return cases + + +def literal_checks(block) -> tuple[int, int, tuple]: + k, c = block.dimension, block.characteristic + events = complete_events(block) + prices = Counter(events) + require(len(prices) == k + (1 << k) - 1, "complete operator inventory") + require(set(prices.values()) == {c}, "every operator must attain its floor") + operators = matrices(k, c) + targets = tuple(((7 * m + 1) % c, (m * m + 3) % c) for m in range(1 << k)) + count = 0 + for sources, dirty in fixtures(k, c): + actual = execute(events, c, sources, dirty, targets, operators) + wanted = expected(c, sources, dirty, targets, operators) + require(actual == wanted, "literal dirty-input execution") + count += 1 + return count, len(events), (events, operators, targets) + + +def rejecting_controls(block, transitions: tuple, manifest: dict) -> int: + count = 0 + attempts = ((0, 58, transitions), (9, 1, transitions), (9, 57, transitions), + (9, 58, transitions[:-1]), (9, 58, (0, 0)), + (9, 58, (9,) + transitions[1:])) + for k, c, word in attempts: + try: + compile_block(k, c, word) + except ValueError: + count += 1 + else: + raise ValueError("accepted invalid constructor input") + changed = json.loads(json.dumps(manifest)) + next(row for row in changed["files"] if row["usage"] == "input")["sha256"] = "0" * 64 + try: + check_sources(PACKAGE.parents[1], changed) + except ValueError: + count += 1 + else: + raise ValueError("accepted changed source pin") + altered_reads = list(block.reads) + altered_reads[1] = (0, 0) + bad = type(block)(block.dimension, block.characteristic, block.sources, tuple(altered_reads)) + try: + check_prefixes(bad) + except ValueError: + count += 1 + else: + raise ValueError("accepted wrong read boundaries") + return count + + +def call_mutations(block, evidence: tuple) -> int: + events, operators, targets = evidence + c, k = block.characteristic, block.dimension + zero = ((0, 0),) * k + require(events[0][0] == "A", "padding control setup") + wanted = expected(c, zero, (1, 1), targets, operators) + require(execute(events[1:], c, zero, (1, 1), targets, operators) != wanted, + "unpaid output call not detected") + position = next(i for i, event in enumerate(events) if event == ("B", 0)) + sources = ((1, 0),) + zero[1:] + changed = events[:position] + events[position + 1:] + require(execute(changed, c, sources, (0, 0), targets, operators)[0] != (0, 0), + "unpaid source call not detected") + return 2 + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path) + args = parser.parse_args() + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + inputs = check_sources(PACKAGE.parents[1], manifest) + witness = json.loads((PACKAGE / "WITNESS.json").read_text()) + k, c = witness["dimension"], witness["characteristic"] + require((k, c) == (9, 58), "witness parameters") + transitions = tuple(witness["transition_sequence"]) + vertices = closed_walk(k, transitions) + require(len(transitions) == 512 and len(set(vertices[:-1])) == 512, "Hamilton cycle") + require(sorted(Counter(transitions).values()) == [56] * 5 + [58] * 4, "balance") + block = compile_block(k, c, transitions) + masks = check_prefixes(block) + walks, small_masks = small_walks() + table = capacity_table() + cases, events, evidence = literal_checks(block) + controls = rejecting_controls(block, transitions, manifest) + call_mutations(block, evidence) + hashes = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(PACKAGE.iterdir()) if p.is_file()} + receipt = {"marker": "PASS_CONNECTOR_BALANCED_WALK_THRESHOLD", + "claim_type": "scoped proof with finite construction corroboration", + "witness": {"dimension": k, "characteristic": c, "masks": masks, + "complete_calls": events, "dirty_fixtures": cases}, + "closed_small_walks": walks, "small_mask_checks": small_masks, + "capacity_rows": 1023, "displayed_capacities": table, + "rejected_controls": controls, "live_inputs": inputs, "sha256": hashes} + rendered = json.dumps(receipt, indent=2, sort_keys=True) + "\n" + if args.output: + require(PACKAGE not in args.output.resolve().parents, "receipt must be outside package") + args.output.write_text(rendered) + print(rendered, end="") + + +if __name__ == "__main__": + main()