ruleset "c2lr"
title "C2LR swap-or-stay"
about "This website's machine on a C2LR lattice: every rule of the standard set, and C1-C10. A swap-or-stay step's routes are the machine's matching, so the junction, rail, passing and one-waveform rules (R2, R3, R5, R22) do not judge its crossings; R4 still asks for its class. Both pairings are allowed: one diagonal at every junction (demonstrated) and the two-pair checkerboard steps (assumed, and marked so in every report)."

param max_chain = 15
param c2lr_forms = {"diagonal", "checkerboard"}

rule C1 "A leg holds one crystal, or two between an enter and its exit"
  about "A leg holds one crystal. It holds two only after a swap-or-stay step moved a crystal toward a junction into a partner leg whose crystal stayed (an enter), and until that crystal leaves again by the same step type it entered by (its exit): the crystal that entered is the one that leaves, and no other step type takes it out."
  source "arXiv:2403.00756"
  when c2lr_device():
  (for all s in legs, t in instants: occupancy(s, t) <= 1 or entered(s, t))
  and (for all k in steps: exits_as_entered(k))

rule C2 "A C2LR step's only per-leg choice is its direction bit"
  about "Every crystal shifts toward its pair's junction or away from it, and that is all a step chooses per leg: the step names the crystals shifted toward and nothing else, and its routes are the machine's matching. A step of a C2LR class that writes its own routes is refused."
  source "arXiv:2403.00756"
  when c2lr_device():
  for all k in steps where is_transport(k): bits_only(k)

rule C3 "Horizontal and vertical legs choose independently"
  about "In one step a crystal on a horizontal leg and one on a vertical leg set their direction bits independently: the step carries one bit per crystal and nothing per axis."
  source "arXiv:2403.00756"
  when c2lr_device():
  for all k in steps where exchange(k): independent_axes(k)

rule C4 "A step is C2LR, one shared waveform, C2LR back"
  about "Every crystal shifts by its bit, one junction waveform shared by every junction exchanges the two wells nearest each junction in play, and the shift is undone: one waveform, whose time is the step's however many crystals move."
  source "arXiv:2403.00756"
  when c2lr_device():
  for all k in steps where exchange(k): one_waveform(k)

rule C5 "Every crystal ends a step at a leg centre"
  about "After every step each crystal rests at the centre of a leg; a C2LR machine has nowhere else to hold one."
  source "arXiv:2403.00756"
  when c2lr_device():
  for all i in ions, t in instants where position(i, t) != none:
    position(i, t) in legs

rule C6 "A step pairs legs by the machine's matching"
  about "A swap-or-stay step pairs every leg with at most one other, at one junction, by one variation of the machine: one diagonal at every junction (W-S, W-N, E-S or E-N, all four demonstrated), or two pairs at the junctions of one checkerboard colour (the proposal's, not demonstrated, so assumed). A crystal shifted toward a junction has a partner leg there, the machine offers the variation, and the rule set allows its form (c2lr_forms)."
  source "arXiv:2403.00756"
  when c2lr_device():
  for all k in steps where exchange(k): matched(k) and form(k) in c2lr_forms

rule C7 "No crystal ends a step in a junction"
  about "A crystal crosses a junction inside a step and never rests on one: where three or more rails meet, nothing is left standing when a step ends."
  source "arXiv:2403.00756"
  when c2lr_device():
  for all i in ions, t in instants: position(i, t) not in junctions

rule C8 "The trap frequency is held during a shift"
  about "The C2LR shift moves a crystal by a sixth of the leg while holding its centre-of-mass frequency (1.85 MHz for Ba-Sr, 1.4 MHz for Yb-Ba). It is a property of the step's waveform, recorded with its primitive rather than decided from a programme."
  source "arXiv:2403.00756"
  when c2lr_device():
  com_frequency_held()

