From 78c77c5e8b0d3d1988f4cd9d72b9382d818cff43 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 13:36:09 +0000 Subject: [PATCH] feat(research): save 22 disjoint-triple roles via a descendant tie --- .../disjoint-descendant-traversal/PROOF.md | 81 +++++++ .../disjoint-descendant-traversal/README.md | 118 ++++++++++ .../SOURCES.json | 60 +++++ .../disjoint-descendant-traversal/TASK.json | 97 ++++++++ .../VALIDATION.md | 62 +++++ .../disjoint-descendant-traversal/VERIFY.json | 42 ++++ .../construction.py | 62 +++++ .../disjoint-descendant-traversal/verify.py | 218 ++++++++++++++++++ 8 files changed, 740 insertions(+) create mode 100644 research/disjoint-descendant-traversal/PROOF.md create mode 100644 research/disjoint-descendant-traversal/README.md create mode 100644 research/disjoint-descendant-traversal/SOURCES.json create mode 100644 research/disjoint-descendant-traversal/TASK.json create mode 100644 research/disjoint-descendant-traversal/VALIDATION.md create mode 100644 research/disjoint-descendant-traversal/VERIFY.json create mode 100644 research/disjoint-descendant-traversal/construction.py create mode 100644 research/disjoint-descendant-traversal/verify.py diff --git a/research/disjoint-descendant-traversal/PROOF.md b/research/disjoint-descendant-traversal/PROOF.md new file mode 100644 index 0000000000..c10476b5a4 --- /dev/null +++ b/research/disjoint-descendant-traversal/PROOF.md @@ -0,0 +1,81 @@ +# Exact finite map and complete historical charges + +For ordered ground points P, let D_(a,b)(P) send each a-subset input to the +sum of inputs disjoint from each b-subset target. Splitting P into L and R, +the channel with source-left cardinality i and target-left cardinality j +is `D_(i,j)(L) tensor D_(a-i,b-j)(R)`. Applying these two tensor factors in +either order gives the same integer map. This equality holds on arbitrary +inputs and needs no cancellation or approximation. + +The constructor changes only subproblems of shape `(n,a,b)=(11,2,2)`. +The pinned planner splits them into five and six ground points. In channel +`(i,j)=(1,1)`, the left-first and right-first unshared costs are both 146; +the constructor checks this equality explicitly. It takes the opposite order +from the planner. All other channels and all root choices stay as in #981. +The argument above proves that every changed subproblem still computes +D_(2,2)(11), and hence the full circuit computes D_(3,3)(22). + +Every addition combines disjoint source families. Retaining the first +binary decomposition of an already existing support leaves its integer +coefficient vector unchanged. Pruning unreachable nodes also leaves all +output vectors unchanged. Different factor orders can expose different +previously interned supports, so their equal unshared costs need not give +equal final DAG sizes. The finite checker derives the 30,676 retained +additions from this new DAG. It derives every output vector independently +from the set-theoretic predicate `S intersect T is empty`. This establishes +all 1,540 by 1,540 coefficients, with both zero and nonzero coefficients +included. The count is a certificate of this construction, not a lower bound +on other possible circuits. + +The retained compiler gives c+v roles for c additions and v outputs. Here +c=30,676 and v=1,540, giving 32,216 roles. Every compiled operation first adds +its other input roles into its pivot, then adds the pivot into its distinct +fanout roles. It is an invertible integer linear map. Subtract the pivot +from the fanout roles first, then subtract the other input roles from the +pivot to invert it. The slot-alias checks ensure these instructions have +the stated meaning. Thus arbitrary dirty values are permitted in the mixer +and returned by its literal inverse. The clean source-to-output block is +checked separately by full symbolic support replay. The retained twelve-step +signed invocation can therefore reuse this block while cancelling every +initial side value, exactly under its existing boundary contract. + +For any active node, let A be the union of ground points of ancestor source +triples, and B the union of reachable target triples. Every such source +triple is disjoint from every such target triple, since coefficients are +positive and every output row has exactly the required support. Thus A and +B are disjoint. The phase enclosure in the pinned +`notes/disjoint-tensor-compression.tex` applies to any such DAG, rather than +only its original factor choices. Source lines, coordinate spaces and target +complements remain nested with the same norm-one residual witnesses. +The retained checker traverses both actual physical orientations of the new +compiled circuit. It checks the case conditions for every transition; it +does not explicitly construct the 104,897 residual bases. + +For the complete historical invoice, retain h=22, v=binomial(h,3)=1,540, +intersection-two roles `R2=binomial(h,2)*(4*(h-2)-6)=17094` and h+1 centres. +The source proof gives + +```text +R0 = c+v +M = 2c+2*binomial(h,2)*(3*(h-2)-6) +C = J = 4v +S_inv = 4M+2C+4J+18v +S_all = 3v^2*S_inv +W = 2v^3+2v^2*(R0+R2+h+1) +m = h^3 +L = 3v^2*h*(h+1) +s = W*m-2v^3+2L +E = 64*(W+m+1)^3 +``` + +These formulas keep every mixer or inverse, source access, injection, +restoration, centre, intersection-two role, join and recursive child in the +same historical contract. The checker evaluates them at the new c, obtaining +`S_inv=409880`, `S_all=2916214224000`, `W=241300813600` and +`s=2569370958862400`. It also checks `2<=s 5 or 4 - i - j > 6: + continue + cost_left = plan(5, i, j)[0] + cost_right = plan(6, 2 - i, 2 - j)[0] + lr = comb(6, 2 - i) * cost_left + comb(5, j) * cost_right + rl = comb(5, i) * cost_right + comb(6, 2 - j) * cost_left + left_first = lr <= rl + if (i, j) == (1, 1): + if lr != 146 or rl != 146: + raise ValueError('the changed channel must remain a 146/146 tie') + left_first = not left_first + if left_first: + middle = { + s: self.transform(left, i, j, { + r: values[r | s] for r in subsets(left, i)}) + for s in subsets(right, 2 - i)} + for target in subsets(left, j): + row = self.transform(right, 2 - i, 2 - j, { + s: mapped[target] for s, mapped in middle.items()}) + for other, node in row.items(): + terms[target | other].append(node) + else: + middle = { + s: self.transform(right, 2 - i, 2 - j, { + r: values[r | s] for r in subsets(right, 2 - i)}) + for s in subsets(left, i)} + for target in subsets(right, 2 - j): + row = self.transform(left, i, j, { + s: mapped[target] for s, mapped in middle.items()}) + for other, node in row.items(): + terms[target | other].append(node) + return {target: self.total(nodes) for target, nodes in terms.items()} diff --git a/research/disjoint-descendant-traversal/verify.py b/research/disjoint-descendant-traversal/verify.py new file mode 100644 index 0000000000..1af0fadd7d --- /dev/null +++ b/research/disjoint-descendant-traversal/verify.py @@ -0,0 +1,218 @@ +"""Exact finite certificate for the new descendant circuit; no new kappa. + +Produced by Nick Petalas. Apache-2.0. Standard library only. +""" +import hashlib +from itertools import combinations +import json +from math import comb +from pathlib import Path +import platform +import sys +import time + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def source_hashes(): + sources = json.loads((PACKAGE / 'SOURCES.json').read_text()) + hashes = {} + require(len(sources['files']) <= 16, 'source inventory bound') + for row in sources['files']: + if row['usage'] == 'input': + digest = hashlib.sha256((ROOT / row['path']).read_bytes()).hexdigest() + require(digest == row['sha256'], 'changed source: ' + row['path']) + hashes[row['path']] = digest + for path in sorted(PACKAGE.iterdir()): + if path.is_file(): + hashes[path.relative_to(ROOT).as_posix()] = hashlib.sha256(path.read_bytes()).hexdigest() + return hashes + + +def triple_masks(): + return tuple(sum(1 << point for point in triple) + for triple in combinations(range(22), 3)) + + +def check_dag(circuit): + inputs = triple_masks() + require(tuple(circuit.inputs) == inputs, 'input order changed') + require(set(circuit.outputs) == set(inputs), 'output index set changed') + require(len(circuit.support) == len(circuit.args) <= 41441, 'node bound') + nodes = sorted(circuit.active) + require(len(nodes) == 32216, 'active node count changed') + actual, additions = {}, 0 + for node in nodes: + require(1 <= node < len(circuit.args), 'invalid active node') + pair = circuit.args[node] + if node <= len(inputs): + require(pair is None, 'source has an addition') + value = 1 << (node - 1) + else: + require(isinstance(pair, tuple) and len(pair) == 2, 'invalid addition') + left, right = pair + require(left in actual and right in actual, 'acyclic ancestor missing') + require(not actual[left] & actual[right], 'overlapping integer coefficients') + value = actual[left] | actual[right] + additions += 1 + require(value == circuit.support[node], 'cached support disagrees with literal DAG') + actual[node] = value + require(additions == circuit.additions == 30676, 'addition count changed') + for target in inputs: + expected = sum(1 << index for index, source in enumerate(inputs) + if source & target == 0) + require(actual[circuit.outputs[target]] == expected, 'wrong integer output coefficient') + return {'additions': additions, 'inputs': len(inputs), 'outputs': len(inputs), + 'coefficient_positions': len(inputs) ** 2, + 'nonzero_coefficients': len(inputs) * comb(19, 3)} + + +def check_embedding(circuit, code): + require(code['roles'] == 32216, 'compiled role count changed') + values = [0] * code['roles'] + inputs = triple_masks() + positions = {source: index for index, source in enumerate(inputs)} + require(set(code['sources']) == set(inputs), 'compiled sources missing') + require(set(code['outputs']) == set(inputs), 'compiled outputs missing') + for source, slot in code['sources'].items(): + require(0 <= slot < len(values) and values[slot] == 0, 'source slot collision') + values[slot] = 1 << positions[source] + require(len(code['gates']) == 32216, 'compiled gate bound') + for node, ins, outs in code['gates']: + require(ins and outs and ins[0] == outs[0], 'missing shared pivot') + require(len(set(ins)) == len(ins) and len(set(outs)) == len(outs), 'slot alias') + require(set(ins) & set(outs) == {ins[0]}, 'extra input/output alias') + require(all(0 <= slot < len(values) for slot in ins + outs), 'slot bound') + for slot in ins[1:]: + require(not values[ins[0]] & values[slot], 'embedded coefficients overlap') + values[ins[0]] |= values[slot] + require(values[ins[0]] == circuit.support[node], 'embedded node differs') + for slot in outs[1:]: + require(values[slot] == 0, 'fanout target is not fresh') + values[slot] = values[ins[0]] + for target, slot in code['outputs'].items(): + require(values[slot] == circuit.support[circuit.outputs[target]], 'embedded output differs') + additions = sum(len(ins) + len(outs) - 2 for _, ins, outs in code['gates']) + require(additions == 61352, 'literal disjoint mixer charge changed') + return {'roles': code['roles'], 'gates': len(code['gates']), + 'physical_scalar_additions': additions, + 'all_integer_coefficient_positions_checked': True} + + +def dirty_inverse(code): + original = [(index * 37 % 101) - 50 for index in range(code['roles'])] + values = original.copy() + for _, ins, outs in code['gates']: + values[ins[0]] += sum(values[slot] for slot in ins[1:]) + for slot in outs[1:]: + values[slot] += values[ins[0]] + for _, ins, outs in reversed(code['gates']): + for slot in outs[1:]: + values[slot] -= values[ins[0]] + values[ins[0]] -= sum(values[slot] for slot in ins[1:]) + require(values == original, 'literal integer inverse failed on dirty roles') + return {'dirty_integer_roundtrips': 1, 'dirty_roles': len(values)} + + +def invoice(additions): + h, v, m = 22, comb(22, 3), 22 ** 3 + side = additions + v + comb(h, 2) * (4 * (h - 2) - 6) + mixer = 2 * additions + 2 * comb(h, 2) * (3 * (h - 2) - 6) + accesses = injections = 4 * v + invocation = 4 * mixer + 2 * accesses + 4 * injections + 18 * v + steps = 3 * v * v * invocation + width = 2 * v ** 3 + 2 * v * v * (side + h + 1) + lost = 3 * v * v * h * (h + 1) + rank = width * m - 2 * v ** 3 + 2 * lost + error_budget = 64 * (width + m + 1) ** 3 + require(2 <= rank < m ** 5, 'stopped recurrence rank guard') + require(4 * steps + 8 * rank + 8 * width + 8 * m < error_budget, 'node charge guard') + return {'side_roles': side, 'centres': h + 1, 'mixer_additions': mixer, + 'source_accesses': accesses, 'weighted_injections': injections, + 'signed_invocation_steps': invocation, 'three_stage_steps': steps, + 'W': width, 'm': m, 'L': lost, 's': rank, 'E': error_budget, + 'fixed_deficit': width * m - rank} + + +def rejected(action, message): + try: + action() + except (ValueError, KeyError, IndexError): + return + raise ValueError('control survived: ' + message) + + +def controls(circuit, code): + target = next(iter(circuit.outputs)) + saved = circuit.outputs[target] + try: + circuit.outputs[target] = 1 + rejected(lambda: check_dag(circuit), 'wrong final coefficient') + finally: + circuit.outputs[target] = saved + node = next(node for node in sorted(circuit.active) if circuit.args[node]) + saved_pair, saved_support = circuit.args[node], circuit.support[node] + try: + circuit.args[node] = (saved_pair[0], saved_pair[0]) + rejected(lambda: check_dag(circuit), 'duplicated summand') + circuit.args[node] = (node, saved_pair[1]) + rejected(lambda: check_dag(circuit), 'cycle') + circuit.args[node] = saved_pair + circuit.support[node] ^= 1 + rejected(lambda: check_dag(circuit), 'cached support corruption') + finally: + circuit.args[node], circuit.support[node] = saved_pair, saved_support + saved_roles = code['roles'] + try: + code['roles'] -= 1 + rejected(lambda: check_embedding(circuit, code), 'missing paid role') + finally: + code['roles'] = saved_roles + gate = next(index for index, (_, ins, _) in enumerate(code['gates']) if len(ins) == 2) + saved_gate = code['gates'][gate] + try: + n, ins, outs = saved_gate + code['gates'][gate] = (n, ins, (outs[0], outs[0])) + rejected(lambda: check_embedding(circuit, code), 'fanout alias') + finally: + code['gates'][gate] = saved_gate + return 6 + + +def main(): + started = time.monotonic() + hashes = source_hashes() + sys.path.insert(0, str(PACKAGE)) + from construction import DescendantCircuit + circuit = DescendantCircuit() + dag = check_dag(circuit) + code = circuit.compile() + embedded = check_embedding(circuit, code) + inverse = dirty_inverse(code) + frames = circuit.verify_frames() + require(frames['orientations'] == 2 and frames['all_physical_transitions_checked'], + 'both physical frame orientations required') + count = controls(circuit, code) + # A control restores every mutation before the final successful replay. + check_dag(circuit) + check_embedding(circuit, code) + bill = invoice(dag['additions']) + require(bill['signed_invocation_steps'] == 409880, 'complete scalar bill changed') + require(bill['three_stage_steps'] == 2916214224000, 'complete tensor bill changed') + report = {'claim_type': 'finite certificate', 'no_new_kappa': True, + 'python': platform.python_version(), 'platform': platform.platform(), + 'dag': dag, 'embedding': embedded, 'inverse': inverse, 'frames': frames, + 'invoice': bill, 'rejecting_controls': count, + 'source_sha256': hashes, 'elapsed_seconds': time.monotonic() - started} + print(json.dumps(report, sort_keys=True)) + print('PASS_DISJOINT_DESCENDANT_TRAVERSAL additions=30676 roles=32216 no_new_kappa') + + +if __name__ == '__main__': + main()