Redundant arithmetic

The Lebesgue margin is a size-only heuristic and prices the redundant leading end's delay only to within a digit. The delay itself is a closed form. Read ⌊(u/v)n + φ⌋, φ a rational phase, as a residual game: the reader has emitted a prefix, holds the residual m it still owes, and each turn the opponent injects the next input digit and the reader emits an output digit; the read is exact at lookahead c exactly when the reader can hold the residual inside some set forever, and the largest such set is the winning set. Scale the state by L = lcm(v, the denominator of φ) so every residual is an integer. Two bounds close on the winning set. The endpoint bound — inject the extreme digit ±a forever, and surviving forces |m| ≤ E(c) = ⌊aL(vb^c − u)/(v(b − 1))⌋. The flush window — a residual the reader can still flush satisfies ⌊m/L⌋ ∈ [−ar_c, ar_c], r_c the c-digit repunit; it is asymmetric, its top carrying a further L − 1, the overhang the floor's own truncation buys, so the two bounds bind side by side and often on opposite sides. Their intersection is an interval, and wherever the length test that follows grants, it is the winning set itself rather than a bound on it — and the game moves the residual by two steps, Lu/v per injected digit and Lb^c per emitted one, so an interval at least Lb^c long always has an emission carrying the injected state back inside it: the read is exact at lookahead c once the interval is that long. Nothing shorter will do when the two steps are coprime, and the general statement is a covering one. An emission moves the state by a whole multiple of Lb^c and so cannot change its class modulo that lattice: the reader's play is invisible there, and from a given state the injections alone sweep the successor across a coset of the subgroup their own step generates in Z/Lb^c — the multiples of g_c, the gcd of the two steps. Such a coset is exactly a class modulo g_c, holding Lb^c/g_c residues. But the emission lattice already tiles the line, so what a state needs of the winning set is a representative and never a value: call a class modulo g_c saturated when every one of those residues has a representative in the interval. The map carrying a class to its successor, t ↦ bt − (b − 1)Lφ (mod g_c), fixes the start class: the start state is Lφ itself in those same scaled units, and the additive term is built from it, so b·Lφ − (b − 1)Lφ = Lφ. The orbit that decides the start state therefore never moves, and the read is exact at lookahead c exactly when that one class is saturated. Coprime steps leave one class, saturated exactly when the interval is Lb^c long: the length test is the one-class case of the saturation test. So the least granting c is the delay. A phase translates the flush window and does nothing else, so a phase can never RAISE the delay, and it lowers it by one exactly where the endpoint bound binds on the right while the window binds on the left. The Lebesgue margin is this criterion with its floors dropped, which is why it lands within one digit and why it misses in BOTH directions: over 169 cells the true delay runs one digit above it at 18 and one below at 14, never two off. One corner the size-only reading gets wrong outright: slopes b^k with k ≥ 0 read at k, but dividing by the radix is a free shift only when a ≥ b − 1 — below that it costs one digit at every depth alike, a strictly stronger demand on the digit set than redundancy.