rule C9 "Every crystal is heated by every waveform"
  about "The shared waveforms play on every leg, so a step heats every crystal on the machine: one that moved by the step's swap heat, every other by its stay heat. A crystal that sat a step out is not cold."
  source "arXiv:2403.00756"
  when c2lr_device() and models_heating():
  for all k in steps where c2lr_step(k): heats_every_crystal(k)

rule C10 "Control is shared signals plus one input and one switch per leg"
  about "A C2LR machine is driven by a fixed set of shared analog signals (27 in the paper), plus one digital input and one switch per leg: its document says so, and its drawing is the lattice of legs they drive."
  source "arXiv:2403.00756"
  when control() = "c2lr":
  c2lr_wiring()

rule R0 "Every operation finds its ions where it says they are" core
  about "Each operation names its ions and where they are; replaying the execution from the start must find them there, and every ion must end it standing in a site."
  setup_ok()
  and (for all o in operations: well_formed(o) and found(o))
  and (for all i in ions: position(i, final()) != none)

rule R1 "A site holds at most its capacity" core
  about "An ion standing in a site, or passing through it, takes one of its places."
  source "deck_v3; arXiv:2004.04706; arXiv:2511.15910"
  for all s in sites, t in instants:
    occupancy(s, t) <= capacity(s)

rule R2 "A junction holds one ion at a time"
  about "Where three or more rails meet, only one ion may be at any moment, resting or passing through. An ion here is a qubit ion with the coolant ion that shares its well: a qubit-coolant pair crosses a junction as one crystal, as the Ba-Yb pair does through an X-junction. Two qubit ions in one junction at once is what the rule refuses -- except during a swap-or-stay exchange on a C2LR machine, where the shared junction waveform exchanges the two wells nearest it by design, and the routes are the machine's own matching, never the programme's."
  source "deck_v3; arXiv:2510.23519; arXiv:2206.11888; arXiv:2403.00756"
  for all j in junctions, t in instants where not exchange(t):
    occupancy(j, t) <= 1

rule R3 "A rail carries at most its capacity"
  about "No more ions travel along one rail at once than the rail is built for (one, on most machines). A swap-or-stay exchange on a C2LR machine carries its two crystals along the junction's two rails by design, and is not judged here."
  source "deck_v3; arXiv:2510.23519"
  for all r in rails, t in instants where not exchange(t):
    occupancy(r, t) <= capacity(r)

rule R4 "Every transport step uses a movement the machine declares"
  about "A step's motion is one of the movement classes the machine's control system is built to produce."
  source "deck_v3; arXiv:2504.17886"
  for all k in steps where is_transport(k): class_declared(k)

rule R4b "A step either moves ions or gates them, never both"
  about "Moving ions within traps and between them use different control pathways, and neither runs alongside gates."
  source "arXiv:2504.17886"
  for all k in steps where is_transport(k):
    mode(k) in {"intra", "inter"} and not carries_gates(k)

rule R4d "The control channels can drive every transport step"
  about "One channel carries one waveform: every ion a channel moves must move the same way, and a site may sit a step out only if it has its own switch."
  source "deck_v3; arXiv:2403.00756; arXiv:2305.03828"
  for all k in steps where is_transport(k): drivable(k)

rule R5 "No two ions pass each other on a rail in one step"
  about "Within one step, two ions may not travel the same rail in opposite directions, one from each end: an ion rides the rail's RF null, a single line, so the two would have to pass through each other. Exchanging two ions inside one trap by rotating their crystal is a different operation, the ion swap, and this rule does not concern it; nor does a swap-or-stay exchange on a C2LR machine, whose two crystals pass each other through the junction's shared waveform by design."
  source "deck_v3"
  for all a, b in hops where simultaneous(a, b) and rail(a) = rail(b) and not exchange(a):
    not (from(a) = to(b) and to(a) = from(b))

rule R6 "Each operation runs only where the site is equipped for it"
  about "Gates only in sites with a gate laser, measurement and reset only where there is readout, cooling only where there is a cooling beam."
  source "deck_v3; arXiv:2504.17886"
  (for all g in gates: can(site(g), "gate"))
  and (for all o in operations where kind(o) in {"measure", "reset"}: can(site(o), "spam"))
  and (for all c in coolings, i in ions(c): can(position(i, start(c)), "cool"))

