diff --git a/research/bit-simple-graph-obstruction/CONTROL.json b/research/bit-simple-graph-obstruction/CONTROL.json new file mode 100644 index 0000000000..39d1b072cc --- /dev/null +++ b/research/bit-simple-graph-obstruction/CONTROL.json @@ -0,0 +1,147 @@ +{ + "model": "Coordinate rank-four D supports; two early q helper columns; all Q outputs", + "results": [ + { + "name": "two-full-complement-control", + "order": [ + 0, + 1 + ], + "edges": [ + [ + 0, + 1 + ], + [ + 0, + 1 + ], + [ + 0, + 1 + ], + [ + 0, + 1 + ] + ], + "fields": [ + { + "name": "e01", + "vertices": [ + 0, + 1 + ] + }, + { + "name": "e01", + "vertices": [ + 0, + 1 + ] + }, + { + "name": "e01", + "vertices": [ + 0, + 1 + ] + }, + { + "name": "e01", + "vertices": [ + 0, + 1 + ] + } + ], + "supports": [ + [ + 0, + 1, + 2, + 3 + ], + [ + 0, + 1, + 2, + 3 + ] + ], + "calls": 2, + "active_fields": 4, + "private_fields": 0, + "edge_fields": 4, + "status": "sat", + "solver_seconds": 0.002181, + "boolean_code_variables": 16, + "all_active_outputs_have_Q": true, + "formal_group_bits": 2, + "native_full_calls_per_port": 2, + "unused_helpers_per_full": 217, + "paid_profile": { + "1": 2646, + "2": 2684, + "3": 158, + "4": 88, + "5": 204, + "6": 22, + "7": 38 + }, + "target_profile": { + "8": 434, + "15": 444 + }, + "rank_surplus": -126, + "R_rows": [ + [ + 6, + 15, + 13, + 6 + ], + [ + 7, + 13, + 9, + 14 + ] + ], + "native_chains": [ + { + "u": 9, + "w": 12, + "basis": [ + 9, + 12, + 1, + 2 + ], + "early_q_column_updates": [ + 7, + 9 + ] + }, + { + "u": 11, + "w": 15, + "basis": [ + 11, + 15, + 1, + 2 + ], + "early_q_column_updates": [ + 6, + 11 + ] + } + ], + "literal_stage_product_check": "PASS", + "exact_endpoint_check": "PASS", + "all_native_chain_checks": "PASS", + "witness_scope": "Abstract native-call word; fixed cover-route tariff is not certified" + } + ] +} diff --git a/research/bit-simple-graph-obstruction/PROOF.md b/research/bit-simple-graph-obstruction/PROOF.md new file mode 100644 index 0000000000..eeac2a53f8 --- /dev/null +++ b/research/bit-simple-graph-obstruction/PROOF.md @@ -0,0 +1,120 @@ +# A last-call obstruction for a simple support graph + +This is a scoped negative result over F2. It does not give a kappa value or an +obstruction to every BIT controller. + +## Model + +There are finitely many field coordinates and f>0 calls, in order 0 through +f-1. Call i has a coordinate support C_i of size four. Every coordinate lies +in one or two supports. Two distinct supports intersect in at most one +coordinate. Thus shared coordinates form a simple graph; private coordinates +fill the supports to size four. + +Let q squared be zero. For every call i, let D_i be a separate commuting +involution. Its formal group symbol is independent of the other symbols. +Write T_i for the diagonal matrix which applies D_i on C_i and the identity +outside C_i. The call is + + F_i = T_i (I + q R_i). + +Every column of R_i outside C_i is zero. Rows outside C_i are permitted. +There must be u_i,w_i in the span of C_i with + + u_i != 0, R_i u_i = 0, R_i w_i = u_i. + +This is the native main Jordan chain. Complete (u_i,w_i) to a basis of C_i +with two helper directions. Their R_i columns are arbitrary, including +writes outside C_i. This is a relaxation of the two-early-helper caller +interface; the theorem does not require a physical implementation for every +matrix it permits. + +The desired endpoint is diagonal. On coordinate a it is + + (product of D_i for which a is in C_i) (I + t_a q), + +where each t_a is zero or one. Thus D-only targets are permitted. The word +has no additional thin call. A scalar basis change is permitted only when +it can be absorbed into this stated form and the supports remain coordinate +supports. Non-coordinate D projectors are outside this model. + +## Coefficient equation + +Let s_i(a) be the bit vector of earlier calls k> b & 1: + stage[a][b].add(d | 1) + out = [[set() for _ in range(n)] for _ in range(n)] + for a, b, c in itertools.product(range(n), repeat=3): + for left in stage[a][b]: + for right in state[b][c]: + if left & right & 1: + continue + term = left ^ right + if term in out[a][c]: + out[a][c].remove(term) + else: + out[a][c].add(term) + state = out + for a, b in itertools.product(range(n), repeat=2): + d = sum((1 << (i + 1)) for i, support in enumerate(supports) if a in support) + expected = {d, d | 1} if a == b else set() + if state[a][b] != expected: + raise ValueError("The literal native-stage product fails") + + +def make_case(name, edges, order, timeout_ms): + f = len(order) + position = {v: i for i, v in enumerate(order)} + edges = sorted(tuple(sorted(edge)) for edge in edges) + fields = [{"name": f"e{a}{b}", "vertices": [a, b]} for a, b in edges] + for v in order: + degree = sum(v in e for e in edges) + if degree > 4: + raise ValueError("A call has more than four fields") + for j in range(4 - degree): + fields.append({"name": f"a{v}_{j}", "vertices": [v]}) + n = len(fields) + supports = [tuple(j for j, fld in enumerate(fields) if v in fld["vertices"]) + for v in order] + if any(len(s) != 4 for s in supports): + raise ValueError("A call does not have rank four") + memberships = [[int(j in support) for j in range(n)] for support in supports] + prefix = [[sum(memberships[k][j] << k for k in range(i)) for j in range(n)] + for i in range(f)] + false = z3.BoolVal(False) + matrices = [[[false for _ in range(n)] for _ in range(n)] for _ in range(f)] + variables = [] + for b, field in enumerate(fields): + sites = sorted(position[v] for v in field["vertices"]) + if len(sites) == 1: + matrices[sites[0]][b][b] = z3.BoolVal(True) + elif len(sites) == 2: + i, j = sites + for a in range(n): + if prefix[i][a] ^ prefix[i][b] == prefix[j][a] ^ prefix[j][b]: + v = z3.Bool(f"x_{b}_{a}") + variables.append(v) + matrices[i][a][b] = v + matrices[j][a][b] = z3.Not(v) if a == b else v + else: + raise ValueError("Only one-call and two-call fields are in this model") + solver = z3.Solver() + solver.set(timeout=timeout_ms) + chain_vars = [] + for i, support in enumerate(supports): + u = [z3.Bool(f"u_{i}_{j}") for j in range(4)] + w = [z3.Bool(f"w_{i}_{j}") for j in range(4)] + solver.add(z3.Or(*u)) + local_rows = [[matrices[i][a][b] for b in support] for a in range(n)] + ru = matrix_vector(local_rows, u) + rw = matrix_vector(local_rows, w) + for a in range(n): + solver.add(z3.Not(ru[a])) + solver.add(rw[a] == (u[support.index(a)] if a in support else false)) + chain_vars.append((u, w)) + started = time.monotonic() + status = solver.check() + elapsed = time.monotonic() - started + result = {"name": name, "order": order, "edges": edges, "fields": fields, + "supports": supports, "calls": f, "active_fields": n, + "private_fields": sum(len(x["vertices"]) == 1 for x in fields), + "edge_fields": len(edges), "status": str(status), + "solver_seconds": round(elapsed, 6), "boolean_code_variables": len(variables), + "all_active_outputs_have_Q": True, + "formal_group_bits": f, "native_full_calls_per_port": f, + "unused_helpers_per_full": 217, + "paid_profile": {"1": 1323*f, "2": 1342*f, "3": 79*f, + "4": 44*f, "5": 102*f, "6": 11*f, "7": 19*f}, + "target_profile": {"8": 217*f + 111*sum(len(x["vertices"]) == 1 for x in fields), + "15": 111*len(edges)}, + "rank_surplus": 217*f*8 +111*(4*f*7+n)-5129*f} + if status == z3.unknown: + result["reason_unknown"] = solver.reason_unknown() + if status != z3.sat: + return result + model = solver.model() + evaluate = lambda v: z3.is_true(model.eval(v, model_completion=True)) + rows = [[sum(evaluate(v) << b for b, v in enumerate(row)) for row in mat] + for mat in matrices] + chains = [] + for i, ((u, w), support) in enumerate(zip(chain_vars, supports)): + ub = sum(evaluate(v) << support[j] for j, v in enumerate(u)) + wb = sum(evaluate(v) << support[j] for j, v in enumerate(w)) + if ub == 0 or apply(rows[i], ub) or apply(rows[i], wb) != ub: + raise ValueError("The model has a bad native main chain") + basis = [ub, wb] + for b in support: + if rank(basis + [1 << b]) > len(basis): + basis.append(1 << b) + if len(basis) != 4: + raise ValueError("The main chain has no basis completion") + # The first two columns are the native main chain. The last two are + # early helper columns. The early q update changes only those columns. + early_columns = [apply(rows[i], basis[j]) ^ basis[j] for j in (2, 3)] + chains.append({"u": ub, "w": wb, "basis": basis, + "early_q_column_updates": early_columns}) + for a, b in itertools.product(range(n), repeat=2): + coeffs = {} + for i in range(f): + if rows[i][a] >> b & 1: + signature = prefix[i][a] ^ prefix[i][b] + coeffs[signature] = coeffs.get(signature, 0) ^ 1 + coeffs = {key: value for key, value in coeffs.items() if value} + if coeffs != ({0: 1} if a == b else {}): + raise ValueError("The model fails the exact formal endpoint") + literal_product_check(rows, supports) + result.update({"R_rows": rows, "native_chains": chains, + "literal_stage_product_check": "PASS", + "exact_endpoint_check": "PASS", + "all_native_chain_checks": "PASS", + "witness_scope": "Abstract native-call word; fixed cover-route tariff is not certified"}) + return result + + +def distinct_orders(edges, count): + # These orders are all supplied to the solver. The receipt has no + # isomorphism claim about a skipped order. + return itertools.permutations(range(count)) + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--out", type=Path, required=True) + parser.add_argument("--timeout-ms", type=int, default=30000) + parser.add_argument("--all-orders", action="store_true") + parser.add_argument("--suite", choices=("simple", "parallel", "control"), default="simple") + args = parser.parse_args() + k4 = list(itertools.combinations(range(4), 2)) + suites = { + "simple": [("K4-minus-01", [e for e in k4 if e != (0, 1)], 4), ("K4", k4, 4)], + "parallel": [ + ("two-full-double-edge", [(0, 1)]*2, 2), + ("three-full-double-path", [(0, 1)]*2 + [(1, 2)]*2, 3), + ("four-full-double-single-double", [(0, 1)]*2 + [(1, 2)] + [(2, 3)]*2, 4), + ], + "control": [("two-full-complement-control", [(0, 1)]*4, 2)], + } + results = [] + for name, edges, count in suites[args.suite]: + orders = distinct_orders(edges, count) if args.all_orders else [tuple(range(count))] + for order in orders: + result = make_case(name, edges, list(order), args.timeout_ms) + results.append(result) + print(json.dumps({k: result[k] for k in ("name", "order", "status", "solver_seconds", "rank_surplus")}), flush=True) + args.out.write_text(json.dumps({"model": "Coordinate rank-four D supports; two early q helper columns; all Q outputs", + "results": results}, indent=2) + "\n") + if result["status"] == "sat": + break + + +if __name__ == "__main__": + main() diff --git a/research/bit-simple-graph-obstruction/verify.py b/research/bit-simple-graph-obstruction/verify.py new file mode 100644 index 0000000000..caa39ab53c --- /dev/null +++ b/research/bit-simple-graph-obstruction/verify.py @@ -0,0 +1,205 @@ +#!/usr/bin/env python3 +"""Check the simple-graph theorem fixtures and an exact positive control.""" +import argparse +from copy import deepcopy +from hashlib import sha256 +import itertools +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def apply(rows, vector): + return sum(((row & vector).bit_count() & 1) << a for a, row in enumerate(rows)) + + +def rank(vectors): + pivots = {} + for vector in vectors: + while vector: + bit = vector.bit_length() - 1 + if bit in pivots: + vector ^= pivots[bit] + else: + pivots[bit] = vector + break + return len(pivots) + + +def supports(edges, order): + fields = [tuple(edge) for edge in edges] + for vertex in order: + fields += [(vertex,)] * (4 - sum(vertex in edge for edge in edges)) + return [tuple(j for j, field in enumerate(fields) if vertex in field) for vertex in order] + + +def prefix_labels(supports_, n): + return [[sum((1 << k) for k in range(i) if a in supports_[k]) for a in range(n)] + for i in range(len(supports_))] + + +def simple_last_diagonal(supports_): + need(all(len(s) == 4 for s in supports_), 'Each support must have rank four') + need(all(len(set(a) & set(b)) <= 1 for a, b in itertools.combinations(supports_, 2)), + 'The simple-graph support hypothesis fails') + n = max(max(s) for s in supports_) + 1 + need(all(sum(a in s for s in supports_) <= 2 for a in range(n)), + 'A coordinate has more than two owners') + prefix = prefix_labels(supports_, n) + last = len(supports_) - 1 + checked = 0 + for a, b in itertools.permutations(supports_[last], 2): + earlier = [i for i in range(last) if b in supports_[i]] + if earlier: + i = earlier[0] + need(prefix[i][a] ^ prefix[i][b] != prefix[last][a] ^ prefix[last][b], + 'An off-diagonal last coefficient can cancel') + checked += 1 + return checked + + +def check_chains(case): + n = case['active_fields'] + rows = case['R_rows'] + need(len(rows) == len(case['supports']) == len(case['native_chains']), 'Stage counts differ') + for matrix, support, chain in zip(rows, case['supports'], case['native_chains']): + mask = sum(1 << a for a in support) + need(len(support) == 4 and len(matrix) == n, 'The native call shape differs') + need(all(row & ~mask == 0 for row in matrix), 'A column lies outside its native support') + u, w, basis = chain['u'], chain['w'], chain['basis'] + need(u != 0 and not (u | w) & ~mask, 'The native main chain has a bad support') + need(apply(matrix, u) == 0 and apply(matrix, w) == u, 'The native main chain fails') + need(basis[:2] == [u, w] and len(basis) == rank(basis) == 4, + 'The native roles do not form an independent basis') + need(all(not vector & ~mask for vector in basis), 'A role lies outside its native support') + need([apply(matrix, z) ^ z for z in basis[2:]] == chain['early_q_column_updates'], + 'The early helper-column update differs') + + +def literal_product(case, flags=None): + n = case['active_fields'] + flags = [1] * n if flags is None else flags + state = [[{0} if a == b else set() for b in range(n)] for a in range(n)] + for i, (rows, support) in enumerate(zip(case['R_rows'], case['supports'])): + stage = [[set() for _ in range(n)] for _ in range(n)] + for a in range(n): + d = (1 << (i + 1)) if a in support else 0 + stage[a][a].add(d) + for b in range(n): + if rows[a] >> b & 1: + stage[a][b].add(d | 1) + out = [[set() for _ in range(n)] for _ in range(n)] + for a, b, c in itertools.product(range(n), repeat=3): + for left in stage[a][b]: + for right in state[b][c]: + if left & right & 1: + continue + term = left ^ right + if term in out[a][c]: + out[a][c].remove(term) + else: + out[a][c].add(term) + state = out + for a, b in itertools.product(range(n), repeat=2): + d = sum(1 << (i + 1) for i, support in enumerate(case['supports']) if a in support) + expected = ({d, d | 1} if flags[a] else {d}) if a == b else set() + need(state[a][b] == expected, 'The literal stage product has a wrong endpoint') + return state + + +def rejected(name, operation): + try: + operation() + except ValueError as error: + return {'name': name, 'result': 'REJECT', 'reason': str(error)} + raise ValueError('A negative control passed: ' + name) + + +def run(): + k4 = list(itertools.combinations(range(4), 2)) + fixture_count = 0 + coefficient_count = 0 + for edges in (k4, [e for e in k4 if e != (0, 1)]): + for order in itertools.permutations(range(4)): + coefficient_count += simple_last_diagonal(supports(edges, order)) + fixture_count += 1 + diagonal_cases = 0 + for mask in range(16): + matrix = [(1 << i) if mask >> i & 1 else 0 for i in range(4)] + for u, w in itertools.product(range(1, 16), range(16)): + need(apply(matrix, u) != 0 or apply(matrix, w) != u, + 'A diagonal matrix contains a nonzero main Jordan chain') + diagonal_cases += 1 + control = json.loads((PACKAGE / 'CONTROL.json').read_text())['results'][0] + check_chains(control) + literal_product(control) + rows = control['R_rows'] + need([a ^ b for a, b in zip(*rows)] == [1 << i for i in range(4)], + 'The two q coefficients do not sum to the identity') + paid = {int(r): n for r, n in control['paid_profile'].items()} + targets = {int(r): n for r, n in control['target_profile'].items()} + need(paid == {1:2646, 2:2684, 3:158, 4:88, 5:204, 6:22, 7:38}, + 'The declared two-FULL invoice differs') + need(targets == {8:434, 15:444}, 'The complete target debit differs') + surplus = sum(r*n for r, n in targets.items()) - sum(r*n for r, n in paid.items()) + need(surplus == -126 and max(paid) < min(targets), 'The positive control price gate differs') + bad_word = deepcopy(control) + bad_word['R_rows'][0][0] ^= 1 + bad_chain = deepcopy(control) + bad_chain['native_chains'][0]['u'] = 0 + controls = [ + rejected('changed_q_coefficient', lambda: literal_product(bad_word)), + rejected('missing_target_Q', lambda: literal_product(control, [0,1,1,1])), + rejected('zero_main_chain', lambda: check_chains(bad_chain)), + rejected('parallel_edges_outside_simple_graph', lambda: simple_last_diagonal(control['supports'])), + ] + evidence = json.loads((PACKAGE / 'solver-evidence/MANIFEST.json').read_text()) + totals = {} + for name, row in evidence['files'].items(): + raw = (PACKAGE / 'solver-evidence' / name).read_bytes() + need(sha256(raw).hexdigest() == row['sha256'], 'A frozen solver receipt changed') + cases = json.loads(raw)['results'] + need(len(cases) == row['cases'] and all(c['status'] == 'unsat' for c in cases), + 'The recorded solver outcomes differ') + for case in cases: + expected = supports(case['edges'], case['order']) + need([list(s) for s in expected] == case['supports'], 'A recorded support differs') + totals[name] = len(cases) + need(sum(totals.values()) == 80, 'The recorded solver case count differs') + return { + 'schema_version': 1, + 'status': 'PASS_BIT_SIMPLE_GRAPH_OBSTRUCTION', + 'simple_graph_order_fixtures': fixture_count, + 'last_off_diagonal_coefficients_checked': coefficient_count, + 'diagonal_chain_cases': diagonal_cases, + 'positive_control': {'literal_stage_product':'PASS', 'native_chains':'PASS', + 'early_helper_columns':'PASS', 'rank_surplus':surplus}, + 'negative_controls': controls, + 'solver_evidence': {'recorded_cases':totals, 'integrity':'PASS', + 'unsat_reproved':False, 'solver_run':False, + 'scope':'The frozen statuses depend on the recorded Z3 solver. The standard-library checks do not prove those UNSAT claims.'}, + 'new_kappa': False, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--output', type=Path) + args = parser.parse_args() + result = json.loads(json.dumps(run())) + expected = PACKAGE / 'RESULT.json' + if expected.exists() and json.loads(expected.read_text()) != result: + raise ValueError('The exact retained result differs') + if args.output: + args.output.write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + print('PASS_BIT_SIMPLE_GRAPH_OBSTRUCTION fixtures=48 diagonal_cases=3840 control=PASS solver_run=false new_kappa=false') + + +if __name__ == '__main__': + main()