From 0d259ac983f9e2b184a3858d09acbb3ca32d35e2 Mon Sep 17 00:00:00 2001 From: Cinna Davis Date: Fri, 23 Oct 2026 00:47:41 -0500 Subject: [PATCH] Derive sharp carried-frame intervals and reject both extremal paid profiles --- .../carried-warp-frame-intervals/PROOF.md | 135 +++++++++ .../carried-warp-frame-intervals/README.md | 126 ++++++++ .../carried-warp-frame-intervals/RESULT.json | 284 ++++++++++++++++++ .../carried-warp-frame-intervals/SOURCES.json | 60 ++++ .../carried-warp-frame-intervals/TASK.json | 98 ++++++ .../carried-warp-frame-intervals/VERIFY.json | 27 ++ .../carried-warp-frame-intervals/frame_dag.py | 256 ++++++++++++++++ .../carried-warp-frame-intervals/replay.py | 107 +++++++ .../carried-warp-frame-intervals/verify.py | 193 ++++++++++++ 9 files changed, 1286 insertions(+) create mode 100644 research/carried-warp-frame-intervals/PROOF.md create mode 100644 research/carried-warp-frame-intervals/README.md create mode 100644 research/carried-warp-frame-intervals/RESULT.json create mode 100644 research/carried-warp-frame-intervals/SOURCES.json create mode 100644 research/carried-warp-frame-intervals/TASK.json create mode 100644 research/carried-warp-frame-intervals/VERIFY.json create mode 100644 research/carried-warp-frame-intervals/frame_dag.py create mode 100644 research/carried-warp-frame-intervals/replay.py create mode 100644 research/carried-warp-frame-intervals/verify.py diff --git a/research/carried-warp-frame-intervals/PROOF.md b/research/carried-warp-frame-intervals/PROOF.md new file mode 100644 index 0000000000..84a1a9213e --- /dev/null +++ b/research/carried-warp-frame-intervals/PROOF.md @@ -0,0 +1,135 @@ +# Sharp marginal frame intervals and the extremal price test + +This is a written proof about the binary frame contract defined below. The +finite exact replays supplement it. No formal proof kernel, physical phase +admission or multiplication theorem is claimed. Prepared by 1337isnot1337 with +substantial OpenAI Codex assistance; Apache-2.0. + +## The graph and the quantified statement + +Let V be F₂^h for any finite positive h. Let D be a finite directed acyclic +multigraph whose vertices are topologically numbered. Each edge e:a→b carries +an invertible linear map G_e:V→V. A specified subset of vertices has prescribed +subspaces F_v. A feasible assignment consists of subspaces U_v≤V such that + + U_v = F_v at each prescribed vertex; + G_e(U_a) ≤ U_b for every edge e:a→b. + +Assume at least one feasible assignment exists. Define L in topological order: + + L_v = F_v at prescribed vertices; + L_v = sum_{e:a→v} G_e(L_a) otherwise. + +The empty sum is the zero subspace. Define H in reverse topological order: + + H_v = F_v at prescribed vertices; + H_v = intersection_{e:v→b} G_e^(-1)(H_b) otherwise. + +The empty intersection is V. Then: + +1. L and H are feasible, and every feasible U satisfies L_v≤U_v≤H_v. +2. For each single vertex v and each subspace S with L_v≤S≤H_v, there + exists a feasible assignment U with U_v=S. It is constructed by adding + the prescription U_v=S and recomputing the lower propagation. + +This is a standard order propagation argument applied to this caller. Choices +at different vertices remain coupled by the edges. The statement concerns +one prescribed marginal at a time, over all subspaces, not a registry search. + +## Proof of the bounds + +Compare against any feasible U. Forward induction gives L_v≤U_v: this is +immediate at prescribed vertices, and a sum of images of contained subspaces +is contained in U_v at an unprescribed vertex. Backward induction gives U_v≤H_v, +using inverse images and intersections. Thus L_v≤H_v. + +For an edge a→b, if b is unprescribed its recurrence contains G_e(L_a). +If b is prescribed, the existence of a feasible U gives +G_e(L_a)≤G_e(U_a)≤F_b=L_b. Hence L is feasible. For H, an unprescribed a +satisfies G_e(H_a)≤H_b by definition. At a prescribed a, use feasibility and +the already established backward bound to get G_e(F_a)≤H_b. Thus H is feasible. +The implementation checks these prescribed-vertex compatibility conditions +explicitly and rejects empty intervals. + +## Proof of complete marginal attainability + +Fix v and S between L_v and H_v. Keep L unchanged before v, prescribe S at v, +and propagate sums of images forward. Incoming edges at v remain valid because +their images are contained in L_v≤S. + +At each later vertex w, the extra contribution from S is the sum of G_path(S) +over paths from v to w whose internal vertices are unprescribed. This follows +inductively because linear isomorphisms preserve sums of subspaces. At the first +prescribed endpoint w on any such path, the reverse recurrence gives +H_v≤G_path^(-1)(F_w). Consequently G_path(S)≤F_w. The original lower contribution +was also contained in F_w, so prescribing F_w causes no conflict. That vertex +resets the downstream contribution to its fixed F_w. This proves compatibility +at every prescribed vertex and constructs the required feasible assignment. + +## Binding the graph to the native word + +The input is the exact frame-carrying program constructed by Dugongue's PR4971 +at head 0130b196145a43a7d305de41f49e56e8e8556378. It retains Cao Yifan's native +round-three source and the credited native/helper lineage. + +Each live field holds a pointer (v,A), meaning that its current frame, before +any next paid climb, is A(U_v). Initially v is its prescribed entrance and A=I. +A weighted whole-field swap exchanges the pointers. A native warp of signed +operator k changes A to G_k A, using the inverse map for negative k. + +A scalar contact between live fields creates one vertex u and an edge +(v,u,A) for each operand. Both pointers then become (u,I). A scalar SCALE +commutes with the frame and creates no constraint. A scalar contact with the +owned cell retains its supplied frame as a prescribed vertex. Every live +terminal frame is prescribed. Owned-center events and all scalar coefficients +are retained. The graph is acyclic because every new contact is later in the +word than the pointers feeding it. + +Every feasible graph assignment has a sufficient chronological realization: +before a contact u, climb each operand from A(U_v) to U_u. The edge constraint +makes this an ascending nested climb. At a warp carry the actual frame by G_k; +at a weighted swap carry it with the exchanged field. Restore each prescribed +terminal frame by its final edge. This realizes exactly the binary contract. + +Conversely, any schedule in this contract with the same scalar contacts, swaps, +warp maps and fixed boundaries defines such a graph assignment. Between two +contacts, invertible maps preserve containment, so any ascending climbs can be +deferred through the intervening warps to the next contact. The composed map +on that edge therefore sends the earlier contact frame into the later one. +This is the precise schedule class to which the sharp bounds apply. + +These statements concern subspaces and normalized linear actions. They do not +prove that every new canonical frame transition has the required physical +absolute phase or uniform implementation. The separate replay checks all +632 independent-input normalized rows, actual G-image warp conditions, frame +chronology, paid ranks and owned-cell clearing for each emitted candidate. + +## Paid rank and the two extremal profiles + +The sum of the dimensions of the 632 live frames changes only at paid climbs. +Swaps permute its terms and the invertible warp maps preserve each dimension. +Consequently every ascending realization with these fixed entrances and exits +has the same total live paid rank. The eight retained rank-eight owned-center +jobs add a fixed 64. The complete source and each realized schedule have total +paid rank 5,327. + +For a paid profile n_r, define C_k(n)=sum_r n_r min(r,k). For any concave rank +price f on {0,...,9} with f(0)=0, put d_j=f(j)-f(j-1). Direct summation gives + + f(r) = r d_9 + sum_{k=1}^8 min(r,k) (d_k-d_(k+1)). + +Every curvature coefficient d_k-d_(k+1) is nonnegative. Equal total rank cancels +the linear term when comparing profiles. Therefore C_k(source)≤C_k(candidate) +for every k implies that the source price is no greater for every such f. +A positive cut difference yields strict inequality for every strictly concave f, +including f(r)=r^t for 0> vector & 1 and not generated >> vector & 1: + result.append(vector) + generated = space(result) + need(generated == subspace, "Not a binary subspace") + return tuple(result) + + +def dimension(subspace): + return subspace.bit_count().bit_length() - 1 + + +@lru_cache(None) +def join(left, right): + if left & right == left: + return right + if left & right == right: + return left + return space(basis(left) + basis(right)) + + +def linear(columns, vector): + result = 0 + for bit, column in enumerate(columns): + if vector >> bit & 1: + result ^= column + return result + + +@lru_cache(None) +def compose(left, right): + return tuple(linear(left, column) for column in right) + + +@lru_cache(None) +def inverse(columns): + size = 1 << len(columns) + need(all(type(x) is int and 0 <= x < size for x in columns), "Binary map range") + values = [linear(columns, x) for x in range(size)] + need(len(set(values)) == size, "Singular binary map") + back = [0] * size + for source, target in enumerate(values): + back[target] = source + return tuple(back[1 << bit] for bit in range(len(columns))) + + +@lru_cache(None) +def image(columns, subspace): + return space(tuple(linear(columns, vector) for vector in basis(subspace))) + + +class FrameDAG: + """Edges (a,b,G) impose G(U_a) <= U_b, with a < b and G invertible.""" + + def __init__(self, h): + need(type(h) is int and 1 <= h <= 9, "Ambient dimension between one and nine") + self.h = h + self.identity = tuple(1 << bit for bit in range(h)) + self.full = (1 << (1 << h)) - 1 + self.fixed = [] + self.parents = [] + self.children = [] + + def node(self, fixed=None): + if fixed is not None: + basis(fixed) + need(fixed & self.full == fixed, "Frame outside ambient space") + index = len(self.fixed) + self.fixed.append(fixed) + self.parents.append([]) + self.children.append([]) + return index + + def edge(self, source, target, columns=None): + columns = self.identity if columns is None else tuple(columns) + need(0 <= source < target < len(self.fixed), "Edges require topological order") + need(len(columns) == self.h, "Map dimension") + inverse(columns) + self.parents[target].append((source, columns)) + self.children[source].append((target, columns)) + + def bounds(self, extra=None): + fixed = self.fixed[:] + for node, subspace in (extra or {}).items(): + need(type(node) is int and 0 <= node < len(fixed), "Unknown pinned node") + basis(subspace) + need(subspace & self.full == subspace, "Pinned frame outside ambient space") + need(fixed[node] is None or fixed[node] == subspace, "Changed fixed node") + fixed[node] = subspace + lower = [] + for node, value in enumerate(fixed): + bound = 1 + for parent, columns in self.parents[node]: + bound = join(bound, image(columns, lower[parent])) + if value is not None: + need(bound & value == bound, "Infeasible lower bound") + bound = value + lower.append(bound) + upper = [None] * len(fixed) + for node in reversed(range(len(fixed))): + bound = self.full + for child, columns in self.children[node]: + bound &= image(inverse(columns), upper[child]) + if fixed[node] is not None: + need(fixed[node] & bound == fixed[node], "Infeasible upper bound") + bound = fixed[node] + need(lower[node] & bound == lower[node], "Empty frame interval") + upper[node] = bound + self.check(lower, fixed) + self.check(upper, fixed) + return lower, upper + + def check(self, values, fixed=None): + fixed = self.fixed if fixed is None else fixed + need(len(values) == len(fixed), "Node inventory") + for node, value in enumerate(values): + basis(value) + need(value & self.full == value, "Node outside ambient space") + need(fixed[node] is None or fixed[node] == value, "Fixed node mismatch") + for parent, columns in self.parents[node]: + moved = image(columns, values[parent]) + need(moved & value == moved, "Mapped containment failed") + + def extend(self, node, subspace): + return self.bounds({node: subspace})[0] + + +class NativeSchedule: + """Remove paid climbs; carry each demand pointer through swaps and warps. + + Owned-cell contacts retain their supplied frames. All main/helper entrances + and exits remain fixed. Scalar coefficients and normalized words stay fixed. + """ + + def __init__(self, canonical, program): + self.canonical = canonical + need(canonical["h"] == 9, "Retained nine-bit caller") + self.spaces = list(map(space, canonical["frames"])) + self.maps = {} + for warp in canonical["warps"]: + op, columns = warp["op"], tuple(warp["G_columns"]) + need(type(op) is int and op > 0 and op not in self.maps, "Warp IDs") + self.maps[op], self.maps[-op] = columns, inverse(columns) + self.program = [deepcopy(event) for event in program if event[0] != "climb"] + graph = self.graph = FrameDAG(9) + self.contacts = {} + values = [] + + def node(label=None): + value = None if label is None else self.spaces[label] + result = graph.node(value) + values.append(value) + return result + + current = [(node(label), graph.identity) for label in canonical["start"]] + for index, event in enumerate(self.program): + if event[0] == "weighted_swap": + left, right = event[1:3] + current[left], current[right] = current[right], current[left] + elif event[0] == "warp": + _, role, op, _, _ = event + need(role[0] == "L" and op in self.maps, "Known live warp") + parent, columns = current[role[1]] + current[role[1]] = parent, compose(self.maps[op], columns) + elif event[0] == "scalar": + gate, label = event[1:] + roles = gate[1:3] if gate[0] in ("add", "copy") else gate[1:2] + live = [role[1] for role in roles if role[0] == "L"] + if not live or gate[0] == "scale": + continue + contact = node(label if len(live) < len(roles) else None) + values[contact] = self.spaces[label] + for role in live: + parent, columns = current[role] + graph.edge(parent, contact, columns) + current[role] = contact, graph.identity + self.contacts[index] = contact + for role, label in enumerate(canonical["final"]): + final = node(label) + parent, columns = current[role] + graph.edge(parent, final, columns) + graph.check(values) + self.original_values = values + + def realize(self, values): + self.graph.check(values) + canonical = deepcopy(self.canonical) + frames = list(self.spaces) + labels = {subspace: label for label, subspace in enumerate(frames)} + current = [frames[label] for label in canonical["start"]] + result = [] + + def label(subspace): + if subspace not in labels: + labels[subspace] = len(frames) + frames.append(subspace) + canonical["frames"].append(list(basis(subspace))) + return labels[subspace] + + def climb(role, target): + old = current[role] + if old != target: + need(old & target == old, "Non-nested realized climb") + result.append(["climb", "carried", role, label(old), label(target), + dimension(target) - dimension(old)]) + current[role] = target + + for index, original in enumerate(self.program): + event = deepcopy(original) + if event[0] == "weighted_swap": + left, right = event[1:3] + event[5] = [label(current[left]), label(current[right])] + current[left], current[right] = current[right], current[left] + event[6] = [label(current[left]), label(current[right])] + elif event[0] == "warp": + role, op = event[1][1], event[2] + old = current[role] + current[role] = image(self.maps[op], old) + event[3:] = [label(old), label(current[role])] + elif event[0] == "scalar": + gate = event[1] + roles = gate[1:3] if gate[0] in ("add", "copy") else gate[1:2] + live = [role[1] for role in roles if role[0] == "L"] + if live: + target = current[live[0]] if gate[0] == "scale" else values[self.contacts[index]] + for role in live: + climb(role, target) + event[2] = label(target) + result.append(event) + for role, final in enumerate(canonical["final"]): + climb(role, frames[final]) + return canonical, result diff --git a/research/carried-warp-frame-intervals/replay.py b/research/carried-warp-frame-intervals/replay.py new file mode 100644 index 0000000000..63537c825d --- /dev/null +++ b/research/carried-warp-frame-intervals/replay.py @@ -0,0 +1,107 @@ +"""Separate exact chronological and free-word replay, Apache-2.0. + +Prepared by 1337isnot1337 with substantial OpenAI Codex assistance. This uses +the retained event meanings but imports none of the retained row primitives. +""" +from collections import Counter +from fractions import Fraction + +from frame_dag import image, inverse, need, space, dimension + + +def replay(canonical, program, backward=False): + frames = list(map(space, canonical["frames"])) + maps = {} + for warp in canonical["warps"]: + columns = tuple(warp["G_columns"]) + maps[warp["op"]], maps[-warp["op"]] = columns, inverse(columns) + rows = [{(role, ()): Fraction(1)} for role in range(632)] + [{}] + current = canonical["start"][:] + [None] + paid = Counter() + + def register(role): + need(role[0] in ("L", "C"), "Known register class") + if role[0] == "C": + need(role[1] == 0, "Only the retained owned C0") + return 632 + need(0 <= role[1] < 632, "Live register range") + return role[1] + + for event in program: + kind = event[0] + if kind == "weighted_swap": + _, left, right, a, b, before, after = event + need(left != right and [current[left], current[right]] == before, "Swap incoming frames") + a, b = Fraction(a), Fraction(b) + need(a and b, "Invertible weighted swap") + rows[left], rows[right] = ({key: a * value for key, value in rows[right].items()}, + {key: b * value for key, value in rows[left].items()}) + current[left], current[right] = current[right], current[left] + need([current[left], current[right]] == after, "Swap carries frames") + elif kind == "warp": + _, role, operator, old, new = event + target = register(role) + need(operator in maps and current[target] == old, "Warp incoming frame") + need(image(maps[operator], frames[old]) == frames[new], "Warp map/frame mismatch") + symbol = (1 if operator > 0 else -1) * (abs(operator) + (1000000 if backward else 0)) + moved = {} + for (variable, word), value in rows[target].items(): + word = word[1:] if word and word[0] == -symbol else (symbol,) + word + key = variable, word + moved[key] = moved.get(key, Fraction(0)) + value + rows[target] = {key: value for key, value in moved.items() if value} + current[target] = new + elif kind in ("climb", "center"): + if kind == "climb": + _, _, target, old, new, rank = event + need(frames[old] & frames[new] == frames[old] and old != new, + "Strict nested climb") + else: + _, target, old, new, rank = event + need(target == 0, "Owned C0 center") + target = 632 + need(frames[old] & frames[new] in (frames[old], frames[new]), "Nested center") + need(current[target] == old, "Paid incoming frame") + need(rank == abs(dimension(frames[new]) - dimension(frames[old])) and rank > 0, + "Paid rank mismatch") + current[target] = new + paid[rank] += 1 + elif kind == "scalar": + gate, frame = event[1:] + target = register(gate[1]) + if gate[0] == "clear": + need(target == 632, "Owned clear only") + rows[target], current[target] = {}, frame + continue + need(current[target] == frame, "Scalar target frame") + if gate[0] in ("add", "copy"): + source = register(gate[2]) + need(current[source] == frame, "Scalar source frame") + if gate[0] == "copy": + need(target == 632, "Owned copy only") + rows[target] = dict(rows[source]) + else: + need(target != source, "Distinct ADD operands") + coefficient = Fraction(gate[3], gate[4]) + for key, value in tuple(rows[source].items()): + value = rows[target].get(key, Fraction(0)) + coefficient * value + if value: + rows[target][key] = value + else: + rows[target].pop(key, None) + else: + need(gate[0] == "scale", "Known scalar opcode") + coefficient = Fraction(gate[2], gate[3]) + need(coefficient, "Invertible SCALE") + rows[target] = {key: coefficient * value for key, value in rows[target].items()} + else: + need(kind in ("phase", "adapter", "residual_adapter"), "Known inert marker") + need(current[:632] == canonical["final"] and not rows[632], "Terminal frames and owned clear") + for role in range(632): + expected = {(role, ()): Fraction(1)} + if backward and role < 112: + expected[role + 112, ()] = Fraction(-1) + if not backward and 112 <= role < 224: + expected[role - 112, ()] = Fraction(1) + need(rows[role] == expected, "Normalized independent-input endpoint") + return paid diff --git a/research/carried-warp-frame-intervals/verify.py b/research/carried-warp-frame-intervals/verify.py new file mode 100644 index 0000000000..5305134b5f --- /dev/null +++ b/research/carried-warp-frame-intervals/verify.py @@ -0,0 +1,193 @@ +#!/usr/bin/env python3 +"""Sharp carried-frame intervals and exact native endpoints; no new kappa. + +Apache-2.0. Prepared by 1337isnot1337 with substantial OpenAI Codex assistance. +Source and predecessor credit are in README.md and the retained source notices. +""" +import argparse +from collections import Counter +from copy import deepcopy +from fractions import Fraction +import hashlib +import json +from pathlib import Path +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +from frame_dag import FrameDAG, NativeSchedule, basis, dimension, image, inverse, join, need, space +from replay import replay + + +def rejected(action, reason): + try: + action() + except ValueError as error: + need(reason in str(error), "Unexpected rejection reason: " + str(error)) + return str(error) + raise ValueError("A rejection control was accepted: " + reason) + + +def source(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + for row in pins["files"]: + if row["usage"] == "input": + need(hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], + "Changed source: " + row["path"]) + code = ("import contextlib,io,json,sys;sys.path.insert(0,sys.argv[1]);" + "capture=io.StringIO();" + "exec('with contextlib.redirect_stdout(capture):\\n import verify as S');" + "p={d:S.construct(w)[0] for d,w in S.a['programs'].items()};" + "print(json.dumps({'canonical':S.c,'programs':p}))") + with tempfile.TemporaryDirectory(prefix="carried-source-cache-") as cache: + run = subprocess.run([sys.executable, "-I", "-B", "-X", "pycache_prefix=" + cache, + "-c", code, str(ROOT / "research/native-frame-carrying-swaps")], + check=True, capture_output=True, text=True, timeout=120) + return json.loads(run.stdout) + + +def toy(): + graph = FrameDAG(3) + initial, left, right, terminal = (graph.node(space([1])), graph.node(), + graph.node(), graph.node(space([1, 2, 4]))) + rotation = (2, 4, 1) + graph.edge(initial, left) + graph.edge(left, right) + graph.edge(left, right, rotation) + graph.edge(right, terminal) + lower, upper = graph.bounds() + all_spaces = {1} + for vector in range(1, 8): + all_spaces |= {join(value, space([vector])) for value in tuple(all_spaces)} + need(len(all_spaces) == 16, "All subspaces of F2^3") + solutions = [] + for a in all_spaces: + for b in all_spaces: + if space([1]) & a == space([1]) and a & b == a and image(rotation, a) & b == image(rotation, a): + values = [space([1]), a, b, space([1, 2, 4])] + graph.check(values) + solutions.append(values) + need(len(solutions) == 6, "Exhaustive toy schedule count") + pins = 0 + for node in (left, right): + actual = {values[node] for values in solutions} + interval = {value for value in all_spaces if value & lower[node] == lower[node] and value & upper[node] == value} + need(actual == interval, "Complete marginal interval, including intermediate subspaces") + for value in interval: + extension = graph.extend(node, value) + graph.check(extension) + need(extension[node] == value, "Pinned extension") + pins += 1 + wrong = lower[:] + wrong[right] = join(wrong[left], image(inverse(rotation), wrong[left])) + controls = { + "wrong_map_direction": rejected(lambda: graph.check(wrong), "Mapped containment failed"), + "coupled_marginal_choices": rejected( + lambda: graph.check([lower[initial], upper[left], lower[right], lower[terminal]]), + "Mapped containment failed"), + "pin_below_lower": rejected(lambda: graph.extend(right, space([1])), "Infeasible lower bound"), + "changed_fixed_node": rejected(lambda: graph.extend(terminal, space([1, 2])), "Changed fixed node"), + "singular_map": rejected(lambda: inverse((1, 1, 4)), "Singular binary map"), + } + return {"subspaces": 16, "assignments_checked": 256, "solutions": len(solutions), + "marginal_pins_extended": pins, "controls": controls} + + +def profile_record(profile): + return {str(rank): count for rank, count in sorted(profile.items())} + + +def cut_differences(candidate, baseline): + return [sum(count * min(rank, cut) for rank, count in candidate.items()) - + sum(count * min(rank, cut) for rank, count in baseline.items()) + for cut in range(1, 10)] + + +def run(): + retained = source() + canonical = retained["canonical"] + result = {"status": "PASS_CARRIED_WARP_FRAME_INTERVALS", "toy": toy(), "directions": {}, + "new_kappa_claimed": False, + "scope": "Sharp marginal intervals for the binary frame contract; exact normalized endpoints; no new physical phase or supplier admission"} + for direction, original in retained["programs"].items(): + backward = direction == "backward" + baseline = replay(canonical, original, backward) + need(baseline == Counter({1: 2201, 2: 412, 3: 510, 4: 127, 5: 40, 8: 8}), "Source paid profile") + schedule = NativeSchedule(canonical, original) + graph = schedule.graph + lower, upper = graph.bounds() + bounds_census = Counter(f"{dimension(a)}-{dimension(b)}" for a, b, fixed in + zip(lower, upper, graph.fixed) if fixed is None) + records = {} + generated = {} + for name, values in (("original_contacts", schedule.original_values), ("least", lower), ("greatest", upper)): + changed, program = schedule.realize(values) + paid = replay(changed, program, backward) + cuts = cut_differences(paid, baseline) + need(sum(rank * count for rank, count in paid.items()) == 5327, "Fixed total paid rank") + if name == "original_contacts": + need(paid == baseline, "Original contact reconstruction") + else: + need(all(value >= 0 for value in cuts) and any(value > 0 for value in cuts), + "Extremal schedule dominated for every strictly concave rank price") + records[name] = {"paid": profile_record(paid), "rank_mass": 5327, + "min_rank_cut_difference": cuts, + "warp_events": sum(e[0] == "warp" for e in program), + "swaps": sum(e[0] == "weighted_swap" for e in program), + "frame_count": len(changed["frames"])} + generated[name] = changed, program + contact = next(node for node in schedule.contacts.values() + if dimension(upper[node]) - dimension(lower[node]) >= 2) + vector = next(vector for vector in basis(upper[contact]) if not lower[contact] >> vector & 1) + intermediate = join(lower[contact], space([vector])) + need(lower[contact] != intermediate != upper[contact], "Strict intermediate source frame") + extension = graph.extend(contact, intermediate) + changed, program = schedule.realize(extension) + pinned_paid = replay(changed, program, backward) + records["intermediate_pin"] = {"node": contact, "lower_dimension": dimension(lower[contact]), + "pinned_dimension": dimension(intermediate), + "upper_dimension": dimension(upper[contact]), + "paid": profile_record(pinned_paid)} + changed, program = generated["least"] + bad = deepcopy(program) + next(event for event in bad if event[0] == "climb")[-1] += 1 + controls = {"wrong_paid_rank": rejected(lambda: replay(changed, bad, backward), "Paid rank mismatch")} + bad_warp = deepcopy(original) + need(bad_warp[3] == ["warp", ["L", 273], -59, 0, 0] and + bad_warp[4] == ["warp", ["L", 273], 59, 0, 0], "Pinned warp counterexample") + bad_warp[3][4], bad_warp[4][3] = 1, 1 + controls["false_warp_frame"] = rejected(lambda: replay(canonical, bad_warp, backward), "Warp map/frame mismatch") + bad_swap = deepcopy(original) + event = next(event for event in bad_swap if event[0] == "weighted_swap" and event[5][0] != event[5][1]) + event[6] = event[5][:] + controls["missing_swap_frame_carry"] = rejected(lambda: replay(canonical, bad_swap, backward), "Swap carries frames") + bad_sign = deepcopy(original) + event = next(event for event in bad_sign if event[0] == "weighted_swap") + event[3] = str(-Fraction(event[3])) + controls["wrong_swap_sign"] = rejected( + lambda: replay(canonical, bad_sign, backward), "Normalized independent-input endpoint") + result["directions"][direction] = {"graph_nodes": len(graph.fixed), + "graph_edges": sum(map(len, graph.parents)), + "contact_nodes": len(schedule.contacts), + "variable_interval_dimensions": dict(sorted(bounds_census.items())), + "schedules": records, "controls": controls} + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true") + args = parser.parse_args() + result = json.loads(json.dumps(run())) + serialized = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.write: + (HERE / "RESULT.json").write_text(serialized) + need(result == json.loads((HERE / "RESULT.json").read_text()), "Deterministic frame interval receipt") + print(serialized, end="") + + +if __name__ == "__main__": + main()