rule R6b "A two-ion gate acts on two ions standing in one site"
  about "Both ions of a two-qubit gate are in the same trap when it starts, and in the trap the programme names for it, if it names one."
  source "arXiv:2504.17886"
  (for all g in two_qubit_gates, i in ions(g): position(i, start(g)) = site(g))
  and (for all g in two_qubit_gates where size(declared_sites(g)) > 0:
         site(g) in declared_sites(g))

rule R7 "A two-ion gate starts with cool enough ions"
  about "Both ions' motional energy at the start of a two-qubit gate is within the machine's budget; a cooling operation must come first otherwise. Below the budget the heat is not ignored: it is priced into the gate's error (R16, and the noise model behind every logical error rate). The budget is a hard limit because that error law describes the gate only while the ions stay in the Lamb-Dicke regime; a hotter gate is refused, not priced. A machine that declares no budget leaves only the price."
  source "deck_v3; arXiv:2511.15910"
  for all g in two_qubit_gates, i in ions(g):
    heat(i, start(g)) <= heat_budget()

rule R7b "A gate zone stays within its heat duty cycle"
  about "A gate zone may absorb only so much heat over time; no machine declares such a budget yet."
  source "arXiv:2504.17886"
  when declares_duty_budget():
  for all s in sites: duty(s) <= duty_budget(s)

rule R7c "A programme with two-ion gates cools"
  about "Under broadcast wiring cooling is not optional: a programme that gates and never cools cannot reach a useful error rate."
  source "arXiv:2510.23519; arXiv:2606.06455"
  when models_heating():
  count(two_qubit_gates) = 0 or count(coolings) > 0

rule R8 "An ion does one thing at a time" core
  about "No ion takes part in two operations at once: it cannot be gated in one place while it is carried to another."
  source "deck_v3"
  for all a, b in operations where a != b and simultaneous(a, b):
    disjoint(ions(a), ions(b))

rule R9 "The programme's figures are the replay's figures"
  about "Every time, cost, step count or heat figure the programme states about itself equals what replaying it computes."
  for all c in claims: approx(claimed(c), replayed(c))

rule R10 "The programme computes the circuit"
  about "The pulses the programme fires, read through which ion plays which qubit, compose to the circuit's operation; every gate is performed once, by its own ions, together in a trap that can gate."
  source "this website; arXiv:2406.19479"
  computes_circuit()

rule R11 "Along a loop, every ion moves the same way in a step"
  about "Transport along one loop is one direction at a time; and every junction's crossing time is declared by the machine (a junction of five or six rails the machine does not price crosses at the X-junction's time and heat, since no table measures one)."
  source "arXiv:2511.15910"
  (for all a, b in hops where simultaneous(a, b) and loop(a) = loop(b) and loop(a) != none:
     shift(a) = shift(b))
  and (for all j in junctions: priced(j))

rule R12 "One gate at a time in a trap"
  about "A trap's laser serves one gate at a time; different traps may gate together."
  source "arXiv:2511.15910; arXiv:2004.04706"
  for all a, b in gates where a != b and simultaneous(a, b):
    site(a) != site(b)

rule R13 "A gate's chain holds at most max_chain ions"
  about "A gate in a chain longer than about fifteen ions is slow and poor, so no gate starts in a site holding more."
  source "arXiv:2511.15910; arXiv:2004.04706"
  for all g in gates: occupancy(site(g), start(g)) <= max_chain

rule R14 "A split takes the ion at the end of its chain, or pays to reorder"
  about "An ion leaves its chain from the end that faces the rail; an ion further in must first be swapped to that end, which costs gates."
  source "arXiv:2510.23519"
  for all m in splits: at_chain_end(m) or swap_paid(m)