Scope. The rational-slope delay is proved entire — both bounds, the phase lemma, the sufficiency of the length test and its necessity — for every radix, every symmetric redundant digit set, every rational slope and every phase, no computed value load-bearing; it is an iff wherever the injection step Lu/v and the emission step Lb^c are coprime. The b^k corner is proved in both halves by two different routes: k < 0 is that iff read at c = 0, where the injection step is 1; k ≥ 0 sits outside it, where the two steps share everything, and is settled by hand — E collapses to 0 at c = k and the surviving singleton is invariant, while at c = k − 1 the bound is already negative. Where those two steps share a factor the saturation test takes over, and it too is proved entire at that same scope, by the fixed point above: the start class is its own orbit, so the delay is decided by one class and the demand that the digit set cover the subgroup in a single step (Lb^c/g_c ≤ 2a + 1) is no condition on the law. What that demand was carrying is the gap between the start state and a general one, and for a general state the winning set is not a class condition at all. Redundancy makes j steps reach an interval of 2ar_j + 1 multiples of the injection step — a proper sub-progression of the state's own coset until the depth J = min{j : 2ar_j + 1 ≥ Lb^c/g_c} at which it becomes the whole coset — and a state wins exactly when that reachable set misses the interval's complement at every depth. That is proved for every radix, redundant digit set, slope and phase, and with nothing uncovered: the argument needs the interval to be no longer than Lb^c, so that a residue has a representative in it, and where the interval is longer the length test above already grants and already hands over the interval itself — which is the same set this condition names there, its complement being empty. The two cover every case between them. Below J it turns on the state's residue rather than its class: the class reading fails there, at 21 of the 55 cells of a census to radix 12 and lookahead 5 where a disagreement is possible at all — cells outside it carry the same failure — the smallest at radix 2 with digits {−1, 0, 1} and slope 12/5 at lookahead 2, where the game has 13 winning states against that reading's 9. Every one of them dodges at the FIRST depth, so the dial is the digit set and not the lookahead: all 21 sit at the redundancy floor, 2a + 1 ≤ b + 1, the narrowest digit set still redundant, hence the fewest reachable states. That is where to look rather than a test — 52 of the 55 sit there too. One quantity accounts for both. Write a state as its class together with its position in that class: the class holds Lb^c/g_c residues evenly spaced g_c apart, and the position is the index of the state among them, running over Z/n with n = Lb^c/g_c. In that coordinate the interval's complement meets a class in a single block of λ consecutive positions — the indexing wraps the circle once, and λ = 0 exactly when the class is saturated. Depth j's reachable set, meanwhile, lands in the class j successor steps along, CENTRED on the state's position there and spread over 2ar_j + 1 positions in arithmetic progression by a fixed step — the injection step's own image, a unit of Z/n. Below J that is fewer positions than the class holds, so the progression sits scattered around the circle rather than filling it. The state fails depth j exactly when that point set MEETS the block, so as the centre ranges over the class the survivors are one run per gap of the point set longer than λ, of length gap − λ. Those gaps take at most three lengths, read off the continued fraction of the step. A class can dodge at all iff its widest gap exceeds λ. That is the monotonicity beneath the floor: the point set only grows with a and with j, and adding points subdivides gaps rather than merging them, so the room to dodge is widest at the narrowest digit set and at the first depth. So the shortfall the length test can suffer — an interval falling short of Lb^c by as much as g_c − 1 — was a defect of the TEST and never of the law, and it closes at all 67 measured cells. What lives in that band is a winning set gone sparse, and at every one of those 67 it is a union of classes modulo g_c rather than a lattice, several surviving where the naive step-g_c reading expects one. Of 21 such cells that reading is right at the 9 carrying a single class and nowhere else — and at radix 3 with digits {−2..2}, slope 1/3 under phase 1/8, the survivors are {0, 2, 3} mod 8 and the winning set is no arithmetic progression at all. The 1974 cells across two grids sharing no window that carried the iff before it was proved now check the derivation instead.

verifiers: explore_slope_proof.py, explore_slope_lattice.py, explore_slope_tail.py, explore_slope_tree.py, explore_slope_dodge.py

The dodge criterion above prices ONE depth. A class can LOSE several — its tree landing in an unsaturated class at each of them — and what a state must then survive is all of them together. Wherever that question can be asked λ = 1, and is forced rather than observed: an interval falling short of Lb^c by g_c or more leaves no saturated class at all and hence nothing to assemble, so wherever there is something the complement is a run shorter than g_c, and a run that short meets a class's residues, spaced g_c apart, at most once. Each block is a single position then, and the positions failing depth j are the ones whose point set covers that position. Written out, they close up into one run pulled back: those w with b^jw + d_j inside a centred run of 2M_j + 1 values, M_j = ar_j the run's half-width and d_j the depth's own offset. Call that set of positions level j. Losing two of them is ordinary rather than exotic: 262 cells carry such a class below Lb^c = 6000 in a phase-0 sweep to radix 12, the smallest at radix 2 with digits {−1, 0, 1}, slope 40/9 and lookahead 3, where four classes lose depths 1 and 2 alike and the game has 37 winning states against the class reading's 17.

