From 6a95ef419f94e7b5c2fff710e34081520cc6aba2 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 20 Oct 2026 22:57:58 +0100 Subject: [PATCH] feat(research): prove full coefficient connector overhead exponent --- research/full-coefficient-connector/README.md | 260 +++++++++++++++++ .../full-coefficient-connector/SOURCES.json | 30 ++ research/full-coefficient-connector/TASK.json | 74 +++++ .../full-coefficient-connector/VERIFY.json | 32 +++ research/full-coefficient-connector/verify.py | 267 ++++++++++++++++++ 5 files changed, 663 insertions(+) create mode 100644 research/full-coefficient-connector/README.md create mode 100644 research/full-coefficient-connector/SOURCES.json create mode 100644 research/full-coefficient-connector/TASK.json create mode 100644 research/full-coefficient-connector/VERIFY.json create mode 100644 research/full-coefficient-connector/verify.py diff --git a/research/full-coefficient-connector/README.md b/research/full-coefficient-connector/README.md new file mode 100644 index 0000000000..38b6c86d83 --- /dev/null +++ b/research/full-coefficient-connector/README.md @@ -0,0 +1,260 @@ +# Full coefficient demand has optimal overhead exponent 1/c + +For every fixed finite characteristic c >= 3, let OPT_c(n) be the minimum +complete-call count for the unsigned, one-dirty-connector interface below, +with all c^n - 1 nonzero coefficient rows. Then + +```text +OPT_c(n) = c(c^n - 1) + Theta(c^(n/c)) as n tends to infinity. +``` + +This is a **scoped proof with a deterministic construction and finite +corroboration**. It settles the growth rate of the overhead, not its leading +constant or any new exact optimum. The construction has exactly c readouts +per output. The lower bound covers every legal word, including words that +buy extra readouts. No new kappa or selected-frontier change is claimed. + +This continues the full ternary demand introduced in +[#4238](https://github.com/CrocSwap/integer-mult-bounds/pull/4238), head +`191a905d7adba6695b079f744140a73e832787a8`, and extended to six sources in +[#4244](https://github.com/CrocSwap/integer-mult-bounds/pull/4244), head +`f436d2911351e5be2842208fe96b0b66442323a4`. Their exact small optima are +cited and not rechecked. The new result is the all-n construction and matching +overhead exponent, extended to every finite characteristic. The written proof +is self-contained and does not depend on either pending census. + +## Interface + +Work over any nonzero unital ring R of characteristic exactly c, with free +modules of compatible dimensions. Sources x_0..x_(n-1) are immutable; z is one +borrowed arbitrarily dirty connector. Every nonzero row v in (Z/cZ)^n has a +distinct dirty output y_v. The required action is + +```text +y_v += sum_j v_j A_v B_j x_j; every source and z is restored. +``` + +The maps are arbitrary R-linear maps, possibly singular and noncommuting. +The only calls are unsigned `B_j: z += B_j x_j` and `A_v: y_v += A_v z`. +There are no inverse calls, free copies, source mutation, other connectors, +frame changes, output borrowing or direct A_v B_j calls. Outputs are observed +after the complete batch. Calls include their own private restoration; this +package prices only the number of those complete calls. + +The word is fixed independently of data and map entries and must work for +every admissible choice. Characteristic c means c times the identity is zero +and no smaller positive integer times the identity is zero. No field division +or primality assumption is used. The proof also covers c = 2, where block +constructions and the corresponding exponent have predecessors. + +## Prefix criterion and counts + +Project a word onto its L source calls. At boundary t let q_t count each +source modulo c. Then + +```text +z = z_initial + sum_j (q_t)_j B_j x_j. +``` + +For each output, the sum of its readout prefixes must equal v, and its +readout count must vanish modulo c. Each source count must also vanish +modulo c. These conditions are sufficient by linearity. Necessity follows +by specializing to scalar identity and zero maps on independent source and +dirty inputs. Every source is requested and every row is nonzero, so every +source and output occurs at least c times. In particular L >= cn and c divides +L. This is the established prefix/count argument of #4231/#4238. + +## Directed torus cycles + +For b >= 1 there is a length-c^b directed Hamilton cycle on (Z/cZ)^b using +only positive coordinate increments. Here is an explicit induction. + +- For b = 1 use the one coordinate c times. +- Given a cycle W on b coordinates, delete its last edge to get a path P + visiting every vertex. Its endpoint is -e_j, where e_j was the deleted edge. + On one new coordinate k, use `(P B_k)^c`. + +Each copy visits every old-coordinate vector in one new-coordinate layer, +translated by the old endpoint accumulated from earlier copies. The new +coordinate separates the c layers. After c copies both the old displacement +-c e_j and the new displacement c e_k vanish. The length is +`c((c^b - 1) + 1) = c^(b+1)`. Thus every vertex occurs exactly once among the +boundaries before closure. The code builds this induction iteratively. + +## Construction + +Partition the n sources into c blocks, allowing empty blocks. In each +nonempty block run its torus cycle while all other source coefficients are +zero, returning to zero before the next block. An empty block supplies the +zero prefix without calls. For any v, its c block projections occur among +the available boundaries. Read A_v once at each projection, repeating the +zero boundary when needed. Their sum is v and c copies of incoming dirt +cancel. Readouts do not change the connector, so all outputs can use these +boundaries in the same chronological word. + +Write n = ac + r, 0 <= r < c. Balanced blocks give the source count + +```text +S_c(n) = cn if n < c, +S_c(n) = (c + (c - 1)r)c^a if n >= c. +``` + +There are exactly `c(c^n - 1) + S_c(n)` complete calls. The balance is optimal +within this particular geometry of at most c separately restored blocks, +each exposing every block vector as one prefix. A nonempty b-coordinate block +requires at least c^b boundaries. Splitting a block into two nonempty pieces +does not increase that cost, since c^(a+b) >= c^a + c^b for a,b >= 1, c >= 2. +For a fixed number of nonempty blocks, moving a coordinate from a block of +size b to one of size a with b >= a+2 strictly reduces the sum. This proves +the claimed restricted minimum. It is not a global constant optimum. + +## All-word lower bound, including extra readouts + +Put M = c^n - 1 and + +```text +P_c(L) = binomial(L + c - 1, c) - L, +L_0 = least multiple of c, at least cn, for which P_c(L_0) >= M. +``` + +A restored source path has at most L boundary vectors: the final boundary +equals the initial boundary. A row served by exactly c reads is the sum of a +c-element multiset of these indexed boundaries. There are +`binomial(L+c-1,c)` such multisets. The L pure repeated multisets each sum +to zero, so at most P_c(L) nonzero rows can use exactly c reads. Duplicate +boundaries or duplicate sums only decrease this upper bound. + +Every remaining row needs at least 2c reads, since its count is a positive +multiple of c. Therefore every word has at least + +```text +cM + L + c max(0, M - P_c(L)) +``` + +calls. This implies the simpler lower bound **cM + L_0**. If L >= L_0 it is +immediate. Otherwise let h = (L_0-L)/c. The integer function P_c increases +by at least one at each c-step. Indeed +`P_c(L+1)-P_c(L) = binomial(L+c-1,c-1)-1 >= 1` for L >= 1, c >= 2. +Since P_c(L_0-c) < M, we have M-P_c(L) >= h. The extra reads cost at least +ch = L_0-L. This also proves that L_0 is the exact minimum of this relaxed +counting invoice; it need not be attained by a legal word. + +Finally, + +```text +M <= P_c(L_0) <= (L_0 + c - 1)^c / c!, +L_0 >= (c! M)^(1/c) - (c - 1). +``` + +Together with the construction this proves, for fixed c, + +```text +(c!(c^n-1))^(1/c) - (c-1) + <= OPT_c(n) - c(c^n-1) + <= S_c(n) = O(c^(n/c)). +``` + +Both sides have order c^(n/c). In particular, permitting extra output calls +does not improve the overhead exponent. The constants are not matched. + +## Finite examples and evidence + +These are emitted literal words, not exact-optimum claims. + +| Characteristic | Sources | Source calls | Readouts | Total | Counting lower | +|---:|---:|---:|---:|---:|---:| +| 3 | 5 | 21 | 726 | 747 | 741 | +| 3 | 6 | 27 | 2184 | 2211 | 2202 | +| 3 | 7 | 45 | 6558 | 6603 | 6582 | +| 3 | 8 | 63 | 19680 | 19743 | 19716 | + +#4238's exact five-source value 744 and #4244's exact six-source value 2208 +are smaller than this uniform construction. #4244 also gives a stronger +seven-source lower bound of 6588 using deletion. Those are cited predecessor +results, not contradicted by this simpler all-characteristic bound. + +The verifier checks 41 complete words for c = 2..8, with n ranges +1..9, 1..8, 1..6, 1..5, 1..5, 1..4 and 1..4 respectively. It checks 36,996 +output rows and 186,532 literal calls with a formal coefficient ledger. +It also checks 28 Hamilton cycles, all 780 weak block compositions for +c = 2..5 and n = 1..6, and all 2,220 readout multisets in four small cases. +Twelve separate dense executions use dimensions 2 and 3, c = 3,4,6 and +n = 3,4, with dirty registers and singular noncommuting matrices. + +Six controls are rejected: a dropped source call, a dropped readout, a cyclic +source relabeling, a misrouted output, an appended source call, and the same +ternary word executed in characteristic six. The generated stdout receipt +binds these counts and the example table to SHA-256 hashes of all package +files. There is no hand-written receipt or stored generated replay output. + +## Reproduction + +From the repository root, using CPython 3.12 and the standard library: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/full-coefficient-connector/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/full-coefficient-connector/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/full-coefficient-connector +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/full-coefficient-connector --check-source-history +``` + +The selected record, catalogue and two predecessor READMEs in +[SOURCES.json](SOURCES.json) are historical provenance, resolved from the +pinned base commit. The verifier imports no predecessor code and has no live +external inputs. + +Expected marker: `PASS_FULL_COEFFICIENT_CONNECTOR`. The verifier writes no +files. The all-n result is the written induction and counting proof; the +finite replay corroborates it. No full selected replay or formal proof-kernel +build is needed or claimed for this isolated package. + +The code has no recursion. Replay parameters cap c at 8, n at 12 and rows +at 100,000; the registered cases are smaller. Python-managed allocation is +an explicit Power of Ten deviation: live storage is O((n+c)c^n + c S_c(n)) for +these bounded cases, rather than allocation-free execution. This is a +verification resource bound, not a physical implementation cost theorem. + +## Limits and family decision + +The result concerns full coefficient demand and unit complete-call prices. +It gives no exact optimum for n >= 7 and no optimal leading constant. +It changes the demand and characteristic, not the operation alphabet, so it +is a changed scope from the catalogue card. The c = 2 case is a control and +credited predecessor territory. Characteristic zero has no finite c-read +cancellation and is outside the theorem. + +The call count is proved and the abstract word is constructively supplied. +A caller needing all coefficient rows is unknown. Coefficient preparation, +dispatch, parent stock, hosting, precision, tape and complete supplier +admission remain unknown. Unknown costs are not zero. The decision is to +finish this local theorem and stop construction expansion until a concrete +consumer or a sharper combinatorial question is supplied. This is not a +complete multiplication theorem or a new selected bound. + +## Open next questions + +Structured versions are in [TASK.json](TASK.json). + +1. Close the constant gap between the all-word counting lower bound and the + c-block construction, beginning at c = 3 and n divisible by three. Test + paths whose boundary sets are better c-fold additive bases; include the + cost of realizing those sets by positive source steps and restoration. +2. Improve the explicit seven-source ternary upper bound 6603 toward #4244's + lower bound 6588. A path covering all 2186 rows by three-prefix sums would + preserve the readout floor; count all additional source calls. +3. Identify a real consumer requiring full coefficient demand. Bind its maps + and complete physical invoice before making a supplier claim. + +## Credit + +This contribution was produced by Nick Petalas. Credit Nick Petalas's +#4238/#4244 for the full ternary demand and open larger-source question, +#4231 for the arbitrary-characteristic unsigned interface, Riquelme Soares's +#4189 for the unsigned F3 one-source predecessor, Ross Richardson's #943/#934 +for the prefix-connector and Gray-block lineage, `conorholds`'s #2208 for +block palettes and all-word counting in different alphabets, and ywz65 for +the five-source contract map. The CLAIM mistakenly attributed #2208 to +Richardson; #2208 is by `conorholds`, with Richardson credited for its +#943/#934 lineage. No priority is claimed for Gray codes, direct-sum additive +bases or elementary dirty cancellation. No predecessor credit is changed. +Independent human and formal proof-kernel review are unclaimed. Apache-2.0. diff --git a/research/full-coefficient-connector/SOURCES.json b/research/full-coefficient-connector/SOURCES.json new file mode 100644 index 0000000000..3ce65c5d45 --- /dev/null +++ b/research/full-coefficient-connector/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/bidirectional-connector/README.md", + "usage": "provenance", + "git_blob": "b2beaf30eaa0692211c939ef417dbf8ff849f6ed", + "sha256": "a41f6e79e7df54ea51d563f7007970a4e01ed8c2d1b45d1fefb1f927fee97172" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "provenance", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + } + ] +} diff --git a/research/full-coefficient-connector/TASK.json b/research/full-coefficient-connector/TASK.json new file mode 100644 index 0000000000..c0822da680 --- /dev/null +++ b/research/full-coefficient-connector/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "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": "For each fixed finite characteristic c>=3, construct full-coefficient unsigned connector words with c reads per row and Theta(c^(n/c)) optimal overhead above c(c^n-1).", + "scope_change_reason": "The operation alphabet stays fixed. The demand is all nonzero coefficient rows in (Z/cZ)^n, extending the full ternary demand of PR4238/4244 to arbitrary n and finite characteristic. This is a local combinatorial side result rather than a supplier extension.", + "bottleneck_link": "Full coefficient demand has a sharp overhead exponent in the complete-call model. This supplies an explicit abstract budget, but no actual consumer or physical admission is identified.", + "budget_minutes": 60, + "stop_rule": "Stop at a proved overhead exponent with bounded literal checks; do not optimize a physical supplier without a caller and full invoice.", + "outcome": "completed", + "evidence": "README.md gives the all-size cycle construction and all-word lower bound. verify.py emits 41 words and checks 36996 rows, 186532 calls, 28 cycles, 780 partitions, 2220 multisets, 12 dense cases and 6 controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the optimal leading constant in the excess above c(c^n-1), first for c=3 and n divisible by three?", + "why_it_matters": "The counting bound and block construction have the same exponent but different constants.", + "first_step": "Find smaller c-fold additive boundary bases and charge their positive-step realization and restoration.", + "blocked_by": "Abstract additive bases need not be cheaply realizable as restored source paths." + }, + { + "question": "Can the seven-source full ternary upper bound 6603 be lowered toward the cited 6588 lower bound?", + "why_it_matters": "This is the first unsettled size after the exact six-source predecessor.", + "first_step": "Search a short restored source path covering all 2186 nonzero rows by triple sums.", + "blocked_by": "Triple coverage and the full chronological path invoice must both hold." + }, + { + "question": "Which real caller needs full coefficient demand at favorable complete physical prices?", + "why_it_matters": "A complete-call word alone is not a supplier.", + "first_step": "Pin one caller and its maps, then price coefficient preparation, dispatch, stock, hosting and precision.", + "blocked_by": "No such caller is identified." + } + ] +} diff --git a/research/full-coefficient-connector/VERIFY.json b/research/full-coefficient-connector/VERIFY.json new file mode 100644 index 0000000000..2d0707c907 --- /dev/null +++ b/research/full-coefficient-connector/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Written-proof corroboration: directed torus cycles, balanced blocks, all-word counting invoice, literal generic coefficients, dense dirty-state action and six rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same checks with optimized Python; all semantic checks use explicit exceptions." + } + ] +} diff --git a/research/full-coefficient-connector/verify.py b/research/full-coefficient-connector/verify.py new file mode 100644 index 0000000000..21576d0f84 --- /dev/null +++ b/research/full-coefficient-connector/verify.py @@ -0,0 +1,267 @@ +#!/usr/bin/env python3 +"""Deterministic complete-call words; exact checks use the standard library.""" + +import hashlib +import itertools +import json +import math +from pathlib import Path +import random + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def digits(value, c, n): + result = [] + for _ in range(n): + result.append(value % c) + value //= c + require(value == 0, "coefficient row out of range") + return result + + +def torus_cycle(c, labels): + """A directed Hamilton cycle, using only positive unit increments.""" + word = [] + for j in labels: + if not word: + word = [j] * c + else: + word = (word[:-1] + [j]) * c + return word + + +def source_bound(c, n): + a, r = divmod(n, c) + return r * c if a == 0 else (c + (c - 1) * r) * c**a + + +def compile_word(c, n): + require(2 <= c <= 8 and 1 <= n <= 12, "unsupported finite replay case") + require(c**n <= 100_000, "finite replay row capacity exceeded") + a, r = divmod(n, c) + sizes = [a + (i < r) for i in range(c)] + blocks, source = [], [] + start = 0 + for size in sizes: + labels = list(range(start, start + size)) + blocks.append(labels) + source.extend(torus_cycle(c, labels)) + start += size + require(len(source) == source_bound(c, n), "source invoice") + powers = [c**j for j in range(n)] + first, q = {}, [0] * n + for t, j in enumerate(source): + first.setdefault(sum(q[k] * powers[k] for k in range(n)), t) + q[j] = (q[j] + 1) % c + require(q == [0] * n, "unrestored source path") + reads = [[] for _ in range(len(source))] + for v in range(1, c**n): + row = digits(v, c, n) + for block in blocks: + projection = sum(row[j] * powers[j] for j in block) + reads[first[projection]].append(v) + word = [] + for t, j in enumerate(source): + word.extend(("A", v) for v in reads[t]) + word.append(("B", j)) + require(len(word) == len(source) + c * (c**n - 1), "complete invoice") + return word, source, blocks + + +def check_ledger(c, n, word, modulus=None): + """Track formal A_v z_dirty and A_v B_j x_j, without commuting maps.""" + modulus = c if modulus is None else modulus + z = [1] + [0] * n + outputs = [[0] * (n + 1) for _ in range(c**n)] + for kind, index in word: + if kind == "B": + require(0 <= index < n, "source index") + z[index + 1] = (z[index + 1] + 1) % modulus + else: + require(kind == "A" and 1 <= index < c**n, "readout index") + row = outputs[index] + for j in range(n + 1): + row[j] = (row[j] + z[j]) % modulus + require(z == [1] + [0] * n, "connector dirt or source restoration") + for v in range(1, c**n): + require(outputs[v] == [0] + digits(v, c, n), "output coefficient ledger") + + +def matvec(matrix, vector, c): + return [sum(a * b for a, b in zip(row, vector)) % c for row in matrix] + + +def random_matrices(rng, count, dimension, c): + return [[[rng.randrange(c) for _ in range(dimension)] for _ in range(dimension)] + for _ in range(count)] + + +def dense_case(c, n, dimension, seed): + word, _, _ = compile_word(c, n) + rng = random.Random(seed) + bmaps = random_matrices(rng, n, dimension, c) + amaps = random_matrices(rng, c**n, dimension, c) + # Singular, noncommuting maps are present even over composite rings. + bmaps[0] = [[int(i == 0 and j == 1) for j in range(dimension)] + for i in range(dimension)] + bmaps[1] = [[int(i == 1 and j == 0) for j in range(dimension)] + for i in range(dimension)] + sources = [[rng.randrange(c) for _ in range(dimension)] for _ in range(n)] + saved_sources = [row[:] for row in sources] + injected = [matvec(bmaps[j], sources[j], c) for j in range(n)] + z = [rng.randrange(c) for _ in range(dimension)] + initial_z = z[:] + outputs = [[rng.randrange(c) for _ in range(dimension)] for _ in range(c**n)] + expected = [row[:] for row in outputs] + for v in range(1, c**n): + row = digits(v, c, n) + total = [sum(row[j] * injected[j][k] for j in range(n)) % c + for k in range(dimension)] + delta = matvec(amaps[v], total, c) + expected[v] = [(x + y) % c for x, y in zip(expected[v], delta)] + for kind, index in word: + if kind == "B": + delta = matvec(bmaps[index], sources[index], c) + z = [(x + y) % c for x, y in zip(z, delta)] + else: + delta = matvec(amaps[index], z, c) + outputs[index] = [(x + y) % c for x, y in zip(outputs[index], delta)] + require(z == initial_z and sources == saved_sources, "dense restoration") + require(outputs == expected, "dense noncommuting action") + + +def capacity(c, length): + return math.comb(length + c - 1, c) - length + + +def counting_lower(c, n): + """Minimum of the all-word relaxed invoice, with no floating roots.""" + m = c**n - 1 + lengths = range(c * n, source_bound(c, n) + 1, c) + threshold = next(length for length in lengths if capacity(c, length) >= m) + invoice = min(length + c * max(0, m - capacity(c, length)) for length in lengths) + require(invoice == threshold, "counting threshold reduction") + require(math.factorial(c) * m <= (threshold + c - 1)**c, "root lower bound") + return c * m + threshold + + +def check_cycles(): + cases = 0 + for c in range(2, 9): + for b in range(1, 5): + if c**b > 5000: + continue + word = torus_cycle(c, list(range(b))) + q, seen = [0] * b, set() + for j in word: + require(tuple(q) not in seen, "Hamilton cycle repeats early") + seen.add(tuple(q)) + q[j] = (q[j] + 1) % c + require(len(seen) == c**b and q == [0] * b, "Hamilton coverage") + cases += 1 + return cases + + +def check_multisets(): + examined = 0 + for c, n in ((2, 2), (3, 3), (3, 4), (4, 3)): + _, source, _ = compile_word(c, n) + q, prefixes = [0] * n, [] + for j in source: + prefixes.append(tuple(q)) + q[j] = (q[j] + 1) % c + sums, pure = set(), 0 + for indices in itertools.combinations_with_replacement(range(len(source)), c): + total = tuple(sum(prefixes[t][j] for t in indices) % c for j in range(n)) + if indices[0] == indices[-1]: + require(not any(total), "pure repeated prefix must vanish") + pure += 1 + if any(total): + sums.add(total) + examined += 1 + require(pure == len(source), "pure multiset count") + require(len(sums) <= capacity(c, len(source)), "nonzero multiset capacity") + require(len(sums) == c**n - 1, "small construction has full coverage") + return examined + + +def check_controls(): + word, _, _ = compile_word(3, 4) + bpos = next(i for i, op in enumerate(word) if op[0] == "B") + apos = next(i for i, op in enumerate(word) if op[0] == "A") + relabelled = [(kind, (index + 1) % 4 if kind == "B" else index) + for kind, index in word] + misrouted = word[:] + misrouted[apos] = ("A", 1 + misrouted[apos][1] % 80) + controls = [word[:bpos] + word[bpos + 1:], word[:apos] + word[apos + 1:], + relabelled, misrouted, word + [("B", 0)]] + for control in controls: + try: + check_ledger(3, 4, control) + except ValueError: + continue + raise ValueError("invalid literal word accepted") + try: + check_ledger(3, 4, word, modulus=6) + except ValueError: + return len(controls) + 1 + raise ValueError("wrong characteristic accepted") + + +def check_partitions(): + cases = 0 + # Enumerate all weak compositions in small cases, rather than sampling them. + for c in range(2, 6): + for n in range(1, 7): + best = None + for cuts in itertools.combinations(range(n + c - 1), c - 1): + bounds = (-1,) + cuts + (n + c - 1,) + sizes = [bounds[i + 1] - bounds[i] - 1 for i in range(c)] + cost = sum(c**b for b in sizes if b) + best = cost if best is None else min(best, cost) + cases += 1 + require(best == source_bound(c, n), "balanced palette minimum") + return cases + + +def main(): + totals = {"cycle_cases": check_cycles(), "partition_cases": check_partitions(), + "multisets": check_multisets(), "negative_controls": check_controls(), + "literal_words": 0, "outputs": 0, "calls": 0, "dense_cases": 0} + for c, maximum in ((2, 9), (3, 8), (4, 6), (5, 5), (6, 5), (7, 4), (8, 4)): + for n in range(1, maximum + 1): + word, source, _ = compile_word(c, n) + check_ledger(c, n, word) + require(counting_lower(c, n) <= len(word), "lower bound exceeds witness") + require(sum(op[0] == "B" for op in word) == len(source), "source call count") + totals["literal_words"] += 1 + totals["outputs"] += c**n - 1 + totals["calls"] += len(word) + for c in (3, 4, 6): + for n in (3, 4): + for dimension in (2, 3): + dense_case(c, n, dimension, 1000 * c + 10 * n + dimension) + totals["dense_cases"] += 1 + table = [] + for n in range(5, 9): + length = source_bound(3, n) + table.append({"c": 3, "n": n, "source_calls": length, + "readouts": 3 * (3**n - 1), + "calls": length + 3 * (3**n - 1), + "counting_lower": counting_lower(3, n)}) + package = Path(__file__).resolve().parent + names = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + hashes = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in names} + receipt = {"schema_version": 1, "files_sha256": hashes, "counts": totals, + "ternary_examples": table} + print("PASS_FULL_COEFFICIENT_CONNECTOR " + json.dumps(totals, sort_keys=True)) + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()