rule R15 "Heat figures are upper bounds"
  about "The heat from successive motions can interfere and partly cancel; the clock adds it up instead, so every heat figure is an upper bound."
  source "arXiv:2605.25118"
  when models_heating():
  heat_is_upper_bound()

rule R16 "Gate error depends on the ions' heat"
  about "The error of a two-qubit gate is computed from how hot its ions are when it starts, not taken as a constant."
  source "arXiv:2510.23519; arXiv:2605.25118"
  when models_heating():
  gate_error_reads_heat()

rule R17 "Ions heat with elapsed time, moving or not"
  about "Background heating accrues with time for every ion, whether or not it moves."
  source "arXiv:2605.25118"
  when models_heating():
  heat_accrues_with_time()

rule R18 "A junction is where three or more rails meet"
  about "Whatever a node is called, it is a junction exactly when three or more rails meet at it, and crossing it is priced by that number."
  source "quant-ph/0702175; arXiv:2305.03828; arXiv:1210.3655"
  for all n in nodes: (n in junctions) = (degree(n) >= 3)

rule R19 "A junction joins at most max_junction_degree() rails"
  about "A trap built in more than one layer has junctions of up to six rails, so 6 is the limit unless the machine declares a lower one (4 for a surface trap, which has T- and X-junctions and nothing denser). A junction of five or six rails crosses at the X-junction's time and heat unless its machine prices that degree itself: no shipped table measures one."
  source "collaborator review 2026-09; collaborator review 2026-10; arXiv:2201.12579"
  for all n in nodes: degree(n) <= max_junction_degree()

rule R20 "Rails meet at a wide enough angle"
  about "Any two rails meeting at a node make at least the machine's minimum angle (60 degrees unless it declares another)."
  source "collaborator review 2026-09; arXiv:2201.12579"
  for all n in nodes, r1, r2 in rails_at(n) where r1 != r2:
    angle(n, r1, r2) >= min_rail_angle()

rule R21 "Rails lie in a plane"
  about "A rail meets only the nodes it ends at, and two rails cross only at a node they share: the drawing must be a surface trap."
  source "collaborator review 2026-09; quant-ph/0702175"
  (for all r in rails, n in nodes: not lies_on(n, r))
  and (for all r1, r2 in rails where r1 < r2: not cross(r1, r2))

rule R22 "A transport step is one waveform"
  about "Under broadcast control every ion that moves in a step performs the exact same motion; a site may sit the step out, never do something else. A swap-or-stay step on a C2LR machine is one shared waveform by construction -- each crystal's only choice is its direction bit -- so the different routes its crystals take are not judged here (C2, C4 are its rules)."
  source "collaborator review 2026-09; arXiv:2510.23519; arXiv:2305.12773"
  when control() != "direct":
  for all a, b in transport where simultaneous(a, b) and not exchange(a):
    motion(a) = motion(b)

rule R23 "A junction is crossed, not rested on"
  about "No ion stops where three or more rails meet while the traps elsewhere have room for every ion. A slot of a loop or rail the programme moves as a whole is part of a conveyor, and is not such a stop."
  source "reader report 2026-09; deck_v3; arXiv:2510.23519"
  when count(ions) <= sum(min(capacity(s), max_chain) for s in sites where s not in junctions):
  for all i in ions, t in instants:
    position(i, t) in junctions implies rotated(position(i, t))

rule R24 "Every two-qubit gate of the circuit is performed, and no other" core
  about "Each two-qubit gate of the input circuit is carried out, and the execution performs no two-qubit gate the circuit does not ask for."
  (for all c in circuit_ops where needs_gate(c): gate_count(c) >= 1)
  and (for all g in two_qubit_gates: serves_circuit(g))

rule R25 "Each qubit's operations keep the circuit's order"
  about "On every qubit, each operation is over before the next one on that qubit begins, in the order the circuit is written -- even where two of them would commute."
  for all c1, c2 in circuit_ops where next_on_qubit(c1, c2) and performed(c1) and performed(c2):
    end(last(c1)) <= start(first(c2))