The ambient interval is not a second kind of constraint on top of those: it is level 0 of the same family — no tree, and its own set is the block itself — so every inclusion–exclusion term containing it is settled by enumerating that one position. That leaves ONE lattice term, a single pairwise intersection, and b^jw is a function of bⁱw whether or not b is a unit modulo n, so a gcd reduction carries it to a count of one run's points whose image falls below a threshold: two floor-sums, O(log n). The SIZE of a class's winning set is then a closed count, with no walk over the interval anywhere in it. A level sitting inside a deeper one is forgotten by the union, so a family of any size reduces to its maximal levels, and the number of those is the family's width; the count closes as soon as the width is at most 2. But width 3 exists — 4844 classes over 29,233 cells (a radix, digit set, lookahead, slope and phase together) with Lb^c ≤ 150,000, the smallest at 11,664 under radix 6 with digits {−4 … 4} and slope 4384/9, whose class 1 loses depths 1, 2 and 3 — and there the closed form has no formula for the triple term.

The count survives anyway, because at every one of those 4844 the triple term is EMPTY — the two shallowest maximal levels never meet, and a triple cannot outlive its pairs. What makes that sayable before any of it is looked at, and what says which pair it will be, is one coordinate: meeting is the containment test at a second radius. Write Δ = j − i. The repunit identity r_j = b^Δr_i + r_Δ makes M_j = b^ΔM_i + M_Δ exactly, and b^ΔM_i stays under n/2, so the deeper level's run is the shallower one's image lengthened by 2M_Δ and nothing wraps. One quantity then decides both questions — the offset y between the deeper run's centre and the image of the shallower run's, shifted by M_Δ and read modulo n. Level i lies inside level j whenever y ≤ 2M_Δ, a radius set by the DIFFERENCE of the two depths; the two can meet at all only where y ≤ 2M_j, or in the mirror arc at or above n − 2M_j + 2M_Δ — a radius set by the DEEPER depth alone. So a pair carries a meeting measure μ = (4M_j − 2M_Δ + 1)/n — the share of the circle an offset must land in for a meeting to be possible at all, clamped at 1 where the two arcs have overlapped and the count reads the circle twice — before any y is looked at. And a third maximal level caps that measure for the two shallowest: i₃ is itself a level below J, so 2M_i3 + 1 ≤ n, while the same repunit identity gives M_i3 > bⁱ³⁻ⁱ²M_i2, whence μ_shallow < 2/bⁱ³⁻ⁱ². A factor of b is what the third level buys, and it is bought only for the SHALLOW pair: measured max 0.4118 and median 0.178, against a median of 0.892 and a max of 1 for the single pair of a width-2 family, which has no third level under it.

Scope. The assembly is a property: level 0's collapse and the gcd reduction ask nothing about which residues are attained, and the closed count matches a state-by-state walk at 1684 of 1684 classes losing two levels, over all 219 cells with Lb^c ≤ 3000, its pair term against a direct walk over Z/n at 3766 pairs. The two radii and the cap are properties too — a repunit identity with b^ΔM_i < n/2, and 2M_i3 + 1 ≤ n with the same identity — checked at 0 violations of the meeting radius over 1,786,658 pairs and 0 of the cap over 5656 width-3 classes. The containment radius is sufficient and NOT necessary: its converse declines a containment that really holds, at 284 pairs of the smaller census and 1436 of the larger, so a width read off the derived half alone is an upper bound on the true one — coverage, never soundness. Every width quoted above is measured containment in both directions instead, the reverse containment occurring nowhere, a deeper level being the larger set. That the shallow pair is empty is a pattern and nothing stronger: 4844 of 4844 at Lb^c ≤ 150,000 and 812 of 812 at a census carrying a sixth of that population, phase 0 throughout, with every one of those emptinesses falling to the interval bound rather than to the discreteness of the values an offset can take. The cap bounds the measure and is not a proof that no offset lands inside it, and no derivation is on offer here; what a triple term would need to become owed is a width-3 class with all three pairs non-empty, which none of the 4844 carries.

verifiers: explore_slope_assemble.py, explore_slope_width.py, explore_slope_empty.py

