diff --git a/research/depth4-chain-tariff/README.md b/research/depth4-chain-tariff/README.md new file mode 100644 index 0000000000..1121b2637b --- /dev/null +++ b/research/depth4-chain-tariff/README.md @@ -0,0 +1,183 @@ +# Count vectors and prices for the depth-four dirty chain, m = 2..5 + +This package classifies every feasible call-count vector of the unsigned +depth-four dirty chain connector in characteristics m = 2, 3, 4, 5, for every +nonzero target residue and for words of any length. It is a scoped proof whose +completeness step is a finite reduction checked by computer. The contribution +was produced by Nick Petalas. + +The calls are `z_l += B_l z_{l-1}` for l = 1..4. The source x = z_0 is +immutable; z_1, z_2, z_3 and y = z_4 start dirty, and the maps are arbitrary. +A correct word restores z_1..z_3 and adds `c B4 B3 B2 B1 x` to y, 1 <= c < m. +Write n_l for the number of calls l. Let P(m) be the set of minimal correct +count vectors: + +```text +m = 2: P = {(2,4,4,2)} +m = 3: P = {(3,3,9,3), (3,6,6,3), (3,9,3,3)} +m = 4: P = {(4,4,8,4), (4,8,4,4)} +m = 5: P = {(10,5,5,5), (5,10,5,5), (5,5,10,5), (5,5,5,10)} +``` + +**Theorem.** For m in {2,3,4,5} and every c != 0 mod m, a count vector is +attained by a correct word if and only if every n_l is a multiple of m and n +dominates some member of P(m) coordinate by coordinate. P(m) does not depend +on c. + +With positive complete-call prices p_1..p_4 and S = p_1 + p_2 + p_3 + p_4, +the exact cheapest bill is therefore + +```text +m = 2: 2S + 2(p2 + p3) +m = 3: 3S + 6 min(p2, p3) +m = 4: 4S + 4 min(p2, p3) +m = 5: 5S + 5 min(p1, p2, p3, p4) +``` + +At unit prices this recovers the minimum lengths 12, 18, 20, 25 of PR4249. +The new information is where the premium sits. In characteristics two, three +and four it is paid only on the two middle operations: no minimal word doubles +the first or last call, however cheap those calls are. At m = 3 the profile +(3,6,6,3) is minimal but is optimal only when p2 = p3. In characteristic five +any one operation can be doubled. + +For 6 <= m <= 32, PR4263's balanced witnesses give P(m) = {(m,m,m,m)} and the +bill mS by the divisibility argument below. That is a corollary of cited +pending work, not rechecked here. For m >= 33 the classification is open. + +## Proof + +**Interval counts.** Let N_ij (1 <= i <= j <= 4) count scattered subwords +`i (i+1) ... j` of the word. As in PR4249 and PR4257, appending letter j adds +N_{i,j-1} to N_ij for i < j and increments N_jj, so + +```text +z_j(final) = z_j(initial) + sum_{i<=j} N_ij B_j ... B_i z_{i-1}(initial). +``` + +A word is correct exactly when all ten counts vanish mod m except N_14 = c. +Sufficiency is this identity. For necessity take every module to be the ring, +every map the identity, and switch on one initial register at a time. Then +each n_l = N_ll is a multiple of m, and positive, since n_l = 0 forces +N_14 = 0. Appending m copies of any letter acts as the identity, so any +correct count vector stays correct after adding a multiple of m to one +coordinate. The witnesses in [witnesses.json](witnesses.json) attain every +member of P(m) for every c, and padding gives sufficiency. + +**Reduction to the middle letters.** Fix the order of the 2s and 3s. Let +A[i][j] = 1 when the i-th 2 precedes the j-th 3, let u_i count the 1s before +the i-th 2 and let r_j count the 4s after the j-th 3. A 1 only matters through +which 2s follow it, and a 4 only through which 3s precede it. So + +```text +N12 = sum u, N13 = u . A1, N23 = 1'A1, N34 = sum r, +N24 = r . A'1, N14 = u' A r, N11 = n1, N22 = n2, N33 = n3, N44 = n4. +``` + +For exact counts, u is nondecreasing in [0, n1] and r is nonincreasing in +[0, n4]. If n1 and n4 are left free, u and r range over all residue vectors: +every residue vector lifts to a nondecreasing integer sequence, and 1s after +the last 2 (or 4s before the first 3) change only N11 (or N44), which is then +padded to a multiple of m. The verifier implements both versions as engine A. + +**Completeness.** It remains to show that no correct vector misses P(m). + +- m = 5. A vector of positive multiples of 5 that dominates no single doubling + is (5,5,5,5). Engine A with exact counts finds N14 = 0 for every correct + remainder of such a word, for every c. +- m = 4. A vector that dominates neither (4,4,8,4) nor (4,8,4,4) has + n2 = n3 = 4, with n1 and n4 arbitrary. Over all 70 orders of four 2s and + four 3s and all residue vectors u, r, the relaxed engine never reaches a + nonzero N14 once the other nine conditions hold. +- m = 3. A vector that dominates no member of P(3) has (n2, n3) in + {(3,3), (3,6), (6,3)}, with n1 and n4 arbitrary. The relaxed engine again + reaches only N14 = 0. +- m = 2. A vector that dominates no member has n2 = 2 or n3 = 2. Suppose + n2 = 2. Then N12 = u1 + u2 = 0 mod 2, so u1 = u2. Every subword 1234 is a 1, + then a 2, then a subword 34 after that 2. If t_i counts the subwords 34 after + the i-th 2, then N14 = u1 t1 + u2 t2 = u1 (t1 + t2) = u1 N24 = 0, which is + not c = 1. Reversing a word and relabelling l -> 5 - l preserves correctness + and swaps n2 with n3, which covers n3 = 2. + +The relaxations leave n1 and n4 unbounded, so this covers words of any +length, not a bounded search. Positive controls show the relaxed engine does +reach every residue on the adjacent feasible middle pairs: (3,9), (6,6), (9,3) +at m = 3, and (4,8), (8,4) at m = 4. At m = 5 it reaches every residue at +n2 = n3 = 5, which is why m = 5 needs the exact outer counts. QED. + +Prices: every optimum has its count vector in P(m), because a strictly larger +feasible vector costs strictly more at positive prices. Minimizing over P(m) +gives the table above, using p2 + p3 >= 2 min(p2, p3) at m = 3. + +## Verification + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/depth4-chain-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/depth4-chain-tariff/verify.py +``` + +Both print `PASS_DEPTH4_CHAIN_TARIFF witnesses=29 replays=87 +box_comparisons=125 cross_checks=116` and a receipt hash over every package +file and source input. The verifier uses only the standard library and takes +about 70 seconds. It checks: + +1. all 29 witness words, one per (m, c, Pareto vector): exact counts, the ten + interval conditions, an independent UT5(Z/m) matrix product, and three + literal replays each with dirty registers and random noncommuting 2x2 maps; +2. the relaxed engine on each missed middle pair for m = 3, 4, and its + positive controls; +3. the exact engine at (5,5,5,5) and the m = 2 lemma on n2 = 2 with the other + counts in {2,4,6}, plus the mirror symmetry on the binary witness; +4. engine B, a direct DP over the six non-diagonal interval residues, on the + boxes [2,6]^4 at m = 2, [3,6]^4 at m = 3 and [4,8]x{4}x{4}x[4,8] at m = 4. + For all 125 (vector, residue) cases it agrees with the claimed cone, and in + the 116 cases with every count at most 6 it also agrees with engine A; +5. controls: an adjacent swap, a wrong residue, a wrong-residue replay, the + 4m floor at m = 4, and an exact-engine positive case. + +`witnesses.json` was produced by a seeded local annealing search that is not +part of the package; the verifier checks the words themselves. + +## Related work + +- PR4249 (Nick Petalas) supplies the chain model and the depth-four minimum + lengths 12, 18, 20, 25. The unit-price case of the tariff table agrees with + all four values. +- PR4257 (Nick Petalas) is the depth-three count classification. Its + divisibility and padding arguments are reused; its exceptional profiles + are one level shorter and share no number with this table. +- PR4263 (Nick Petalas) attains 4m for 6 <= m <= 32. It is used only for the + cited corollary above. + +## Attribution and scope + +The complete-call connector interface comes from Ross Richardson's +PR943/PR934 lineage and the +[universal connector](../universal-connector-boundary/README.md). +[SOURCES.json](SOURCES.json) pins the main-tree provenance and the exact +heads of PR4249, PR4257 and PR4263. Scattered-subword counting is classical. + +The `connector-alphabet-change` card is explicitly changed to a pricing side +question in [TASK.json](TASK.json). The alphabet is unchanged and no operation +is declared free. Prices must cover complete calls. Admission, instruction +dispatch, coefficient preparation, routing of three dirty intermediates, +precision, stock and supplier/outer transfer remain separate obligations. +There is no supplier caller, selected-frontier change, new κ, formal-kernel +proof or complete multiplication theorem. Independent human and formal +proof-kernel review are unclaimed. Apache-2.0. + +## Open next questions + +The structured versions in TASK.json give first steps and blockers. + +1. What is P(m) for m >= 33? It is {(m,m,m,m)} exactly when the balanced + vector is feasible, which PR4263 shows only up to m = 32. +2. How many words attain each Pareto vector? PR4257 recorded the depth-three + counts; a counting DP at length 25 needs a sparser encoding for CI. +3. Which operations carry the premium at depth five? Here the outer calls are + never doubled at m = 2, 3, 4, but any call can be at m = 5. The same + middle-letter reduction applies with three inner letters. +4. Can a concrete recursive caller with three dirty intermediates use one of + these profiles at a favorable complete physical cost? diff --git a/research/depth4-chain-tariff/SOURCES.json b/research/depth4-chain-tariff/SOURCES.json new file mode 100644 index 0000000000..33283b40fe --- /dev/null +++ b/research/depth4-chain-tariff/SOURCES.json @@ -0,0 +1,44 @@ +{ + "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" + } + ], + "literature": [ + { + "pr": 4249, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4249", + "commit": "03b8a19d7442edebb3565064631f6ca2408d731e", + "use": "Chain model, interval-count reduction and the depth-four minimum lengths 12, 18, 20, 25 at m = 2..5. Cited; no executable or foreign Git object is required." + }, + { + "pr": 4257, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4257", + "commit": "91b4e49d0b80b0d8589f6e2cb23a0af75422e91b", + "use": "Depth-three count classification and the padding and divisibility arguments reused at depth four." + }, + { + "pr": 4263, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4263", + "commit": "2183322b32a5975ecb4a6aec2ec8f43ac08b1aec", + "use": "Balanced 4m witnesses for 6 <= m <= 32, used only for the cited corollary that the tariff there is m times the price sum." + } + ] +} diff --git a/research/depth4-chain-tariff/TASK.json b/research/depth4-chain-tariff/TASK.json new file mode 100644 index 0000000000..f274970d3d --- /dev/null +++ b/research/depth4-chain-tariff/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": "Classify all feasible unsigned depth-four dirty-chain call-count vectors and the exact positive unequal-price tariff in characteristics m = 2..5 for every nonzero target residue, for words of any length; record the cited corollary for 6 <= m <= 32.", + "scope_change_reason": "The operation alphabet is unchanged. This is a pricing and count-feasibility side result extending PR4257 from depth three to depth four, using the depth-four minima of PR4249, rather than a new supplier operation.", + "bottleneck_link": "A completed call can carry a different cost at each chain port. At small characteristic the depth-four premium can only be paid on specific operations (the middle two at m = 2, 3, 4), which unit length alone does not show. No actual supplier consumer is supplied.", + "budget_minutes": 60, + "stop_rule": "Stop with the count classification for m = 2..5 proved by an unbounded reachability reduction plus bounded corroboration, or report a counterexample; no m >= 33 search, multiplicity census or supplier expansion.", + "outcome": "completed", + "evidence": "README.md gives the reduction and proofs; verify.py checks witness words (interval counts, UT5 product, literal dirty replay), the outer-free relaxation on every missed middle pair, the exact m = 5 balanced exclusion, a direct interval-state DP against the claimed cone and against the exact reduction engine on boxes, controls and a generated source-hash receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What are the depth-four Pareto count vectors for m >= 33?", + "why_it_matters": "The tariff is m times the price sum exactly when the balanced vector is feasible; PR4263 shows this only for 6 <= m <= 32.", + "first_step": "Search balanced words at m = 33..40 with PR4263's annealer, or find a parametric family of the three interleaving sequences.", + "blocked_by": "No all-m depth-four construction is known." + }, + { + "question": "How many words attain each depth-four Pareto vector?", + "why_it_matters": "Schedule freedom at the cheapest profile may matter for routing in a caller; PR4257 recorded the analogous depth-three counts.", + "first_step": "Run a counting version of the interval-state DP at each Pareto vector; the m = 5 vectors have length 25.", + "blocked_by": "A pure-Python count at m = 5 needs a sparser state encoding to stay within the CI time limit." + }, + { + "question": "Which operations carry the premium at depth five?", + "why_it_matters": "At m = 2, 3, 4 the first and last operations are never doubled at a minimum; at m = 5 every single doubling is minimal. A depth-five analogue would show which ports carry the premium.", + "first_step": "Apply the same reduction with the inner letters bounded and the outer letters as prefix/suffix residues.", + "blocked_by": "Depth-five minimum lengths are not yet known." + } + ] +} diff --git a/research/depth4-chain-tariff/VERIFY.json b/research/depth4-chain-tariff/VERIFY.json new file mode 100644 index 0000000000..ba540ff346 --- /dev/null +++ b/research/depth4-chain-tariff/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json", + "research/universal-connector-boundary/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 420, + "checks": "Pareto witnesses with UT5 product and literal dirty replay; unbounded outer-free completeness for m = 3, 4; m = 2 lemma check; exact m = 5 balanced exclusion; direct DP versus claimed cone and exact engine; controls; source-hash receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 420, + "checks": "Same checks under -O; every check uses explicit require(), not assert." + } + ] +} diff --git a/research/depth4-chain-tariff/verify.py b/research/depth4-chain-tariff/verify.py new file mode 100644 index 0000000000..a101af7e76 --- /dev/null +++ b/research/depth4-chain-tariff/verify.py @@ -0,0 +1,313 @@ +#!/usr/bin/env python3 +"""Verify the depth-four dirty chain count-vector classification for m = 2..5. + +Standard library only. The calls are z_l += B_l z_{l-1} (l = 1..4) with x = z_0 +immutable, dirty z_1..z_3 and y = z_4. A word is correct for (m, c) when its +interval subword counts N_ij (1 <= i <= j <= 4) vanish mod m, except N_14 = c. + +Checks: + 1. every Pareto witness word: counts, interval conditions, an independent + UT5(Z/m) product and literal dirty replay with noncommuting maps; + 2. completeness for words of any length: + m = 2: the two-middle-call lemma, checked on a bounded box; + m = 3, 4: the outer-free relaxation has no solution on the ideals + missed by the Pareto set (1s and 4s unbounded); + m = 5: the balanced vector (5,5,5,5) is infeasible; + 3. a second engine (direct interval-state DP) on bounded boxes, compared + with the exact reduction engine vector by vector; + 4. positive and negative controls, and a generated source-hash receipt. +""" +import hashlib +import itertools +import json +import random +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent + +INTERVALS = [(i, j) for i in range(1, 5) for j in range(i, 5)] +PARETO = { + 2: [(2, 4, 4, 2)], + 3: [(3, 3, 9, 3), (3, 6, 6, 3), (3, 9, 3, 3)], + 4: [(4, 4, 8, 4), (4, 8, 4, 4)], + 5: [(10, 5, 5, 5), (5, 10, 5, 5), (5, 5, 10, 5), (5, 5, 5, 10)], +} +# (n2, n3) pairs with n1, n4 unbounded that a non-dominating vector can have. +MISSED_MIDDLE = {3: [(3, 3), (3, 6), (6, 3)], 4: [(4, 4)]} +# Outer-free middle pairs that must be feasible (positive controls). +HIT_MIDDLE = {3: [(3, 9), (6, 6), (9, 3)], 4: [(4, 8), (8, 4)]} +# Direct-DP boxes: top count per letter. Engine A is compared wherever every +# count is at most ENGINE_A_CAP (its cost grows binomially). +BOX = {2: (6, 6, 6, 6), 3: (6, 6, 6, 6), 4: (8, 4, 4, 8)} +ENGINE_A_CAP = 6 + + +def require(cond, msg): + if not cond: + raise SystemExit(f"FAIL: {msg}") + + +def target(m, c): + return {k: (c % m if k == (1, 4) else 0) for k in INTERVALS} + + +def interval_counts(word, m): + """Interval subword counts by the append recurrence.""" + n = {k: 0 for k in INTERVALS} + for letter in word: + for i in range(letter - 1, 0, -1): + n[(i, letter)] = (n[(i, letter)] + n[(i, letter - 1)]) % m + n[(letter, letter)] = (n[(letter, letter)] + 1) % m + return n + + +def ut5_product(word, m): + """Independent check: product of elementary matrices I + E_{l,l-1}.""" + mat = [[int(r == s) for s in range(5)] for r in range(5)] + for letter in word: + # left-multiply by I + E_{letter, letter-1}: row letter += row letter-1 + mat[letter] = [(a + b) % m for a, b in zip(mat[letter], mat[letter - 1])] + return mat + + +def mat_mul(a, b, m): + return [[sum(a[i][k] * b[k][j] for k in range(len(b))) % m + for j in range(len(b[0]))] for i in range(len(a))] + + +def mat_add(a, b, m): + return [[(x + y) % m for x, y in zip(ra, rb)] for ra, rb in zip(a, b)] + + +def literal_replay(word, m, c, rng, dim=2): + """Run the word on dirty registers with random dim x dim maps over Z/m.""" + rand = lambda r, s: [[rng.randrange(m) for _ in range(s)] for _ in range(r)] + maps = {l: rand(dim, dim) for l in range(1, 5)} + init = [rand(dim, 1) for _ in range(5)] + reg = [[row[:] for row in v] for v in init] + for letter in word: + reg[letter] = mat_add(reg[letter], mat_mul(maps[letter], reg[letter - 1], m), m) + for l in range(4): + if reg[l] != init[l]: + return False + chain = init[0] + for l in range(1, 5): + chain = mat_mul(maps[l], chain, m) + want = mat_add(init[4], [[(c * v) % m for v in row] for row in chain], m) + return reg[4] == want + + +def check_word(word, m, c, n): + require([word.count(l) for l in range(1, 5)] == list(n), f"counts {m},{c},{n}") + require(interval_counts(word, m) == target(m, c), f"intervals {m},{c},{n}") + prod = ut5_product(word, m) + for r in range(5): + for s in range(5): + want = 1 if r == s else (c % m if (r, s) == (4, 0) else 0) + require(prod[r][s] == want, f"UT5 product {m},{c},{n}") + + +# ---- Engine A: exact reduction over the middle letters -------------------- +# +# A word is determined, for all interval counts, by: the interleaving of its +# 2s and 3s; u_i = number of 1s before the i-th 2; r_j = number of 4s after +# the j-th 3. With A[i][j] = 1 when the i-th 2 precedes the j-th 3: +# N12 = sum u, N13 = sum_i u_i b_i (b = A 1), N23 = 1'A1, +# N34 = sum r, N24 = sum_j r_j a_j (a = A'1), N14 = u'A r, +# N11 = n1, N22 = n2, N33 = n3, N44 = n4. +# Exact counts: u nondecreasing in [0, n1], r nonincreasing in [0, n4]. +# Outer-free relaxation (n1, n4 unbounded): u, r arbitrary residue vectors, +# because nondecreasing integer lifts exist and 1s after the last 2 (4s before +# the first 3) change only N11 (N44). + +def patterns(n2, n3): + for pos in itertools.combinations(range(n2 + n3), n2): + s = set(pos) + yield [2 if k in s else 3 for k in range(n2 + n3)] + + +def pattern_matrix(pat): + twos = threes = 0 + seen2 = [] # number of 2s before each 3 + for letter in pat: + if letter == 2: + twos += 1 + else: + seen2.append(twos) + threes += 1 + # A[i][j] = 1 iff i < seen2[j] + return [[int(i < seen2[j]) for j in range(threes)] for i in range(twos)] + + +def monotone(length, top, decreasing=False): + for combo in itertools.combinations_with_replacement(range(top + 1), length): + yield combo[::-1] if decreasing else combo + + +def reduced_values(m, n, outer_free): + """Set of N14 residues over correct-except-N14 words (None if N23 fails).""" + n1, n2, n3, n4 = n + if not outer_free and (n1 % m or n4 % m): + return set() + if n2 % m or n3 % m: + return set() + values = set() + for pat in patterns(n2, n3): + a = pattern_matrix(pat) + if sum(map(sum, a)) % m: + continue + b = [sum(row) for row in a] + col = [sum(a[i][j] for i in range(n2)) for j in range(n3)] + if outer_free: + us = itertools.product(range(m), repeat=n2) + rs = itertools.product(range(m), repeat=n3) + else: + us = monotone(n2, n1) + rs = monotone(n3, n4, decreasing=True) + good_u = [u for u in us if sum(u) % m == 0 + and sum(x * y for x, y in zip(u, b)) % m == 0] + good_r = [r for r in rs if sum(r) % m == 0 + and sum(x * y for x, y in zip(r, col)) % m == 0] + if not good_u or not good_r: + continue + for u in good_u: + ua = [sum(u[i] * a[i][j] for i in range(n2)) % m for j in range(n3)] + for r in good_r: + values.add(sum(x * y for x, y in zip(ua, r)) % m) + return values + + +# ---- Engine B: direct DP over interval states ------------------------------ + +def dp_box(m, top): + """Reachable interval-residue states for every count vector in [0,top]^4.""" + keys = [(1, 2), (2, 3), (3, 4), (1, 3), (2, 4), (1, 4)] + table = {(0, 0, 0, 0): {(0,) * 6}} + for a in itertools.product(range(top[0] + 1), range(top[1] + 1), + range(top[2] + 1), range(top[3] + 1)): + if a == (0, 0, 0, 0): + continue + out = set() + for l in range(4): + if a[l] == 0: + continue + prev = list(a) + prev[l] -= 1 + prev = tuple(prev) + for st in table[prev]: + n12, n23, n34, n13, n24, n14 = st + if l == 1: + n12 = (n12 + prev[0]) % m + elif l == 2: + n13 = (n13 + n12) % m + n23 = (n23 + prev[1]) % m + elif l == 3: + n14 = (n14 + n13) % m + n24 = (n24 + n23) % m + n34 = (n34 + prev[2]) % m + out.add((n12, n23, n34, n13, n24, n14)) + table[a] = out + return table, keys + + +def dominates(n, p): + return all(x >= y for x, y in zip(n, p)) + + +def main(): + witnesses = json.loads((HERE / "witnesses.json").read_text()) + rng = random.Random(20261021) + replays = 0 + + # 1. witnesses for every (m, c, Pareto vector) + for m, vecs in PARETO.items(): + for c in range(1, m): + for n in vecs: + key = f"{m},{c},{''.join(map(str, n))}" + word = [int(ch) for ch in witnesses[key]] + check_word(word, m, c, n) + for _ in range(3): + require(literal_replay(word, m, c, rng), f"replay {key}") + replays += 1 + require(len(witnesses) == sum(len(v) * (m - 1) for m, v in PARETO.items()), + "witness inventory") + + # 2a. m = 2 lemma: exactly two 2s (or two 3s) force N14 = 0. Proof in + # README; here: engine A with n2 = 2 over a box of n1, n3, n4, and the + # mirror image (word reversal, l -> 5 - l) sends n3 = 2 to n2 = 2. + for n1, n3, n4 in itertools.product((2, 4, 6), repeat=3): + vals = reduced_values(2, (n1, 2, n3, n4), outer_free=False) + require(1 not in vals, f"m=2 lemma n=({n1},2,{n3},{n4})") + word = [int(ch) for ch in witnesses["2,1,2442"]] + mirror = [5 - l for l in reversed(word)] + require(interval_counts(mirror, 2) == target(2, 1), "mirror symmetry") + + # 2b. m = 3, 4: outer-free relaxation on every missed middle pair. + for m, pairs in MISSED_MIDDLE.items(): + for n2, n3 in pairs: + vals = reduced_values(m, (0, n2, n3, 0), outer_free=True) + require(vals <= {0}, f"outer-free m={m} ({n2},{n3}) hits {vals}") + for n2, n3 in HIT_MIDDLE[m]: + vals = reduced_values(m, (0, n2, n3, 0), outer_free=True) + require(vals == set(range(m)), f"control m={m} ({n2},{n3}) {vals}") + + # 2c. m = 5: the balanced vector misses every nonzero target, and the + # outer-free relaxation is not enough (control: it does hit). + vals5 = reduced_values(5, (5, 5, 5, 5), outer_free=False) + require(vals5 <= {0}, f"m=5 balanced hits {vals5}") + require(reduced_values(5, (0, 5, 5, 0), outer_free=True) == set(range(5)), + "m=5 outer-free control") + + # 3. engine B versus engine A and the claimed up-closure on boxes. + compared = cross = 0 + for m, top in BOX.items(): + table, keys = dp_box(m, top) + for n in itertools.product(*(range(m, t + 1, m) for t in top)): + reach = table[n] + for c in range(1, m): + want = (0, 0, 0, 0, 0, c) + direct = want in reach + claimed = any(dominates(n, p) for p in PARETO[m]) + require(direct == claimed, f"box m={m} n={n} c={c}") + if max(n) <= ENGINE_A_CAP: + exact = c in reduced_values(m, n, outer_free=False) + require(exact == direct, f"engines disagree m={m} n={n} c={c}") + cross += 1 + compared += 1 + + # 4. negative controls + bad = [int(ch) for ch in witnesses["4,1,4484"]] + swapped = bad[:] + i = next(k for k in range(len(bad) - 1) if bad[k] != bad[k + 1]) + swapped[i], swapped[i + 1] = swapped[i + 1], swapped[i] + require(interval_counts(swapped, 4) != target(4, 1), "swap control") + require(interval_counts(bad, 4) != target(4, 2), "residue control") + require(not all(literal_replay(bad, 4, 2, random.Random(s)) for s in range(8)), + "replay control") + require(reduced_values(4, (4, 4, 4, 4), outer_free=False) <= {0}, "floor control") + require(reduced_values(3, (3, 6, 6, 3), outer_free=False) == {0, 1, 2}, + "exact engine control") + + # receipt + hashes = {} + for path in sorted(HERE.iterdir()): + if path.is_file() and path.suffix in {".py", ".json", ".md"}: + hashes[f"package/{path.name}"] = hashlib.sha256(path.read_bytes()).hexdigest() + sources = json.loads((HERE / "SOURCES.json").read_text()) + for row in sources["files"]: + actual = hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() + require(actual == row["sha256"], f"input hash mismatch: {row['path']}") + hashes[row["path"]] = actual + receipt = {"pareto": {str(m): v for m, v in PARETO.items()}, + "witnesses": len(witnesses), "replays": replays, + "box_comparisons": compared, "engine_cross_checks": cross, "sha256": hashes} + digest = hashlib.sha256(json.dumps(receipt, sort_keys=True).encode()).hexdigest() + print(json.dumps(receipt, sort_keys=True, indent=1)) + print(f"PASS_DEPTH4_CHAIN_TARIFF witnesses={len(witnesses)} replays={replays} " + f"box_comparisons={compared} cross_checks={cross} receipt_sha256={digest}") + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/research/depth4-chain-tariff/witnesses.json b/research/depth4-chain-tariff/witnesses.json new file mode 100644 index 0000000000..18f1b209bb --- /dev/null +++ b/research/depth4-chain-tariff/witnesses.json @@ -0,0 +1,31 @@ +{ + "2,1,2442": "212343212343", + "3,1,3393": "343132343132134332", + "3,1,3663": "421232432113233432", + "3,1,3933": "123242123422123242", + "3,2,3393": "331432331432334132", + "3,2,3663": "231123433221234243", + "3,2,3933": "321224342122321224", + "4,1,4484": "34231423432312134133", + "4,1,4844": "23124134422212342321", + "4,2,4484": "34323343131234342112", + "4,2,4844": "12221343242142234321", + "4,3,4484": "32431421333143213234", + "4,3,4844": "34231212342341421222", + "5,1,10555": "1432411342131124341111232", + "5,1,51055": "4242421213423212231234312", + "5,1,55105": "4343331231412322314143323", + "5,1,55510": "4342443124413241321344214", + "5,2,10555": "2431411232141342113411213", + "5,2,51055": "1423144222122432413233122", + "5,2,55105": "1432334331131234413432232", + "5,2,55510": "3142341241443244132344124", + "5,3,10555": "4111132413124342111324312", + "5,3,51055": "4212424234122311223314232", + "5,3,55105": "3321233244321344323311134", + "5,3,55510": "4143442443142134442312312", + "5,4,10555": "1114321413121143423142321", + "5,4,51055": "2212322124234134213124234", + "5,4,55105": "3334312133344231324143212", + "5,4,55510": "4144213231421344234142434" +} \ No newline at end of file