diff --git a/research/center-chart-bound/PROOF.md b/research/center-chart-bound/PROOF.md new file mode 100644 index 0000000000..4c52f48fc7 --- /dev/null +++ b/research/center-chart-bound/PROOF.md @@ -0,0 +1,116 @@ +# Every retained center still costs rank eight + +Prepared by Cinna Davis with substantial OpenAI Codex assistance. Apache-2.0. + +## Exact model + +Work in the nine-dimensional binary chart space of Cao Yifan's PR4610 word. +Keep the scalar order, coefficients, field references, logical warp maps, +main endpoints and explicit adapter boundaries. Each scalar operation must +still use a common chart on its operands. Persistent transports keep their +original ascending orientation; zero-length positions may acquire an +ascending transport. A logical warp G remains monomial and maps its entire +new input space to its new output space. All helper boundaries are free. + +Keep the owned center protocol: clear/copy or gather, one complete Gaussian +center call at the retained position, scatter or copy back, then erase. +There is no added center transport between its scalar contacts. Thus its +live chart between these contacts is common. Its zero reset has no chart +constraint until its first nonzero use. Both center endpoint charts may +change. No source center chart is fixed by hand. + +All charts can be arbitrary subspaces of F_2^9. They need not be one-axis +edits, superspaces or subspaces of the submitted charts. This is not a +search over 511 directions or a local optimum statement. Descending +persistent moves, additional center calls, new scalar circuits, changed +logical maps or boundary contracts, enlarged ambient spaces and maps +between digit columns are outside the model. + +## Inclusion graph + +Give every chart boundary and scalar contact a node n with unknown +subspace V_n. A main endpoint or explicit adapter has its original fixed +space. Other nodes, including every helper endpoint and every center +contact, are unconstrained initially. + +An ascending persistent transport from a to b imposes V_a subset V_b. +The two endpoints of a center call are initially unrelated: the closure +adds **no inclusion arc for that call**. This deliberately relaxes its +implementation contract. A common scalar contact shares one node. Persistent arrival at that contact +imposes inclusion, permitting a newly paid ascending step. Nonzero owned +center state has no intervening transport, so its consecutive contact +nodes are equal. A cleared zero state imposes no previous chart relation. + +A logical warp imposes G V_a = V_b. Encode this with both directed +inclusions G V_a subset V_b and G^-1 V_b subset V_a. Warps are not frozen +to their old charts. Every constraint is of the form + + A V_a subset V_b, + +where A is an invertible binary map or the identity. The original word +is checked as a feasible assignment of the whole graph, including all +scalar contacts, all warp maps and both complete paid profiles. + +## Universal lower and upper spaces + +Initialize lower spaces L_n to {0}, except that a fixed node has its +fixed space. For each arc A V_a subset V_b, repeatedly replace + + L_b <- span(L_b union A L_a). + +For every feasible assignment, induction gives L_n subset V_n. Each +replacement is a necessary consequence of one actual inclusion. The +process terminates: every strict replacement raises one finite binary +subspace dimension. At a fixed point the lower assignment itself obeys +all graph inclusions and fixed spaces, so it is the least assignment. +The verifier uses actual XOR span; set union alone would be incorrect. + +Initialize upper spaces U_n to F_2^9, except at fixed nodes. Repeatedly +apply the reverse implication + + U_a <- U_a intersection A^-1 U_b. + +For every feasible assignment V_n subset U_n, again by induction. Each +strict update decreases dimension. Its fixed point is the greatest +assignment. Neither calculation assumes that different chart choices are +independent. Equalities, scalar sharing and warp maps propagate globally. +Original feasibility guarantees that no propagated bound contradicts a +fixed boundary. The implementation checks every final inclusion as well +as containment of the submitted assignment inside the interval. + +## Result on the actual centers + +For both the forward and backward word, each of the eight center calls +has its originally lower/higher endpoints lo,hi satisfying + + U_lo = {0}, dim(L_hi) = 8. + +Thus **every** feasible reassignment has V_lo={0} and dim(V_hi)>=8. +The nesting and direction for the center follow from the bound, although +neither was imposed on its unknown endpoint spaces in the closure. +Its Gaussian rank is at least eight, and the eight calls together retain +at least 64 units of paid rank mass. For 0 0 and size & (size - 1) == 0, 'power-of-two subspace size') + return size.bit_length() - 1 + + +def mv(columns, x): + out = 0 + for i, v in enumerate(columns): + if x >> i & 1: + out ^= v + return out + + +def invert(columns): + table = {mv(columns, x): x for x in range(512)} + need(len(table) == 512, 'invertible logical warp') + return [table[1 << i] for i in range(9)] + + +def join(x, y): + if x & y == x: + return y + if x & y == y: + return x + out, todo = y, x + while todo: + bit = todo & -todo + todo -= bit + v = bit.bit_length() - 1 + if not out >> v & 1: + old = out + while old: + z = old & -old + old -= z + out |= 1 << (v ^ (z.bit_length() - 1)) + return out + + +def build(c, word): + spaces = list(map(space, c['frames'])) + nodes, fixed, arcs, centers = [], set(), [], [] + current, zero = {}, True + paid = Counter() + + def node(f, freeze=False): + n = len(nodes) + nodes.append(spaces[f]) + if freeze: + fixed.add(n) + return n + + def inclusion(a, b, tag=0): + arcs.append((a, b, tag)) + + for r, f in enumerate(c['start']): + current['L', r] = node(f, r < 224) + for e in word: + kind = e[0] + if kind in ('climb', 'center'): + if kind == 'climb': + _, _, r, a, b, width = e + role = ('L', r) + need(spaces[a] & spaces[b] == spaces[a], 'ascending persistent transport') + else: + _, r, a, b, width = e + role = ('C', r) + old = current[role] + need(nodes[old] == spaces[a], 'paid input chart') + need(width > 0 and width == abs(dim(spaces[a]) - dim(spaces[b])), 'paid width') + new = node(b) + low, high = (old, new) if dim(spaces[a]) < dim(spaces[b]) else (new, old) + need(nodes[low] & nodes[high] == nodes[low], 'nested center/paid spaces') + if kind == 'center': + centers.append((low, high)) + else: + inclusion(low, high) + paid[width] += 1 + current[role] = new + elif kind == 'warp': + _, reg, op, a, b = e + role = tuple(reg) + old = current[role] + need(nodes[old] == spaces[a], 'logical warp input chart') + new = node(b) + inclusion(old, new, op) + inclusion(new, old, -op) + current[role] = new + elif kind == 'adapter': + fixed.add(current['L', e[2]]) + elif kind == 'scalar': + g, f = e[1:] + role, contact = tuple(g[1]), node(f) + if g[0] == 'clear': + need(role == ('C', 0), 'only owned scratch cleared') + current[role], zero = contact, True + continue + need(g[0] in ('add', 'copy', 'scale'), 'known scalar operation') + refs = g[1:3] if g[0] in ('add', 'copy') else g[1:2] + for typ, r in refs: + old = current[typ, r] + need(nodes[old] == spaces[f], 'original common scalar chart') + if typ == 'L': + inclusion(old, contact) + elif not zero: + # The retained owned protocol has no call between these contacts. + inclusion(old, contact) + inclusion(contact, old) + current[typ, r] = contact + if any(typ == 'C' for typ, _ in refs): + zero = False + else: + need(kind == 'phase', 'known inert marker') + for r, f in enumerate(c['final']): + old = current['L', r] + need(nodes[old] == spaces[f], 'original final chart') + inclusion(old, node(f, r < 224)) + need(paid == {1:2201, 2:412, 3:510, 4:127, 5:40, 8:8}, 'entire paid source profile') + need(len(centers) == 8, 'eight complete center calls') + return nodes, fixed, arcs, centers + + +def solve(c, word, reverse_queue=False): + nodes, fixed, arcs, centers = build(c, word) + maps = {w['op']: w['G_columns'] for w in c['warps']} + maps.update({-op: invert(cols) for op, cols in list(maps.items())}) + permutations = {op: [mv(cols, x) for x in range(512)] for op, cols in maps.items()} + cache = {} + + def image(bits, tag): + if not tag or bits in (1, FULL): + return bits + key = bits, tag + if key not in cache: + out, todo = 0, bits + while todo: + z = todo & -todo + todo -= z + out |= 1 << permutations[tag][z.bit_length() - 1] + cache[key] = out + return cache[key] + + successors, predecessors = [[] for _ in nodes], [[] for _ in nodes] + for a, b, tag in arcs: + need(image(nodes[a], tag) & nodes[b] == image(nodes[a], tag), 'original graph feasibility') + successors[a].append((b, tag)) + predecessors[b].append((a, -tag)) + reports = {} + for lower in (True, False): + bounds = [1 if lower else FULL for _ in nodes] + q = deque(sorted(fixed)) + for i in q: + bounds[i] = nodes[i] + adjacency = successors if lower else predecessors + while q: + a = q.pop() if reverse_queue else q.popleft() + for b, tag in adjacency[a]: + moved = image(bounds[a], tag) + value = join(bounds[b], moved) if lower else bounds[b] & moved + if value != bounds[b]: + bounds[b] = value + q.append(b) + need(all(bounds[i] == nodes[i] for i in fixed), 'fixed physical interfaces preserved') + for i, old in enumerate(nodes): + need(bounds[i] & old == (bounds[i] if lower else old), 'source lies inside certified interval') + for a, b, tag in arcs: + need(image(bounds[a], tag) & bounds[b] == image(bounds[a], tag), 'fixed-point arc closure') + reports['lower' if lower else 'upper'] = [[dim(bounds[a]), dim(bounds[b])] for a, b in centers] + need(all(pair == [0, 8] for pair in reports['lower']), 'every center high contains eight forced axes') + need(all(pair[0] == 0 for pair in reports['upper']), 'every center low is forced zero') + return {'nodes':len(nodes), 'fixed_nodes':len(fixed), 'inclusion_arcs':len(arcs), + 'center_bounds_low_high':reports, 'unavoidable_center_rank_mass':64} + + +def main(): + raw = (HERE/'inputs/round3-native.json.gz').read_bytes() + pins = json.loads((HERE/'SOURCES.json').read_text()) + pin = next(x for x in pins['files'] if x['path'].endswith('round3-native.json.gz')) + need(hashlib.sha256(raw).hexdigest() == pin['sha256'], 'original PR4610 bytes') + payload = json.loads(gzip.decompress(raw)) + need(set(payload['programs']) == {'forward', 'backward'}, 'both source orientations') + c = payload['canonical'] + need(len(c['start']) == len(c['final']) == 632, 'all persistent fields') + result = {d:solve(c, w) for d, w in sorted(payload['programs'].items())} + for d, w in payload['programs'].items(): + need(solve(c, w, True) == result[d], 'opposite fixed-point worklist order') + changed = deepcopy(c) + for basis in changed['frames']: + if len(basis) >= 2: + basis[0] ^= basis[1] + need(solve(changed, payload['programs']['forward']) == result['forward'], 'all frame basis changes') + need(dim(join(space([1]), space([2]))) == 2 and join(space([1]), space([2])) == space([1,2]), + 'join is XOR span, not set union') + rejected = [] + for label in ('center_width', 'warp_chart', 'dependent_frame_basis'): + bad = deepcopy(payload) + word = bad['programs']['forward'] + if label == 'center_width': + next(e for e in word if e[0] == 'center')[4] -= 1 + elif label == 'warp_chart': + next(e for e in word if e[0] == 'warp' and bad['canonical']['frames'][e[3]])[4] = 0 + else: + basis = next(b for b in bad['canonical']['frames'] if len(b) >= 2) + basis[0] = basis[1] + try: + solve(bad['canonical'], word) + except (ValueError, KeyError): + rejected.append(label) + else: + raise ValueError('source mutation accepted: '+label) + result['controls'] = {'source_mutations_rejected':rejected, + 'opposite_worklist_order':True, 'all_frame_basis_changes':True, + 'xor_span_join':True} + path = HERE/'RESULT.json' + if '--write' in sys.argv: + path.write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') + else: + need(result == json.loads(path.read_text()), 'committed center interval equality') + print('PASS_CENTER_CHART_BOUND: both orientations; every retained center has rank >=8; no new kappa') + + +if __name__ == '__main__': + main()