The two radii above are both conditions on the offset y: one level lies inside the other when y ≤ 2M_Δ, and the two meet at all only when y ≤ 2M_j or y is at or above n − 2M_j + 2M_Δ. What is left between them is where the levels meet WITHOUT one containing the other, and it is two arcs: the lower arc 2M_Δ < y ≤ 2M_j, and the upper arc, its mirror at the top of the circle. What a level pair presents is not offsets, though: it is the b^Δ carries its window holds, each mapping to one offset, and an arc counts as empty when no offset the pair can attain lies in it — so settling that by walking the carries costs b^Δ. It is one inequality per arc instead, because every offset's carry has a closed form. The quantity the form is built on is κ, formed from the same a(Lb^c − u) the endpoint bound E above floors, and the redundancy condition 2a + 1 ≥ b is load-bearing rather than a convenience of the sweep: it is what makes κ's own multiplier non-negative, so that κ = 2au mod Lb^c is a residue rather than a signed combination and the identity is a reduction. With h = gcd(2a, b − 1) and τ(y) = (−y(b − 1)) mod 2a, every offset carries C(y) = ((Lb^cτ(y) + yκ)/(2ag_c)) mod n — a TWO-TERM cost, so a small carry needs a small y and τ = 0. The outer reduction is what makes that a formula rather than a range: τ supplies the wrap only while yκ < Lb^c, and the wraps dropped past that point are exactly the outer modulus, so the form carries no side condition and reaches all of Z/n. And τ vanishes on the multiples of 2a/h alone, so the containing carries — those whose offset puts one level inside the other — run 0, s, 2s, … in a progression of step s = κ/(hg_c).

Both arcs then read off that one step, over the pairs where containment has already failed. The lower arc is empty iff (hr_Δ + 1)s ≥ b^Δ — containment holding out to index hr_Δ along the progression and the arc out to hr_j, so what the inequality asks is whether the first index past containment is already outside the window's range. At most of this population's cells that is derived and not merely verified. Call a cell rigid when its interval falls as far short of Lb^c as the population permits, by g_c − 1, and the endpoint bound's own floor is exact — which is where the step meets its ceiling (b − 1)/h, the two coinciding exactly. There the inequality reads b^Δ − 1 + s ≥ b^Δ for every b, h and Δ, so at a rigid cell the lower arc is empty by property, with margin s − 1 and no enumeration anywhere in the argument. The upper arc is empty iff nh ≥ 2ab^Δ + hsy_max, evaluated at the class its cost is least on, τ′ = h — least by property and not by search, stepping τ′ up costing nh and buying back at most 2ag_cs — with y_max the largest admissible offset in that class. The added term is what the level difference costs: the lower arc's own hypothesis, with a price attached.

The two halves are not equally protected, and that is where the law ends. The population the lower arc's rule is read on is cut at meeting measure μ < 0.4, and that cut ENFORCES its hypothesis — a class losing three levels forces n > 2ar₃ and the cut forces Δ ≤ 2, the measured minimum of nh/(2ab^Δ) being 5.78. It does not enforce the upper arc's: below the cut it gives n > 10ar_j − 5ar_Δ against the 10ar_j + 2a that criterion wants at b = 6. So a failure was predicted just above the cut, and it is there: μ = 0.4597 at Lb^c = 22032 — radix 6, digits {−4..4}, lookahead 4, slope 8272/17, levels 1 and 3 — where seven offsets are attainable in an arc the criterion calls empty. The empty-window law is a below-the-cut law, and at this cap the margin is 0.0597.

One consequence needs none of the derivation. The count the criterion replaces is a floor-sum: per τ class the carry runs as an arithmetic progression in Z/n, so counting a window costs O((2a/h)·log n) against the walk's O(b^Δ).

Scope. Rules on a phase-0 census of level pairs with Lb^c ≤ 60,000, over cells carrying a class that loses at least three levels. The carry's closed form is pointwise exact at 1,868,112 offsets with 0 misses, one in five of them beyond the unreduced form's range. The lower arc's criterion is verified in BOTH directions over the 3516 pairs below the cut — the 8 failing the inequality are set-equal to the 8 whose window holds an attainable offset, and they are one cell, which is not rigid; below the cut the upper arc is empty at all 3516, which is what makes that window the lower arc alone — the closed form and a loop over all b^Δ carries agreeing pair by pair with no shared code path. The rigid-cell reading and the least-cost class τ′ = h are properties, the second printed to hold at all 10,852 non-contained pairs rather than assumed. The upper arc's criterion agrees with an independent count at 4668 of 4668 scored, which is 4668 of those 10,852; the remainder is SCOPE and not a sample — 3996 whose arcs overlap and so have no upper arc, and 2188 whose tightest offset needs a wrap the criterion, unlike the count beside it, is not derived over. The floor-sum count agrees with the loop at 10,308 of 10,308. At a rigid cell the upper criterion admits a clean SUFFICIENT reading, nh ≥ 2ab^j, and that reading is a bound and not the criterion: it is exact at 0 cells of the census, and it misses 16 of the 2972 rigid below-cut cells whose upper arc is empty anyway.

