The swap

The above half has a mass bound of its own, and it is not what decides the fifths and quarters — the weight vectors whose parts, in fortieths, share a divisor of 8 or 10. A rule that abandons an atom covers the bar from the other atoms alone, whose whole coverage is 1 − w_r; so an atom abandoned by any rule meeting the bar at all weighs at most 1 − T. Call the weights under that line the feasibility window. At a bar of 3/4 the window ends at 10/40 and at 7/10 at 12/40, and the fifths' and quarters' lightest atoms, 8/40 and 10/40, sit inside it. What the window does is confine any abandonment to that lightest atom, its partners — the cell's other atoms — lying above the line. With the light atom abandoned the rest must cover T out of 1 − w_r, so the coverage they leave untaken is at most the slack 1 − w_r − T — 1/20 at fifths and zero at quarters at a bar of 3/4, 1/10 and 1/20 at 7/10 — and every label whose coverage exceeds the slack is one they hold.

Held labels are what an optimum can trade. Let an optimum abandon atom r and hold a pair on a partner of at least m times r's mass, the pair's coverage at most w_r times the sum of r's m largest posteriors, plus the optimum's own overshoot. Dropping that pair and taking r's top m labels costs no more — m labels at mass w_r against one at mass at least m·w_r — and still covers the bar, so the result is an optimum too, and it serves r. That is the swap. And the mass condition is an equality: the traded rule costs no more and an optimum costs least, so a swap that fires has the partner's mass exactly m·w_r — the swap is a divisibility statement. Nor need the pair come from one partner. Drop the lowest d_i labels each partner i of a set takes, and take r's top m labels: the result is an optimum exactly when Σ w_id_i = m·w_r and the dropped coverage is under the same bound — the set-valued swap. Its result takes no more labels than the abandoning optimum on any partner, and conversely, so one exists exactly when the abandoning optimum dominates, partner by partner, some optimum serving r.

At the nine fifths and quarters vectors at three atoms and the five at four, at bars 3/4 and 7/10 on the first family of rows, every optimum that abandons an atom peaking above the level is rescued by one swap. The one-pair swap reaches past them and not everywhere: of the three-atom weight vectors with no such failure at 3/4, 162 of 183 are rescued this way at every cell, and 105 of 105 at 7/10; at four atoms 23 of 29 and 5 of 11. The set-valued swap closes the rest, at every one of those 183, 105, 29 and 11 vectors. The 21 the one-pair swap misses at 3/4 all sit at zero slack, lightest mass 10/40, rescued at m = 3 by each partner dropping one label (12 + 18 = 30 = 3·10) or a 15/40 partner dropping two; the permutations of (8, 8, 12, 12) by one 12/40 partner dropping two (24 = 3·8), and at 7/10 by the two 12/40 partners together as well. And zero slack is a theorem. With ℓ labels the lowest d posteriors of a row average at most 1/ℓ, so a drop-set over partners served in full that conserves mass at m = ℓ loses at most w_r of coverage and gains as much: it rescues with no coverage condition at all — the full-partner drop-set. At zero slack the partners leave nothing untaken, so where every posterior is positive each is served in full, and at 3/4 with three atoms their masses sum to 3·w_r: no vector of lightest mass 10/40 has such a failure at 3/4, 30 of 30, the one-pair swap reaching 9. Below that band, at lightest mass 6/40 and under, abandoning optima appear whose every serving optimum takes MORE of some partner.

Those are exchanges too. A rule serving r with m labels is the abandoning optimum with a prefix of labels dropped on some partners, a prefix ADDED on others, and r's top m labels; it costs the optimum's cost less the dropped mass plus the gained mass plus m·w_r, so it is an optimum exactly when it covers the bar and the dropped mass less the gained mass equals m·w_r — the set-valued swap's equality with the gains on its other side — and it covers the bar exactly when the coverage dropped is at most the coverage gained, plus w_r times the sum of r's m largest posteriors, plus the abandoning optimum's overshoot. That is the gain exchange; every serving optimum is one, the set-valued swap being the case with nothing gained. At three atoms there are two partners, both dropping is a set-valued swap and both gaining pays for nothing, so every gain exchange there has one dropper and one gainer, and where each moves one label the dropper is the heavier. At masses (1, 18, 21) the abandoning optimum takes 0, 1 and 3 labels and the serving one 3, 2 and 2: one label dropped on the 21/40 atom, one gained on the 18/40, 21 − 18 = 3·1. And why no set-valued swap stands there is arithmetic before it is coverage — the arithmetic obstruction. A set-valued swap needs a drop-set over the partners the abandoning optimum serves, none dropping more than it holds, of mass exactly m·w_r for some m up to the label count; where the masses admit none, every rescue is a gain exchange before any coverage is read — at (1, 18, 21), no 18d + 21d' is 1, 2 or 3. At three atoms that is the case at 85% of the abandoning optima with a serving optimum and no set-valued swap at 3/4 and 89% at 7/10, the rest sitting at lightest mass 4/40 and 5/40 alone, where a mass-conserving drop-set exists and every one loses too much coverage. At four atoms, where the parts share a divisor of 4 or more and the gain cases sit at lightest mass 4/40 and 5/40, three partners that are multiples of the lightest and sum to 36 or 35 fortieths cannot all exceed 12 or 15, so a partner of mass 4, 8 or 12 — 5, 10 or 15 at lightest mass 5/40 — always exists, and the arithmetic case falls to 0 and 2%, the 2% being that partner abandoned too, holding nothing to drop. So the set-valued swap is the shape of the band without failures and not of the grid, and below the band at three atoms it is mostly the light atom's multiples missing every served partner.

Read across the whole grid, the shared divisor was never the variable; the lightest mass is. Failures of the above half are universal through lightest mass 5/40 and absent from 9/40 up at 3/4 and from 10/40 up at 7/10, and at lightest mass 8/40 the vectors sharing no divisor go 18 of 24 at 3/4 against 135 of 552 overall. The divisor returns at one edge, as divisibility: at 7/10 the six vectors of lightest mass 8/40 without such a failure are exactly the fifths, whose partner masses are multiples of the lightest, so two labels of the light atom trade evenly for one pair on a 16/40 partner; the 24 vectors at that mass sharing no divisor all fail. At a bar of 3/5 the fifths fail at the light atom, whose slack has doubled; the quarters fail only at 1/2.

Scope. Property for the window, the swap, its mass equality, the set-valued swap and the full-partner drop-set: algebra at any cell — any weights, any labels, any bar — and the zero-slack row at 3/4 with three atoms a theorem wherever every posterior is positive. Rule for the rescue at the fifths and quarters and for the set-valued swap closing the rest: the exchanges proved, the count exhaustive at every cell of every vector without such a failure, every rescue re-scored in exact integer arithmetic. The gain exchange and the arithmetic obstruction are properties, algebra at any cell, the exchange's equality and coverage condition asserted at every serving optimum of every abandoning optimum on the sweep — which is the level-excess identity's with its four-atom half restricted to the 119 vectors whose parts share a divisor of 4 or more — and the one-dropper, one-gainer shape at three atoms with them. The arithmetic case's four shares, the grading by lightest mass and the divisibility at the edge are observations on that designed sweep. Not here: a closed form for the grading in the slack above zero, where a partial partner's dropped label sits above its row's mean and the coverage condition returns — the gain cases at lightest mass 4/40 and 5/40, where a mass-conserving drop-set exists and fails on coverage, are that question. Toy scale.

verifiers: explore_ruler_swap.py, explore_ruler_multiswap.py, explore_ruler_gain.py