diff --git a/research/f3-ternary-six-source/README.md b/research/f3-ternary-six-source/README.md new file mode 100644 index 0000000000..58dd16d1bc --- /dev/null +++ b/research/f3-ternary-six-source/README.md @@ -0,0 +1,170 @@ +# Full ternary demand on the unsigned F3 six-source connector + +For six immutable sources over F3, all **728 nonzero ternary coefficient +rows** and one arbitrarily dirty restored connector, the exact complete-call +optimum is **2208**. The operator-count floor is 2202. Every legal word pays at +least two extra call triples, and one explicit 2208-call word exists. + +This is a **scoped proof with an explicit finite witness**. It answers the +six-source open question of +[#4238](https://github.com/CrocSwap/integer-mult-bounds/pull/4238) +(head `191a905d7adba6695b079f744140a73e832787a8`), which proved the 744-call +five-source optimum and left n = 6 undecided. The lower bound is +census-free apart from #4238's five-source value, which is cited and not +re-run here. It also gives lower bounds for every larger n. There is no new +kappa, supplier consumer or selected-frontier change. + +## Exact boundary + +The interface is #4225's and #4238's, unchanged. Read-only sources +x_0..x_{n-1}, one borrowed dirty connector z and output rows y_v, one for each +nonzero v in F3^n. For arbitrary F3-linear maps of compatible dimension, +implement + +```text +y_v += sum_j v_j A_v B_j x_j for all nonzero v; x_j and z unchanged. +``` + +The only operations are unsigned complete calls `B_j: z += B_j x_j` and +`A_v: y_v += A_v z`. Signed calls, extra connectors, source mutation, frame +changes and free copies are excluded. Maps may be singular and need not +commute. + +## Readout criterion and extra triples + +Let source j occur b_j times and readout A_v occur a_v times. Let q_t in F3^n +count the source calls before boundary t, modulo three. Linearity gives +`y_v = y_v0 + a_v A_v z0 + sum_j (sum over readouts of q_t)_j A_v B_j x_j`. +So a word is correct iff every b_j and a_v is a multiple of three and, for each +row, the readout boundaries sum to v. This is #4225's count argument and +triple-prefix identity, generalized to any number of readouts. Each count is +at least three, so the floor is `F(n) = 3n + 3(3^n - 1)` and every word costs +`F(n) + 3E` for an integer E >= 0, its number of **extra triples**. Write e(n) +for the least E over legal words. + +## Deletion lemma (averaging form) + +Take a legal n-source word W and a source j. Delete every B_j call and every +A_v with v_j != 0. Each remaining boundary vector loses coordinate j, so every +surviving row's readouts still sum to that row, and all counts stay multiples +of three. The result W_j is a legal (n-1)-source word for the full nonzero +demand on the other coordinates. + +Its extra triples are the source extras of the other sources plus the readout +extras of rows with v_j = 0. Summing over j, each source extra survives n - 1 +deletions. A readout extra of row v survives once per zero coordinate of v, +which is at most n - 1 because v is nonzero. Hence +`sum_j E(W_j) <= (n - 1) E(W)`. Each E(W_j) is at least e(n - 1), so + +```text +e(n) >= ceil(n e(n - 1) / (n - 1)). +``` + +#4232 proves the attainment-only form of this deletion for binary masks. The +averaging over j is what turns one forced triple into two here. + +## Six sources + +**Lower bound.** #4238's canonical census shows e(5) = 1. The recurrence gives +e(6) >= ceil(6/5) = 2, so every legal word has at least 2202 + 6 = 2208 calls. +Concretely: a word with one extra triple would either have all b_j = 3 and one +row read six times, or one source called six times and every row covered by +three readouts. Deleting a source in the support of the doubly read row, or +the doubled source, would give a five-source word at the 741-call floor. + +**Construction.** The restored 24-event path + +```text +B5 B4 B0 B1 B0 B3 B2 B4 B3 B1 B0 B1 B4 B5 B0 B1 B0 B2 B5 B3 B2 B1 B0 B1 +``` + +uses B_0 and B_1 six times and every other source three times. Its 24 +boundary vectors have every nonzero row of F3^6 as a sum of three of them, +with repetition. Three readouts per row give `24 + 3*728 = 2208` calls. The +verifier builds the literal word from the lexicographically first readout +triple of each row. It checks the word with a generic coefficient ledger, +valid for arbitrary noncommuting maps. It also runs dense random F3 execution +at dimensions 2 and 3 with dirty connector and output rows. + +The six source deletions of this word are legal five-source words with +extras (1, 1, 2, 2, 2, 2). That agrees with the averaging identity: their sum, +10, is at most 5 times 2. + +The witness came from a simulated-annealing search over 24-event paths. In +the same bounded search, 18-event paths reached at most 597 of 728 rows and +21-event paths at most 682. Those maxima are search observations, not proofs. +The lower bound does not use them. + +## Larger source counts + +Let `c(n)` be the counting bound. A path of length L = 3n + 3s has at most +`C(L + 2, 3) - L` distinct nonzero triple sums, and each uncovered row costs +an extra triple, so E >= s + max(0, 3^n - 1 - C(L + 2, 3) + L). Minimizing over +s gives c(n). Feeding the larger of the two bounds into the recurrence, the +verifier prints: + +| n | recurrence | counting | lower bound on e(n) | lower bound on calls | +|---:|---:|---:|---:|---:| +| 5 | 1 (cited) | 0 | 1 | 744 | +| 6 | 2 | 0 | 2 | 2208 (attained) | +| 7 | 3 | 1 | 3 | 6588 | +| 8 | 4 | 4 | 4 | 19716 | +| 9 | 5 | 8 | 8 | 59097 | +| 10 | 9 | 14 | 14 | 177216 | +| 11 | 16 | 23 | 23 | 531540 | +| 12 | 26 | 37 | 37 | 1594467 | + +The recurrence improves #4238's floor-plus-three bound at n = 6, 7 and 8. +Counting dominates from n = 9. Only n = 6 is exact here. + +## Verification + +From the repository root: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/f3-ternary-six-source/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/f3-ternary-six-source +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/f3-ternary-six-source --check-source-history +``` + +Expected marker: `PASS_F3_TERNARY_SIX_SOURCE calls=2208 floor=2202 rows=728`. +Each registered command takes about 5 s. The verifier uses only the standard +library and writes no files. Five rejection controls drop a readout, use a +source twice, misroute a readout, swap two path events, and reproduce #4238's +241-row gap path. + +## Limitations + +- This is the abstract unsigned complete-call interface over F3 only. +- The six-source lower bound depends on #4238's five-source census + (e(5) = 1). That census is cited, not re-run. Its independent verification + is a separate open claim. +- Exact values for n >= 7 are not determined. Only lower bounds are claimed. +- Prices are unit prices. No row- or source-dependent tariff is claimed. +- Admission, coefficient preparation, dispatch of the 2208-record word and + physical charges are additional and unknown. No consumer for ternary demand + is identified. +- No proof-kernel certificate exists. This is not a complete multiplication + theorem. + +## Open next questions + +The structured versions are in [TASK.json](TASK.json). + +1. **Seven sources.** Is the 6588-call lower bound attained? That needs a + 30-event path with three doubled sources covering all 2186 rows, or an + equivalent mix. A bounded annealing run reached 1952. +2. **Eight sources.** The recurrence and counting bounds agree at four extra + triples. One 36-event covering path would settle n = 8 exactly. +3. **Consumer.** Identify a caller that needs coefficient-2 rows before + pricing any recursive use. + +## Credit + +This contribution was produced by Nick Petalas. It builds on #4238's +interface, five-source census and open question; on #4225's mod-three count +floor and triple-prefix identity; on #4232's binary-mask deletion lemma; on +Riquelme Soares's #4189 unsigned-F3 one-source result; on Ross Richardson's +#943/#934 prefix-connector lineage; and on ywz65's five-source contract map. +No predecessor credit line or frozen package is changed. Independent human and +formal proof-kernel review are unclaimed. Apache-2.0. diff --git a/research/f3-ternary-six-source/SOURCES.json b/research/f3-ternary-six-source/SOURCES.json new file mode 100644 index 0000000000..f8ff62762d --- /dev/null +++ b/research/f3-ternary-six-source/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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/universal-connector-boundary/README.md", + "usage": "input", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + } + ] +} diff --git a/research/f3-ternary-six-source/TASK.json b/research/f3-ternary-six-source/TASK.json new file mode 100644 index 0000000000..230c09c570 --- /dev/null +++ b/research/f3-ternary-six-source/TASK.json @@ -0,0 +1,86 @@ +{ + "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": "Exact unsigned F3 six-source complete-call optimum for all 728 nonzero ternary coefficient rows with one arbitrarily dirty restored connector (2208 calls), and a source-deletion averaging lower bound on extra call triples for every n >= 6.", + "scope_change_reason": "Takes the six-source open question of PR4238 in the same unchanged F3 alphabet. Increasing the source count without changing the alphabet is a changed assignment under the card's trigger; this is a local interface side result, not an alphabet extension or supplier admission.", + "bottleneck_link": "Side result. It closes the source count PR4238 left undecided and shows the gap above the operator-count floor grows (one extra triple at n = 5, two at n = 6, at least three at n = 7). No consumer or recursive saving is established.", + "budget_minutes": 60, + "stop_rule": "Stop after the deletion-averaging lower bound, one literal 2208-call witness with semantic checks and bounded controls. No census, exact n >= 7 value, price envelope or selected-frontier change.", + "outcome": "completed", + "evidence": "verify.py checks the 24-event witness path covers all 728 nonzero rows by boundary triple sums, checks the literal 2208-call word by a generic coefficient ledger and dense random F3 execution at dimensions 2 and 3 with dirty registers, checks that all six source deletions of the literal word are valid five-source words with extras [1,1,2,2,2,2], prints the extra-triple lower-bound table for n = 5..12 from the averaging recurrence and the counting bound, and runs five rejection controls. The lower bound uses PR4238's cited five-source census value e(5) = 1, which is not re-run here.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact seven-source optimum? The lower bound is 6588 calls (three extra triples).", + "why_it_matters": "It tests whether the averaging recurrence is sharp beyond n = 6.", + "first_step": "Search 30-event paths with three sources used six times for full coverage of the 2186 nonzero rows; a bounded annealing run reached 1952.", + "blocked_by": "No witness at the lower bound is known; proving a larger bound would need a new argument or a large census." + }, + { + "question": "Is the averaging recurrence sharp at n = 8, where it ties the counting bound at four extra triples?", + "why_it_matters": "Both bounds agree there, so one witness would settle n = 8 exactly.", + "first_step": "Search 36-event paths with four doubled sources for full coverage of 6560 rows.", + "blocked_by": "Not attempted." + }, + { + "question": "Does any concrete caller need full ternary rather than binary demand?", + "why_it_matters": "Without a consumer the extra calls are an interface fact, not a cost change.", + "first_step": "Identify an immutable-source, unobserved-output caller whose outputs use coefficient 2.", + "blocked_by": "No physical or selected-supplier consumer is instantiated." + } + ], + "predecessor_handoff": { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/4238", + "head": "191a905d7adba6695b079f744140a73e832787a8", + "author": "Nick Petalas", + "usage": "Interface, triple-prefix readout criterion, five-source census value e(5) = 1 and the explicit six-source open question; cited, not re-run, and no executable dependency." + }, + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19081265", + "upstream_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "overlap_scope": "100 live open PR titles; 60 recent account PRs; recent hub comments; find_overlap for connector-alphabet-change; title search for ternary; README grep on main. Closed work and arbitrary diffs are incompletely covered.", + "family_decision": "Narrow local interface result; stop. Consumer, complete primitive prices and admission remain unknown." + } +} diff --git a/research/f3-ternary-six-source/VERIFY.json b/research/f3-ternary-six-source/VERIFY.json new file mode 100644 index 0000000000..e611b9958b --- /dev/null +++ b/research/f3-ternary-six-source/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/universal-connector-boundary/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Source hash, 24-event witness coverage of all 728 rows, literal 2208-call word by generic ledger and dense F3 execution, six source-deletion projections, extra-triple lower-bound table n = 5..12, five rejection controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Repeat the complete certificate under optimized Python; checks use explicit exceptions, not assert." + } + ] +} diff --git a/research/f3-ternary-six-source/verify.py b/research/f3-ternary-six-source/verify.py new file mode 100644 index 0000000000..73deebe0bc --- /dev/null +++ b/research/f3-ternary-six-source/verify.py @@ -0,0 +1,282 @@ +#!/usr/bin/env python3 +"""Verify the exact six-source optimum for full ternary demand over F3. + +Interface (unchanged from #4225/#4238): immutable sources x_0..x_{n-1}, one +arbitrarily dirty connector z, outputs y_v for every nonzero v in F3^n, and only +the unsigned complete calls B_j: z += B_j x_j and A_v: y_v += A_v z. + +Checks, standard library only, no files written: + 1. the source pin of the interface README; + 2. the 24-event witness path covers every nonzero row of F3^6 by triple sums; + 3. the literal 2208-call word by a generic coefficient ledger and by dense + random F3 execution with dirty registers; + 4. the source-deletion lemma on the literal word (all six projections are + valid five-source words with the predicted extra counts); + 5. the extra-triple lower-bound table from the averaging recurrence and the + counting bound, starting from #4238's cited five-source value e(5) = 1; + 6. rejection controls. +""" + +from __future__ import annotations + +import hashlib +import itertools +import math +import random +from pathlib import Path + +N = 6 +Q = 3 +ROOT = Path(__file__).resolve().parents[2] +SOURCE = ROOT / "research/universal-connector-boundary/README.md" +SOURCE_SHA256 = "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + +# Restored 24-event source path: sources 0 and 1 occur six times, 2..5 three times. +PATH = (5, 4, 0, 1, 0, 3, 2, 4, 3, 1, 0, 1, 4, 5, 0, 1, 0, 2, 5, 3, 2, 1, 0, 1) +EXPECTED_CALLS = 2208 +FLOOR = 3 * N + 3 * (Q**N - 1) +# Cited from #4238 (head 191a905d7adba6695b079f744140a73e832787a8): the canonical +# five-source census shows the 741-call floor fails, and 744 is attained. +E5_CITED = 1 + + +def fail(message: str) -> None: + raise SystemExit("FAIL: " + message) + + +def check(condition: bool, message: str) -> None: + if not condition: + fail(message) + + +def add(u: tuple[int, ...], v: tuple[int, ...]) -> tuple[int, ...]: + return tuple((a + b) % Q for a, b in zip(u, v)) + + +def boundaries(path: tuple[int, ...], n: int) -> list[tuple[int, ...]]: + """Prefix count vectors q_0..q_{L-1} modulo three (q_L = q_0 = 0).""" + q = [0] * n + out = [tuple(q)] + for j in path[:-1]: + q[j] = (q[j] + 1) % Q + out.append(tuple(q)) + return out + + +def triple_readouts(path: tuple[int, ...], n: int) -> dict[tuple[int, ...], tuple[int, int, int]]: + """Lexicographically first boundary triple a <= b <= c for each covered row.""" + qs = boundaries(path, n) + first: dict[tuple[int, ...], tuple[int, int, int]] = {} + for a, b, c in itertools.combinations_with_replacement(range(len(qs)), 3): + first.setdefault(add(add(qs[a], qs[b]), qs[c]), (a, b, c)) + return first + + +def nonzero_rows(n: int) -> list[tuple[int, ...]]: + return [v for v in itertools.product(range(Q), repeat=n) if any(v)] + + +def build_word(path: tuple[int, ...], n: int) -> list[tuple[str, object]]: + """Interleave source calls and three readouts per row into one literal word.""" + first = triple_readouts(path, n) + at: dict[int, list[tuple[int, ...]]] = {} + for v in nonzero_rows(n): + if v not in first: + fail(f"row {v} is not a triple sum") + for t in first[v]: + at.setdefault(t, []).append(v) + word: list[tuple[str, object]] = [] + for t, j in enumerate(path): + word.extend(("A", v) for v in at.get(t, [])) + word.append(("B", j)) + return word + + +def ledger(word: list[tuple[str, object]], n: int) -> dict[tuple[int, ...], tuple[int, ...]]: + """Generic coefficients: y_v = c_z A_v z0 + sum_j c_j A_v B_j x_j (+ y_v0).""" + z = [1] + [0] * n # coefficient of z0, then of each B_j x_j + y: dict[tuple[int, ...], list[int]] = {} + for kind, arg in word: + if kind == "B": + z[1 + arg] = (z[1 + arg] + 1) % Q + else: + acc = y.setdefault(arg, [0] * (n + 1)) + for k in range(n + 1): + acc[k] = (acc[k] + z[k]) % Q + check(z == [1] + [0] * n, "connector is not restored") + return {v: tuple(c) for v, c in y.items()} + + +def word_valid(word: list[tuple[str, object]], n: int) -> bool: + try: + coeff = ledger(word, n) + except SystemExit: + return False + rows = nonzero_rows(n) + return set(coeff) == set(rows) and all(coeff[v] == (0,) + v for v in rows) + + +def counts(word: list[tuple[str, object]]) -> tuple[dict[object, int], dict[object, int]]: + b: dict[object, int] = {} + a: dict[object, int] = {} + for kind, arg in word: + target = b if kind == "B" else a + target[arg] = target.get(arg, 0) + 1 + return b, a + + +def extra_triples(word: list[tuple[str, object]], n: int) -> int: + b, a = counts(word) + total = sum(b.values()) + sum(a.values()) + floor = 3 * n + 3 * (Q**n - 1) + check((total - floor) % 3 == 0, "extra calls are not whole triples") + return (total - floor) // 3 + + +def matmul(m: list[list[int]], x: list[int]) -> list[int]: + return [sum(r * c for r, c in zip(row, x)) % Q for row in m] + + +def dense_run(word: list[tuple[str, object]], n: int, dim: int, rng: random.Random) -> bool: + def rmat() -> list[list[int]]: + return [[rng.randrange(Q) for _ in range(dim)] for _ in range(dim)] + + def rvec() -> list[int]: + return [rng.randrange(Q) for _ in range(dim)] + + bmaps = [rmat() for _ in range(n)] + amaps = {v: rmat() for v in nonzero_rows(n)} + xs = [rvec() for _ in range(n)] + z0 = rvec() + y0 = {v: rvec() for v in amaps} + z = list(z0) + y = {v: list(w) for v, w in y0.items()} + for kind, arg in word: + if kind == "B": + z = [(p + r) % Q for p, r in zip(z, matmul(bmaps[arg], xs[arg]))] + else: + y[arg] = [(p + r) % Q for p, r in zip(y[arg], matmul(amaps[arg], z))] + if z != z0: + return False + for v, a in amaps.items(): + want = list(y0[v]) + for j in range(n): + if v[j]: + term = matmul(a, matmul(bmaps[j], xs[j])) + want = [(p + v[j] * r) % Q for p, r in zip(want, term)] + if y[v] != want: + return False + return True + + +def delete_source(word: list[tuple[str, object]], j: int) -> list[tuple[str, object]]: + """Remove B_j and every A_v with v_j != 0; relabel the remaining coordinates.""" + out: list[tuple[str, object]] = [] + for kind, arg in word: + if kind == "B": + if arg != j: + out.append(("B", arg - (arg > j))) + elif arg[j] == 0: + out.append(("A", arg[:j] + arg[j + 1 :])) + return out + + +def counting_bound(n: int) -> int: + """Least extra triples forced by the number of distinct nonzero triple sums.""" + rows = Q**n - 1 + best = None + for s in range(0, 10**6): + length = 3 * n + 3 * s + cap = math.comb(length + 2, 3) - length + value = s + max(0, rows - cap) + best = value if best is None else min(best, value) + if s >= best: + return best + fail("counting bound did not terminate") + return -1 + + +def lower_bound_table(n_max: int) -> dict[int, tuple[int, int, int]]: + """n -> (recurrence bound, counting bound, combined), from e(5) = 1.""" + table = {5: (E5_CITED, counting_bound(5), max(E5_CITED, counting_bound(5)))} + for n in range(6, n_max + 1): + rec = -(-n * table[n - 1][2] // (n - 1)) + cnt = counting_bound(n) + table[n] = (rec, cnt, max(rec, cnt)) + return table + + +def main() -> None: + check(hashlib.sha256(SOURCE.read_bytes()).hexdigest() == SOURCE_SHA256, "interface source pin") + + # 2. witness coverage + check(len(PATH) == 24, "path length") + check([PATH.count(j) for j in range(N)] == [6, 6, 3, 3, 3, 3], "source counts") + rows = nonzero_rows(N) + first = triple_readouts(PATH, N) + covered = sum(1 for v in rows if v in first) + check(covered == 728 == len(rows), f"coverage {covered}") + + # 3. literal word + word = build_word(PATH, N) + b, a = counts(word) + check(len(word) == EXPECTED_CALLS, f"word length {len(word)}") + check(all(c % 3 == 0 and c >= 3 for c in b.values()), "source counts") + check(all(c == 3 for c in a.values()) and len(a) == 728, "readout counts") + check(word_valid(word, N), "generic ledger") + check(extra_triples(word, N) == 2, "extra triples of witness") + rng = random.Random(20261020) + for dim in (2, 3): + check(dense_run(word, N, dim, rng), f"dense F3 execution at dimension {dim}") + + # 4. deletion lemma on the literal word + projected_extras = [] + for j in range(N): + sub = delete_source(word, j) + check(word_valid(sub, N - 1), f"projection deleting source {j}") + check(dense_run(sub, N - 1, 2, rng), f"dense projection deleting source {j}") + projected_extras.append(extra_triples(sub, N - 1)) + # Sources 0, 1 carry one extra triple each; deleting one keeps the other. + check(projected_extras == [1, 1, 2, 2, 2, 2], f"projected extras {projected_extras}") + check(sum(projected_extras) <= (N - 1) * extra_triples(word, N), "averaging inequality") + check(min(projected_extras) >= E5_CITED, "five-source projections respect e(5)") + + # 5. lower-bound table + table = lower_bound_table(12) + check(table[6][2] == 2, "e(6) lower bound") + check(table[7][2] == 3 and table[8][2] == 4, "e(7), e(8) lower bounds") + check(FLOOR + 3 * table[6][2] == EXPECTED_CALLS, "optimum equals bound") + print("n recurrence counting combined lower_bound_calls") + for n, (rec, cnt, comb) in table.items(): + floor = 3 * n + 3 * (Q**n - 1) + print(f"{n:<2} {rec:>10} {cnt:>9} {comb:>9} {floor + 3 * comb:>18}") + + # 6. rejection controls + controls = 0 + broken = list(word) + del broken[next(i for i, w in enumerate(broken) if w[0] == "A")] + check(not word_valid(broken, N), "dropped readout accepted") + controls += 1 + broken = [w for w in word if w != ("B", 2)] + [("B", 2)] * 2 + check(not word_valid(broken, N), "two-call source accepted") + controls += 1 + broken = list(word) + i = next(k for k, w in enumerate(broken) if w[0] == "A") + v = broken[i][1] + broken[i] = ("A", tuple((c + 1) % Q for c in v) if v != (2,) * N else (1,) * N) + check(not word_valid(broken, N), "misrouted readout accepted") + controls += 1 + first_n5_path = (0, 1, 0, 2, 1, 0, 3, 2, 1, 4, 3, 2, 4, 3, 4) # #4238 gap path + check(len(triple_readouts(first_n5_path, 5)) - 1 == 241, "#4238 gap-path control") + controls += 1 + swapped = list(PATH) + swapped[0], swapped[1] = swapped[1], swapped[0] + check(len([v for v in rows if v in triple_readouts(tuple(swapped), N)]) < 728, "swap control") + controls += 1 + + print(f"controls={controls} projected_extras={projected_extras}") + print(f"PASS_F3_TERNARY_SIX_SOURCE calls={len(word)} floor={FLOOR} rows={len(rows)}") + + +if __name__ == "__main__": + main()