verifiers: explore_slope_step.py, explore_slope_arc.py

When does addition itself go local? Take a contiguous digit set D = {−a⁻..a⁺} at radix b — the symmetric sets above are the case a⁻ = a⁺ — with slack ρ = a⁻ + a⁺ + 1 − b, the count of digits beyond the radix, and spread W = a⁻ + a⁺. The sum of two streams is exactly local at lookahead c = 1 iff ρ ≥ 2 and b ≥ 3 and D is not a slack-2 set with an end at magnitude 1, and at c = 2 otherwise — proved for every radix and every contiguous set with ρ ≥ 1. The three clauses unpack one inequality, ρ ≥ ⌈a⁻/(b − 1)⌉ + ⌈a⁺/(b − 1)⌉: a side of reach x spends ⌈x/(b − 1)⌉ units of slack — an end at 1 a full unit, an end at 0 none, which is the whole end clause; {0..4} at radix 3 reads at c = 1. Necessity: extreme injections trap the emission game's winning set inside the interval [−(a⁻ − ⌈a⁻/(b − 1)⌉), a⁺ − ⌈a⁺/(b − 1)⌉], and an injected digit stamps its successor's residue class mod b, so a nonempty winning set must span b consecutive values — which fits iff the inequality holds. Sufficiency: exactly that interval is then invariant. So the winning set is the interval, or empty; the proof is checked against the game's computed fixed points at 354 contiguous systems, the winning set matched cell-for-cell. The end clause is invisible to symmetric sets, whose slack-2 members are forced to ends of magnitude ≥ 2. The conditions are signed-digit arithmetic's own: the threshold ρ ≥ 2 is the hardware literature's stated look-back condition, radix ≥ 3 is its founding framework's domain, and the end clause matches a hedge over "a few cases" of slack 2 in its threshold statements — here the pieces arrive as one iff, through window locality rather than carry-propagation analysis.

The Lebesgue margin is what the slope delays above sit within one digit of, and a sum injects a spread of 2W, so it grants the smallest c with b^cρ ≥ 2W. It never underpredicts at any lookahead, and it overpredicts by exactly one digit precisely where the law grants c = 1 while ρ(b − 2) < 2(b − 1) — contiguity ties W = ρ + b − 1, so this is bρ < 2W, and the margin's grant reads only radix and slack, never the set's shape. Both halves follow from the law and that substitution: the margin never reaches c = 0 (ρ < 2W always) and always grants the c = 2 that always suffices, and its c = 1 region — slack ≥ 4 at radix 3, slack ≥ 3 at b ≥ 4 — sits inside the law's inequality by the same case analysis that unpacks its clauses, so the wedge is slack 2 alone at b ≥ 4 and gains slack 3 at radix 3; on the census that is 31 of the 214 cells, 28 at slack 2 and three at slack 3. A symmetric set locks the slack's parity to the radix's (ρ = 2a + 1 − b), so an odd radix realizes only even slack: a symmetric sweep sees half the (b, ρ) grid, and on that half the wedge is indistinguishable from "slack 2" — asymmetric sets fill the other half and separate the two. And the wedge is the margin's, not addition's — settled by a shared margin rather than by a matching wedge. The endpoint above, a⁺ − ⌈a⁺/(b − 1)⌉, is the slope criterion's E at slope 2 and c = 1, verbatim at every radix 3 to 40: ONE shape-aware object serves both operations, and the Lebesgue count is that object with its floors dropped, which is what the one-digit slop is made of on either side. The end exception stays addition's own, never surfacing in scaling.

Scope. The law is a criterion — necessary and sufficient, proved for every radix and every contiguous digit set with ρ ≥ 1, no computed value load-bearing. The margin's story — never underpredicting, one digit exactly on the wedge — is proved at that same scope, the census cells now the check on the chain rather than the evidence, each mirror pair of digit sets counted once; both are addition's own, the never-underpredicting half included — the slope side above misses on both sides. The margin shared with scaling is an identity, checked at 760 cells over radices 3 to 40. Contiguous digit sets only.

verifiers: explore_lookahead_proof.py, explore_margin_wedge.py, explore_redundant_lookback.py, explore_margin_locus.py