The Binary Totient Series

The unconditional record

The following hold with no irrationality hypothesis. They are the results a specialist should know before reading further; each is stated at the scale at which it is actually proved.

This is obtained from a classical Stern–Brocot gap lemma () applied at window \(K = 240\), the last rung of the ladder \(4838 \to 2^{22} \to 2.49\times10^{17} \to Q_0\). It is logically independent of \(\mathrm{Sep}\): it uses no certificate and no period apparatus. Its own open continuation is whether \(\sup_K (b+d)(K) = \infty\); that would close #249 through this theorem’s consumer. [Open]

Propositions \(\ref{prop:sign}\)–\(\ref{prop:parity}\) are the four facts a reader should carry into the next section: the corpus’s best cofinal information is half a certificate, its best rank information runs the wrong way, its reformulations are equivalences rather than reductions, and every purely qualitative property of the coefficient word is satisfied by a rational countermodel.

The plane the barriers live on

Fix two axes for a hypothetical proof of \(\mathrm{Sep}\) (Definition \(\ref{defn:sep}\)): the range of indices at which it consults \(\varphi\), and the resolution at which it consults them. Two derived axes matter as well: the size of the proof’s internal bookkeeping (carry state, \(\mathbb{Q}\)-rank, shift-polynomial degree), and whether the target is asserted pointwise at a chosen index or as an average over a block.

• The quadrant [full resolution \(\times\) bounded range] is closed by Theorem \(\ref{thm:gamma}\) (B1): \(\varphi\) may be pinned exactly on \([1,B]\) and the series can still be rational.

• The complementary quadrant [coarse resolution \(\times\) unbounded range] is closed by Proposition \(\ref{prop:parity}\) (B7): \(\varphi\)’s parity may be pinned at every index, together with boundedness, \(c(n) \le n\), and arbitrarily strong aperiodicity, and the series can still be \(3/2\).

• The remaining quadrant is closed whenever the proof compresses: B5 (no bounded carry state, no fixed-precision signature) and B6 (four independent finite truncations of the totient kernel, all with trivial kernel).

• B4 closes the one construction that tried to reach the good quadrant by prescribing values: residue engineering pays for amplitude in position, and position enters the certificate radius.

• B2 closes the escape of retargeting; B3 records that no bounded result in the corpus has ever promoted.

The corpus’s own results partition along these axes perfectly, which is the first evidence that the axes are the right ones. Every unconditional finite deposit (Proposition \(\ref{prop:deposits}\), the \(K=240\) Farey rung of Theorem \(\ref{thm:denom}\), the actual-LCM orbits at \(a = 4\) and \(a = 6\)) sits at full resolution and bounded range, so B1 says extending them is evidence forever and proof never. Every unconditional cofinal theorem (letterwise positivity for all \(a \ge 8\), the tail bounds from \(\varphi(m) \le m\), unbounded Mersenne-shadow denominator growth) sits at coarse resolution and unbounded range, and Proposition \(\ref{prop:sign}\) proves in the corpus’s own coordinate that this is exactly half a certificate.

B1: the finite-inspection barrier, as a theorem

B1 is the one barrier that is a genuine no-go theorem about proof method, so it is stated and proved as one. The generic vocabulary is needed first. For \(c : \mathbb{N}\to \mathbb{N}\) with \(c(n) \le n\), write \(T_c := \sum_{n \ge 1} c(n)/2^{n}\), \(R^{c}_{N} := \sum_{j \ge 0} c(N{+}1{+}j)/2^{\,j+1}\), \(A_c(h,N,L) := \sum_{j<L}(c(N{+}h{+}1{+}j) - c(N{+}1{+}j))2^{\,L-1-j}\), and let \(\mathrm{Kill}_c(h,N,L)\) and \(\mathrm{Sep}_c\) be \(\mathrm{certifiedKill}\) and \(\mathrm{Sep}\) with \(A_c\) in place of \(\mathrm{windowDiscrepancy}\). For \(c = \varphi\) these are the objects of Definition \(\ref{defn:sep}\).

The Lean-formalised sibling of the same mechanism — a lacunary zero-valued coboundary splice — is Proposition \(\ref{prop:parity}\), which is B7. B1 and B7 are the two object-level witnesses of the wall, one along each axis.

B2–B7

Each barrier below is stated as a claim about a class of arguments, with its status never blurred. Proved means there is a theorem (Lean or ordinary mathematics, as marked) whose content is the elimination. Observed pattern means an audit over the corpus: real evidence, not a theorem, and it is never used as a premise elsewhere in this document.

The shape

Put together, the barriers say something more specific than “the problem is hard”. The certificate residue is a weighted accumulation over an unboundedly long window at full arithmetic resolution, and every device that makes an argument finite destroys precisely the quantity being measured: bounding the window (B1), coarsening the values (B7), compressing the state (B5), truncating the rank (B6), or letting the prover pick the sample (B2). B4 closes the remaining escape — buying the amplitude by construction — with an explicit exponential margin, and B3 records that in practice nothing bounded has ever promoted.

There is exactly one known way to hold unbounded range and full resolution at once without a finite bookkeeping device: stop naming an index and assert an average instead. That is what an exponential-sum bound is. It is why the surviving routes of §\(\ref{sec:survivors}\) are, with the honest exceptions noted there, the ones that never name a good index.

Survivor 1: the first-harmonic block cancellation bound

The real-part form suffices and is strictly weaker: it is enough that \(\sum_{N \in [X,2X)} \mathrm{windowFirstCos}(h,N,L) \le \tfrac{9}{10}X\) (, the elementary unconditional engine; the \(21/25 \to 9/10\) bridge is ). Unpacked, the required object is a constant-saving cancellation estimate for the dyadically weighted totient-difference exponential sum \[\sum_{X \le N < 2X} e\!\left(\frac{\sum_{j<L}\bigl(\varphi(N{+}h{+}1{+}j)-\varphi(N{+}1{+}j)\bigr)2^{\,L-1-j}}{2^{L}}\right), \qquad L \approx \log_2 X + O(1).\] Not one instance of this bound is proved anywhere, at any \(X\), \(h\) or \(L\). Both trees were searched for a theorem supplying it; only consumers exist. [Open]

Survivor 2: the four-term pivot budget

Same lane as Survivor 1, with the analytic burden repackaged. Split the block sum at a largest-prime pivot into centred correlation, fibre-mean, bad-cofactor and non-supplier contributions and bound the four separately.

It inherits Survivor 1’s evasions of B1, B4, B5, B6 and B7 verbatim: the four terms are exact finite sums over canonical largest-prime supplier fibres of the same accumulated-word phases, with no sample choice and nothing prescribed. Its specific advantages are three. The decomposition is an exact identity, proved unconditionally with #print axioms clean (, budget consumer ). The one-sided budget lowers the hard requirement from a norm bound \(\lVert \cdot \rVert \le X/2\) to a real-part bound \(\le 14X/25\). And the pivot rests on genuine arithmetic rather than a sampled surrogate: on the canonical fibre \(m = 1\), \(s = L-h\) the supplier set is literally the shifted dyadic interval of primes, proved as a membership equality (), with the totient factorisation at the pivot the honest \(\varphi(mp) = \varphi(m)(p-1)\) and the non-divisibility discharged by size. Three of the four terms are then counting bookkeeping; only the first needs a genuine correlation estimate, and only in real part.

What it must respect. B6 has a residual-gauge instance: a residual-blind determinant or conditioning test cannot certify that genuine phase reconstruction rather than a locked degenerate configuration has occurred (). So this route must couple rows by an extra arithmetic identity, not merely gauge-normalise columns. Honest status: strictly a repackaging of Survivor 1’s burden; it is listed separately only because three quarters of it are already exact identities on disk. The module asserts no prime-distribution or decorrelation estimate — the socket is deliberately empty. [Open]

Survivor 3: uniform quantitative escape at cofinally many primes

It evades B1, B4, B5, B6 and B7 for the reasons given for Survivor 1: a statement about the true real tail difference at unbounded prime positions, with no letters prescribed, no bounded state, no rank, no coarse coefficient-word invariant. It evades B2 by the second of the two exemptions in Proposition \(\ref{prop:b2}\) — not by denying sample choice, but by demanding a uniform margin. Irrationality gives non-integrality of every tail difference and supplies no lower bound whatever on distance to \(\mathbb{Z}\); certificate completeness therefore cannot manufacture this predicate.

Honest demotion. This is a pointwise producer: it requires naming a good prime, and Observation \(\ref{obs:pointwise}\) records that no pointwise producer in this corpus has ever been supplied at even one large index, across seven independent attempts. It evades every proved barrier while sitting inside the class the strongest observed pattern indicts. Nothing on disk proves it at a single prime for a single \(h\). It ranks below Survivor 1. [Open]

Survivor 4: depth-locked full-depth escape

This is the shortest fully stated open inequality the programme has produced. Its evasion of B2 is recorded on disk rather than argued: its ambient parent \(\mathrm{PeriodMultipleKillSupply}\) is proved equivalent to \(\mathrm{Irrational}(S)\) and \(\mathrm{ApFullDepthEscape}\) implies it (), so it is at least as strong, and possibly strictly stronger — the file’s own docstring records “sufficient for irrationality; not known necessary”. Being possibly strictly stronger, certificate completeness cannot collapse it back. It evades B1 (both \(N\) and \(t\) unbounded), B4 (locking depth to the period means the entire word accumulates and no letter is prescribed), B5 and B6 (no state, no rank). Its substance is pure anti-concentration: via , the difference of two adjacent period blocks must have central residue mod \(2^{h}\) at some multiple period \(h = td\), and the room condition is automatic once \(h\) is large, so nothing but the residue’s position is at stake.

Honest demotion, identical to Survivor 3: it is a pointwise producer and names an index. It is listed because it is the cleanest target for computational exploration — with Theorem \(\ref{thm:gamma}\) as the standing reminder that no amount of such exploration becomes a proof. [Open]

Survivor 5: the rationality-side rank upper bound

This is the only surviving obligation that is not a residue or certificate statement at all, so B2’s certificate completeness cannot reach it — it is not a reformulation of \(\mathrm{Sep}\) in any vocabulary. It evades B1 and B4 entirely (no window, no letters, no prescribed residues) and B5 (linear algebra over the whole orbit, not a bounded-state summary). The scale side is finished and uniform in \(e\) (Proposition \(\ref{prop:rank}\)).

Honest flag, and it is severe. B6 partly indicts this route from inside. The most natural approach to the upper bound is dead (), and what rationality actually buys — uniform eventual periodicity of the carry’s dyadic sections mod \(v\) — provably does not promote to a \(\mathbb{Q}\)-rank bound (Proposition \(\ref{prop:period-not-rank}\)). So this survivor is genuinely coordinate-disjoint from everything else, which is its whole value, but its obvious approach is closed and the missing input is a rigidity theorem nobody has stated.

Evidence bands.

Every claim carries one, and they are never blurred. [Lean] means kernel-checked, with the declaration named and the file:line given. [Cert] means an exact finite computation, valid exactly on the stated range. [Math] means ordinary mathematics, proved here or elsewhere but not formalised — Theorem \(\ref{thm:gamma}\) is the important instance, and its unformalised composition step is flagged where it occurs. [Cited] means published, with the reference. [Open] means not proved, by anyone, anywhere. A proved no-go and an audit over a corpus are both valuable and are never conflated: B1, B2, B4, B5, B6 and B7 are proved eliminations; B3 is an audit and is labelled as evidence every time it is used.

The scale axis.

This is the load-bearing axis of the whole document. scale:fixed means one instance; scale:bounded means every instance up to an explicit bound; scale:cofinal means infinitely often past every threshold; scale:uniform means for all parameters with no dependence. The single most important structural fact about the corpus is narrower: every direct certificate deposit for \(\mathrm{Sep}\) is fixed or bounded, although the corpus also contains uniform and cofinal structural theorems. Those stronger-scale results do not produce \(\mathrm{Sep}\). Theorem \(\ref{thm:gamma}\) says that no accumulation of bounded verification, at any bound, is evidence that the cofinal statement holds. Read every result’s scale tag before reading its content.

Coordinates, and why obstructions are relative to them.

Every obstruction carries a coord tag, because an obstruction is always an obstruction in a representation, never a property of the object. The \(\gamma\)-splice obstructs arguments in the coord:binary-digit coordinate; the rank floor lives in coord:carry-rank; positivity lives in coord:actual-lcm; the Farey exclusion lives in coord:farey. Two consequences follow, and both matter for anyone attacking the problem. First, before reporting a new wall, name the coordinate it was met in and test a re-representation. Second, an obstruction proved in one coordinate is silent about another: Survivor 5 survives precisely because it is coordinate-disjoint from the certificate lane, and Survivor 1 survives because the first-harmonic coordinate is the one in which the corpus’s proved collapse mechanism has no purchase.

Map of what follows.

The premise catalogue records, for each coordinate, the exact statements the corpus holds, with hypotheses, evidence band, scale, and Lean declaration. It is followed by the typed-implication tables (which statement feeds which, and at which quantifier shape), the near-miss index against the open obligations, and the promotion audit whose verdicts are summarised as B3. Nothing after this point restates the barriers; they are all here.

Read this in full before starting.

That instruction is not politeness. The recurring practical failure of this programme has not been a shortage of ideas; it has been rediscovering the same reformulations, because no single document held the whole picture. Every dead route in §\(\ref{sec:wall}\) was found more than once. If you are about to prescribe totient values at engineered positions, read B4 first. If you are about to define a bounded carry state, read B5. If you are about to look for a weaker sufficient condition, read B2 — there probably isn’t one, and the corpus has already proved as much three times. The purpose of assembling the wall is that the next attempt should start where the last one stopped.

The object

The binary-digit reduction

The unconditional denominator floor

The strongest unconditional fact the corpus holds about \(S\) is a lower bound on its denominator should it happen to be rational. It is obtained by a completely elementary Farey/mediant argument, entirely free of any certificate or period apparatus, and is therefore logically independent of the open certificate-supply obligation.

This lemma is a classical Stern–Brocot fact with zero totient or Mersenne content; it is the generic engine underneath every Farey-gap bound in the corpus, for either open problem.

The same record, transported: the Möbius-square and coprimality-probability forms

The exact finite Farey record behind Theorem \(\ref{thm:denom-record}\) is not tied to the \(\varphi(n)/2^n\) presentation of \(S\); it transfers verbatim to two other exact reformulations of the same constant, at exactly half the bound.

The Möbius–Mersenne identity and why bounded coefficients matter

The squared-Lambert gcd-moment identities

This one identity, at \(r=1/2\), specialises to every squared-Lambert rung the corpus computes; two instances are exact and directly relevant to #249’s weight structure:

The exact certificate record: the contiguous band through \(t\le82\)

The certificate apparatus itself (the predicate certifiedKill, its soundness/completeness theorems, and the cofinal supply obligation that is the actual open target) is developed in full in Part 1 of this paper. What is recorded here is a representative historical set of machine-checked anchors, together with the current aggregate theorem closing every scale \(t\le82\). The declaration inventory, rather than this table, is authoritative for all individual certificate shards; no extrapolation beyond the stated band is implied.

Producers

Producers conclude an existence or a supply: a witnessed object, a witnessed finite family, or an unconditional dimension/growth lower bound obtained by exhibiting witnesses (CRT, Dirichlet primes in AP, Bertrand’s postulate, explicit decide computation). Sorted by scale: uniform, then bounded, then fixed; no producer in this lane is cofinal (the cofinal-scale reduction theorems are consumer-shaped and are catalogued as converters below, since each moves a cofinal hypothesis across a coordinate boundary to the target conclusion).

Converters and exact identities

Converters and identities move a statement between coordinates without changing its truth value: definitions, exact algebraic identities, iff-characterisations, and the implication theorems that convert a supply hypothesis in one coordinate into the target conclusion \(\mathrm{Irrational}(S)\). This subsection carries the certificate-kernel core (the Sep(h,N,L) predicate, its completeness iff, and every known reformulation of the open supply obligation) and the Möbius–Mersenne / squared-Lambert identity family, including the Mersenne–Lambert five-row status ladder. Sorted by scale: foundational (n/a) definitions and identities first, then uniform, then cofinal, then bounded, then fixed.

Consumers

This subsection lists every premise in the corpus whose conclusion is conditional on an unsupplied hypothesis, with that hypothesis rendered in display maths so an agent can recognise it as a search target. All targets below are logically downstream of the single exact equivalence that defines the open problem:

Invariants

Necessary conditions that any successful (or unsuccessful) approach must be consistent with — facts a solution cannot contradict, whichever way #249 eventually resolves.

Killers and countermodels

Adversarial constructions and no-go results, kept with the mechanism that closes each route so the machinery outlives the framing. Per the corpus’s own doctrine (project memory feedback_invent_dont_audit): obstructions below are coordinate-relative, and each entry names exactly which coordinate or proof-template it excludes, not the underlying object.

Recently published declarations

This subsection catalogues material that entered the public record after the rest of this paper was drafted: declarations union-merged into modules that were already public (SignedQMomentObstruction, GenericTailOrbitRigidity, DiagonalFreshLossBridge, SquaredMersenneDiagonalEnclosure, ActualForeignResidueProjection, DyadicPrefixCompression, RepunitMobiusNumerator, GeometricCoprimality, LcmDiagonalReduction, PivotAntiReconstruction, all in Erdos249257/), and the newly published per-problem tree ErdosProblems/Erdos249/. Every declaration below was read directly from source; none is inferred from a name. Several of these files contain long chains of “XSupply \(\to\) irrational” implications whose hypothesis is an unproved cofinal predicate. Per the standing rule of this paper, those chains are named as exactly what they are — reductions, not results — and are not restated as if they narrowed the open problem. The module SquareCRTCube is deliberately excluded: its private additions did not compile even in the private tree and were reverted, so nothing from it beyond the existing public file is cited here.

Checked negative result: no free promotion from bounded to cofinal

A ladder like the one above invites an obvious question: is any scale:bounded result actually uniform in disguise, so that removing its threshold is a routine generalisation rather than new mathematics? This was checked directly rather than assumed. An audit read the Lean proof body behind every bounded-scale result in the #249 corpus — eighteen candidates in total, spanning the near-miss list against the #249-supply obligation catalogued in the interface index (fourteen rows, each independently checked against the exact cofinal target it is closest to) together with the remaining bounded/fixed rows in the certificate, Möbius–Lambert, and actual-orbit banks above — and found no bounded result whose proof is uniform enough in its threshold parameter to promote to cofinal or uniform for free. Every candidate failed for one of three reasons, and the failure mode is worth recording because it is a checked negative result, not an absence of search:

1. Finite certificate tables. Results such as (28 explicit values of \(t\) through \(t{=}64\), now a strict subset of the aggregate \(\forall t\le82\) band), (\(h\in[1,8]\) at fixed depth 16), and (\(h\in[1,16]\) at exponent 14) are each a finite list of independently verified rows, not a single argument instantiated at a free parameter. There is no uniform proof underneath to strip the bound from; each new row is a fresh finite computation.

2. interval_cases/decide over a bounded range. Results such as (\(a{\ge}8\)) and the entire /top-edge-staircase family (room conditions of the shape \(J{+}(a{+}6){<}2\cdot2^a\)) are proved by case-splitting a residue or a divisor structure that is only exhaustively enumerable inside the stated range; the mathematical content genuinely narrows as the range widens, so decide cannot simply be re-run at a larger bound without an exponential blow-up in the search space it certifies.

3. Constants that degrade with the parameter. The clearest instance is the echo-versus-height wall (prose:echo_versus_height_two_front_wall, §5e–5f of the ambitious-modular-route note): height-optimal ladder families pay quadratic height \(P(1)\sim 2^{K^2/2}\) matching ’s own growth rate, while height-minimal integer-relation minimizers regrow the echo term \(E_R\) to match — for every tested family, the two costs cannot both be driven to zero as the scale parameter grows. The interface index records the same phenomenon for HalfRung\((J)\)-shaped truncation rungs: the certificate window \(B(J)\) is driven by \(L_J=\mathrm{lcm}(2,\dots,J)\), which grows super-exponentially in \(J\), so the per-\(J\) constant degrades with the very parameter the cofinal claim needs to range over — “the hallmark of a proof that does not survive bound removal” (interface index, row d-3a/d-3b).

None of the fourteen near-miss rows against the #249-supply obligation is closed by a scale argument alone either: reading each one’s own recorded exact_mismatch shows the residual gap is a missing arithmetic input (a constant-saving Weyl-sum bound for e1-companion; a one-sided top-edge residue gap for TE-04/TE-05-weakest), never a generalisable proof technique sitting one omega call away from cofinal. The one row where the source tag itself is imprecise — SGN-01, marked scale:bounded even though its underlying exponent \(a\) is unbounded, see \(^\dagger\) above — is precisely the kind of false positive the audit was built to catch, and even there what remains open is the other half of the certificate band (the top-edge residue), not a scale defect in SGN-01 itself.

Obstructions are coordinate-relative: the binary-digit vs. Möbius–Mersenne case

The clearest instance of coordinate-relative obstruction in the whole #249 corpus is the fate of the classical Erdős (1948) near-integer digit method. That method needs, in essence, a finite automaton: a bounded amount of state carried forward from one digit block to the next, so that the value of a far-away digit block can be recovered from a bounded summary of everything before it. In the binary-digit coordinate this is exactly what fails, and it fails as a proved Lean theorem, not a heuristic remark: shows that for a balanced-pulse family of radius \(m\), any finite State type collapsing the family to a single autonomous summary must satisfy \(|\mathrm{State}|\ge\lfloor m/2\rfloor+2\) — unbounded in \(m\) — so no finite-state decoder can recover the shift \(r\) from its collapsed state ([Lean], scale:uniform, coordinate binary-digit). This is the formal shadow of the elementary facts that \(0\le\varphi(n)\le n\), that \(\varphi\) is unbounded, and that \(\varphi\) has average order \(\tfrac6{\pi^2}n\), equivalently \(\sum_{k\le x}\varphi(k)\sim\tfrac3{\pi^2}x^2\) ([Math]), rather than any false pointwise estimate \(\varphi(n)=\Theta(n)\): the digit-window discrepancy windowDiscrepancy\(\,h\,N\,L\) genuinely needs \(\Omega(m)\) bits of state to track as \(N\) grows, which is exactly why #249’s own binary-digit engine is forced into a cofinal certificate supply () rather than a single finite-state argument: the same shape of no-go recurs at (locked gauge defeats residual-blind rank certificates for the first-harmonic pivot) and at (the dyadic totient-kernel span is genuinely infinite-rank, not compressible to any fixed dimension).

The Möbius–Mersenne coordinate does not carry this obstruction, because it is built on a coefficient sequence, \(\mu(d)\in\{-1,0,1\}\), that is bounded rather than growing with \(d\). The squared-Lambert transfer engine takes any weight with \(|w(d)|\le d\) — \(\mu\) trivially qualifies with room to spare — and converts it into a divisor-convolution power series for free; no finite-state decoder is ever needed because the relevant recursion (the cyclotomic T1–T6 chain: through ) is a finite, exact polynomial identity at every squarefree radical \(r\), uniform in \(r\), with no growth-driven state explosion. This is precisely why the corpus’s strongest unconditional denominator result — the exact-value and lower-bound formulas of and — lives entirely in the Möbius–Mersenne coordinate and is scale-uniform, while the sharpest conditional route in the binary-digit coordinate is scale-cofinal and unclosed. The two coordinates are not equivalent representations of the same difficulty: the wall each one hits is a fact about that coordinate’s own state-growth, not about #249 itself, which is exactly the AP17/AP18 discipline this corpus was built to enforce — before reporting an obstruction, name the coordinate it was measured in, and test whether a re-representation removes it.

Reading this index

Every entry follows the same discipline. Yields: the exact statement proved, with quantifiers in their proved order. Exact mismatch: precisely where the proved statement falls short of the open obligation it is compared against — never “it doesn’t work,” always the named axis of shortfall. What would close it: the exact remaining proposition, stated in full, whose proof (via the cited Lean consumer, already on disk) proves \(\mathrm{Irrational}(S)\).

Each numbered claim carries three tags. scale:fixed means proved at finitely many explicit numerals with no argument in the growing parameter; scale:bounded means proved on a bounded range of a parameter that is itself unbounded elsewhere in the statement; scale:uniform means proved for every value of the relevant parameter (the strongest positive tag short of matching the open target); scale:cofinal means the statement itself has the shape \(\forall a_0\ \exists a\ge a_0\), i.e. it is exactly the quantifier shape the open obligation needs; scale:n/a applies to structural non-existence results with no growing parameter. The evidence tags are [Lean], [Cert], [Math], [Cited], [Open], used exactly as defined in Part I.

The canonical open obligation for #249, proved in Part II to be sufficient (), is the 249-supply obligation: \[\forall h \ge 1,\ \forall N_0,\ \exists N \ge N_0,\ \exists L,\ \mathtt{certifiedKill}\ h\ N\ L .\] Fourteen near-miss rows are catalogued against it below: one headline row (the sharpest reduction in the corpus, given its own subsection) and thirteen further rows, each attacking the same obligation from a different coordinate.

The headline: #249 reduces to a single unsupplied exponential-sum bound

The following two definitions, verified against the live Lean tree in this session, are the sharpest statement of the #249 frontier that the corpus contains.

Row-by-row: the remaining near misses against 249-supply

The headline (§\(\ref{ssec:headline}\)) is row e1-companion of the source interface catalogue in full. The remaining thirteen rows below attack the same 249-supply obligation from independent coordinates in the Lean tree: the actual-LCM sign corridor, the top-edge staircase, the raw rational approximant, the short-window arithmetic word, the diagonal pincer certificate bank, the \(h\)-uniform single-window certificate, the Farey/continued-fraction denominator growth law, the 2-adic pulse block, the LCM-jump slack scalar, the prime-jump commutator, the Möbius–Mersenne denominator channel, and the carry-kernel rank. None of them is closed; each is recorded with its exact remaining content.

Synthesis: where the frontier actually is

Collecting the fourteen rows, three facts stand out as loci for future effort, stated with the same precision as the rows themselves rather than as summary rhetoric.

First, the single closest approach to 249-supply is the first-harmonic reduction of §\(\ref{ssec:headline}\): a constant-saving (\(21/25\) or \(9/10\)) exponential-sum cancellation estimate, with a satisfiable room condition and, via the subset consumer (Theorem \(\ref{thm:hgap-subset}\)), no requirement that the saving hold on a full interval or a positive-density subset. This is the only row in the index whose remaining content is recognisably a single classical estimate rather than a compound arithmetic-geometric statement.

Second, the top-edge staircase (TE-04 through TE-05-weakest, coord:actual-lcm-top-edge) is the only row where the corpus has both halved the obligation (one-sided instead of symmetric) and exposed, via the exact identity of Observation \(\ref{obs:staircase-tension}\), precisely which of two logically symmetric escape branches survives the sign machinery already proved elsewhere in the same file family. That five strictly weaker equivalent or sufficient forms are already proved inter-derivable (Proposition \(\ref{prop:te-chain}\)) means effort here is not fragmented across restatements: proving any one closes the others automatically.

Third, the d4/d5 rank obligation is structurally independent of the residue-coordinate rows above: it is a second, self-contained sufficient condition for #249 (an upper rank bound contradicting the proved \(2^e{-}1\) lower bound), in a coordinate (carry-kernel rank) where a natural finite-rank strengthening is already proved impossible. A rank upper bound, if found, would not need to route through \(\mathtt{certifiedKill}\) at all.

No row in this index is a solution, a partial solution in the sense of resolved cases, or evidence that #249 is likely true or false. Every open producer listed is exactly as open as the original Erdős–Borwein question it reduces to; what the index adds is the exact remaining content, verified against the live Lean tree, of each reduction.

Meta-level: finite inspection cannot certify the supply (the \(\gamma\)-splice remark)

(a) Route as conceived. Every unconditional route to #249 in this corpus bottoms out in a certificate-supply obligation of the shape \(\forall h\ge1\,\forall N_0\,\exists N\ge N_0\,\exists L,\ \mathrm{Sep}(h,N,L)\) (, the exact open-obligation form quoted throughout the existing manuscript). A natural hope is that verifying \(\mathrm{Sep}\) — or its diagonal specialisation — at every scale up to some large, explicit bound \(B\) is evidence that the supply holds, and that pushing \(B\) far enough would eventually amount to a proof.

(b) Exact mechanism that closed it. The manuscript’s own remark ([Math], prose-only, not formalised in Lean: §5.4, “finite inspection cannot establish the supply”) gives an explicit splice construction. Take any coefficient stream \(\gamma:\mathbb N\to\mathbb N\) that agrees with \(\varphi\) on every index \(\le B\), and alter \(\gamma\) at one residue class beyond \(B\) so that the resulting binary series \(\sum\gamma(n)/2^n\) is forced rational. Such a \(\gamma\) exists for every \(B\) (this is the same coboundary-splice technique that produces §\(\ref{sec:parity-countermodel}\)’s parityCoboundaryWeight witness, generalised: insert a lacunary zero-valued coboundary edit \(2/2^m - 4/2^{m+1} = 0\) at some \(m>B\)). Because \(\gamma\) agrees with \(\varphi\) on every index \(\le B\), \(\gamma\) passes every finite certificate that only inspects indices \(\le B\) — in particular every instance of \(\mathrm{Sep}(h,N,L)\) with \(N+L\le B\) that \(\varphi\) itself passes or fails. Yet \(\sum\gamma(n)/2^n\in\mathbb Q\) by construction.

(c) Precise scope. This is a statement about proof method, not about \(\varphi\): it does not touch \(S\) at all. What it excludes is the inference “\(\mathrm{Sep}\) verified up to bound \(B\), for arbitrarily large \(B\), therefore \(\mathrm{Sep}\) holds cofinally.” The scope is exactly \({\small\textsf{scale:bounded}}\) versus \({\small\textsf{scale:cofinal}}\): any finite-B verification, however large, is compatible with both outcomes, because a rational stream can be built to survive any fixed inspection horizon. It says nothing about whether \(\varphi\) itself is such a \(\gamma\) — only that no finite-horizon check can distinguish \(\varphi\) from a \(\gamma\) that is.

(d) Salvage. The splice construction is exactly the mechanism underlying §\(\ref{sec:parity-countermodel}\)’s Lean-formalised countermodel below, so its content is not lost even though this specific remark is unformalised: everywhere a proof strategy in this corpus proposes to certify a supply by exhaustive finite search (the diagonal deposits at \(t\in\{1,\dots,64\}\), ; the row-200,000 sqrt-escape census on the #257 side), this remark is the standing reason such a search, however large, is evidence and not proof. [Math] scale:n/a coord:binary-digit.

The parity-aperiodicity countermodel (TotientParityCoboundaryCountermodel)

(a) Route as conceived. A natural strengthening of #249 attempts: show that any coefficient word \(c:\mathbb N\to\mathbb N\) that (i) is uniformly bounded, (ii) satisfies the trivial linear-growth bound \(c(n)\le n\), (iii) matches \(\varphi(n)\bmod 2\) exactly, and (iv) is not eventually periodic — even strengthened to cofinally, arbitrarily separated, arbitrarily long blocks of non-periodicity — must have irrational binary series \(\sum c(n)/2^n\). This is the natural target for anyone trying to use only \(\varphi\)’s coarse parity/aperiodicity profile.

(b) Exact mechanism. The construction \(\mathtt{parityCoboundaryWeight}(n) := \mathtt{parityBaseWeight}(n) + 2\cdot\mathtt{largePowerTwoBit}(n) - 4\cdot\mathtt{largePowerTwoBit}(n-1)\), where \(\mathtt{parityBaseWeight}\) is the eventually-constant word \(0,1,1,2,4,4,4,\dots\) and \(\mathtt{largePowerTwoBit}(n)=1\) iff \(n=2^{k+3}\), is a lacunary zero-valued coboundary splice on top of an eventually-constant base. The strongest of five landed theorems,

(sum computation ; non-periodicity ; exact parity match ). [Lean] scale:cofinal coord:binary-digit.

(c) Precise scope. This is an object-level existence witness (\(c\ne\varphi\), only \(c\equiv\varphi\pmod2\)) that closes a proof-route: it proves that the hypothesis set \(\{\)bounded, linear growth, \(\varphi\)-parity match, non-eventual-periodicity\(\}\), no matter how strongly the non-periodicity clause is strengthened (up to the arbitrarily-separated arbitrarily-numerous form above), can never entail irrationality of the associated binary series, because \(c\) satisfies every hypothesis and is rational. It says nothing about \(\varphi\) itself — the witness sequence \(c\) is a different, hand-built sequence. Any future sufficient-condition candidate stated purely in terms of \(\{\)coefficient boundedness, growth, parity, periodicity\(\}\) must be checked against this countermodel before being trusted, for either #249 or #257.

(d) Salvage. The lacunary coboundary-splice technique itself — inserting zero-valued edits \(2\cdot2^{-m}-4\cdot2^{-(m+1)}=0\) at sparse ranks to destroy periodicity while preserving the rational sum — is a fully general recipe for building rational-valued, non-eventually-periodic, bounded coefficient sequences matching any parity template, and is literally the mechanism instantiated informally in Theorem \(\ref{thm:gamma}\)’s \(\gamma\)-splice construction. It is also a ready-made stress-test fixture for any future parity-based sufficient condition proposed anywhere in the corpus. Confirms the corpus-wide lesson (project memory feedback_erdos_reductions_rejected_bank_real_results): only arguments using actual quantitative totient/Mersenne size or residue information — as in the TotientActualLcm*, TotientFixedRank* families below — can possibly close #249; pure symbolic-word arguments cannot.

Two scoped #249 no-go countermodels: square-CRT correction suppression is ambiguous

(a) Route as conceived. The totient prime-dilation cocycle \(\varphi(pm)=(p-1)\varphi(m)+[p\mid m]\varphi(m)\) carries a correction term whenever \(p\mid m\). A natural strategy imposes a square congruence \(n\equiv A+pa\pmod{p^2}\) with a “clean” shift \(h\) (\(p\nmid a+h\)) to suppress that correction on a finite horizon, then hopes that correction-suppression (“cleanliness”) is itself enough to guarantee that the resulting finite-difference cube is nonzero — i.e. that cleaning away the correction term automatically leaves behind a genuine, nonvanishing arithmetic signal usable in a curvature argument.

(b) Exact mechanism that closed it. Two explicit, opposite finite computations refute the hoped-for entailment simultaneously:

• Vanishing witness. The smallest returned countermodel has the entire two-step finite block \(\mathtt{actualOneCubeCoeff}\) equal to zero at \(n=52\), \(r_0=13\), \(r_1=13/18\) (, kernel-decided; cleanliness witnessed by ).

• Nonvanishing witness. A separate, nearby clean configuration at \(n=27\) has the same block nonzero (; cleanliness witnessed by ).

Both witnesses are exhibited alongside the positive achievability result (a bounded common base satisfying prescribed CRT anchors/residues does exist). [Cert] (theorem bodies not independently re-verified beyond signatures and docstring — flagged DOCSTRING-SOURCED in the source bank) scale:fixed coord:other:square-crt-cocycle.

(c) Precise scope. These are two #249-scoped countermodels — the coordinate is the totient prime-dilation cocycle specifically, not a problem-agnostic phenomenon. Together they show that correction-suppression is logically independent of the sign/nonvanishing question it was hoped to settle: “clean” (i.e. correction-free) is consistent with both outcomes. This is a statement about a specific finite-difference construction (the representation), not about \(\varphi\): it does not exclude a nonvanishing finite-difference cube in general, only the inference from cleanliness alone to nonvanishing.

(d) Salvage. The general cocycle identity \(\varphi(pm)=(p-1)\varphi(m)+[p\mid m]\varphi(m)\) () and the CRT-witness apparatus (, ) remain fully reusable for any residue-forcing construction, in any coordinate. More valuably, the abstract cube-cancellation lemma extracted from the same file, — “if inserting one coordinate never changes the value of \(f\), the alternating powerset sum of \(f\) vanishes” — is completely divorced from totient/CRT content and is directly reusable for any Hilbert-cube or higher-difference argument on either problem. What remains as the honest open gap: an independent anti-concentration or residue-producer argument for why the clean residual does not vanish, which this module explicitly does not supply.

The adelic height obstruction

(a) Route as conceived. Several proof strategies attempt to clear an unwanted denominator factor from a rational value \(x\) by multiplying by a small integer coefficient \(c\), hoping to discard the complementary denominator information entirely (e.g. localising a diagonal tail difference to one LCM ray channel while dropping the rest).

(b) Exact mechanism.

. The equality strengthening, \(\exists t:\mathbb Z,\ H\cdot c\cdot x = t\cdot x.\mathrm{num}\), is . The Mersenne-scale corollary — for positive \(x\), if \(2^r\mid x.\mathrm{num.natAbs}\) and \(x<2/(2^n-1)\), then \(2^r(2^n-1)<2\cdot x.\mathrm{den}\) — is (generic form ). A companion rigidity fact rules out smuggling the discarded information back in through a linear channel: if a linear map \(\Lambda:V\to W\) factors through a surjective evaluation \(\mathrm{ev}\) (\(\ker\mathrm{ev}\le\ker\Lambda\)), then \(\Lambda\) is exactly \(\mathrm{ev}(\cdot)\bullet w_0\) for a single fixed \(w_0\) — . The upstream primitive these import, and , gives the exact survival/cancellation law: a divisor \(m\mid D\) of a displayed denominator survives reduction of \(a/D\) iff \(m\) is coprime to \(a\); after scaling the numerator by \(h\), a surviving coprime divisor \(C\mid D\) shrinks to exactly \(C/\gcd(C,h)\), never further. [Lean] scale:uniform coord:other:rational-height.

(c) Precise scope. This is pure \(\mathbb Q\)-arithmetic with zero Mersenne or totient content — it is not a statement about \(S\) at all, but about any rational-height bookkeeping argument. Its exact content: scalar denominator-clearing never erases the complementary denominator; it moves that complement into the coefficient’s (Archimedean) size. Any construction that tries to shrink a displayed denominator down to one surviving channel pays for it in coefficient growth. This directly explains why denominator-compression strategies are structurally hard: the Mersenne-shadow denominator lower bound \(2^{t/2}\le\prod_{p\in\mathrm{upperHalfPrimes}\,t}\mathrm{mersenne}(p)\) () forces a quadratic-in-scale coefficient cost via this lemma if one tries to localise to a single channel.

(d) Salvage. Fully problem-agnostic and directly reusable for #257 or any other Lambert-type denominator-survival argument as-is. It is the general mechanism underlying the corpus’s Farey-gap denominator-exclusion family (Part C of the certificate bank, , the strongest current unconditional statement about \(S\): if \(S\) is rational its reduced denominator exceeds \(79{,}639{,}646{,}646{,}701{,}375{,}323{,}355{,}774{,}875{,}831{,}053\approx7.96\times10^{34}\)).

The signed \(q\)-moment machinery — a positive tool, not an obstruction

(a) Route as conceived. A “signed Hankel determinant” / Hermite–Padé style route to #249 would exhibit a finite signed linear combination of dyadically-cleared totient terms and show it is provably nonzero, giving a nonvanishing certificate for a first-harmonic or Möbius-companion construction.

(b) Exact mechanism (a nonvanishing engine, not a no-go).

, built from a fully generic rectangular Cauchy–Binet-style determinant-of-product expansion (definitions and ). [Lean] scale:bounded coord:p-adic.

(c) Precise scope — the point this section exists to make. Despite living in a file named alongside the corpus’s “obstruction” modules, this is explicitly not phrased as a no-go in its own docstring: it is the finite nonvanishing engine that a Hankel–Padé construction for #249 would consume. The parity lemma and the Cauchy–Binet expansion use no totient or Mersenne structure at all — pure linear algebra, fully problem-agnostic, directly transplantable to any base-\(q\) dyadic-clearing argument including #257’s series family. What is missing, and what prevents this from closing anything, is a supply theorem: no result in the corpus proves that a unique-terminal configuration of this shape exists cofinally for the totient-derived family. The obstruction, such as it is, is not in this lemma but in the absence of its hypothesis’s cofinal supply — exactly the same shape of gap as §\(\ref{sec:mahler-defect}\)’s Mahler defect below.

(d) Salvage. The entire lemma is reusable machinery, not wreckage — nothing here needs salvaging because nothing here failed. It stands ready for whichever future construction can supply the missing cofinal unique-terminal-configuration existence.

The residual-gauge obstruction

(a) Route as conceived. A “first-harmonic pivot” strategy for #249 (via exponential/character-sum cancellation, ) might try to certify a nonzero determinant or full-rank minor of a residual-weighted monomial matrix as sufficient evidence that a genuine phase reconstruction (as opposed to a degenerate locked configuration) has occurred.

(b) Exact mechanism.

(row-dependent relaxation ; the column-gauge identity underlying it, \(\det(\mathrm{residualMonomialMatrix}) = \det(\mathrm{phasePowerMatrix})\cdot\prod_j W(j)\), is ; a row-dependent relaxation still fails at ). [Lean] scale:uniform coord:other:first-harmonic-phase.

(c) Precise scope. Pure linear algebra over \(\mathbb C\), fully generic in dimension \(d\) and exponent function \(e\), zero #249-specific content — this is a statement about residual-weighted monomial matrices as a representation, not about the totient object. It rules out exactly one class of certificate: a residual-blind rank/determinant/ conditioning test, used alone, cannot distinguish genuine phase reconstruction from an explicit “locked” degenerate configuration in which a residual weighting scales every column by \(W(j)=z(j)^{-1}\), collapsing the exponent-one row to the constant row \((1,\dots,1)\) while the determinant stays nonzero whenever the base (Vandermonde-shaped) \(\mathrm{phasePowerMatrix}\) determinant is nonzero. It does not rule out determinants carrying an additional arithmetic coupling identity between rows.

(d) Salvage. A hard requirement for any future first-harmonic determinant construction (Part E of the certificate bank, ): the construction must couple rows by an extra arithmetic identity, not merely gauge-normalise columns. The diagonal-gauge-action technique itself is reusable for any determinant-based nonvanishing strategy in any coordinate.

Cone flatness and cone nonflatness

(a) Route as conceived. The diagonal certificate-supply obligation () concerns only the pair \((H,2H)\) at LCM height \(H=\mathrm{periodLcm}(t)\). Two natural strengthenings: (i) show rationality of \(S\) is even more constrained than a single diagonal pair — it flattens an entire cone of ratios; (ii) conversely, exhibit nonflatness on a wider “menu” of cone vertices as a cheaper sufficient certificate than a single pairwise \(\mathrm{certifiedKill}\).

(b) Exact mechanism — flatness (necessary consequence of rationality).

(body LcmConeFlatness.lean). [Lean] scale:uniform (for all sufficiently large \(t\), given rationality) coord:other:lcm-ray-totient. Rationality forces one fractional constant on the entire LCM cone \(\{k\cdot\mathrm{periodLcm}(t):k\ge1\}\) at every scale \(t\ge t_1\), not merely the single diagonal pair — the umbrella collapse theorem shows any \(\mathrm{certifiedKill}\) anywhere on the two-multiplier cone, at arbitrarily large \(t\), forces \(\mathrm{Irrational}(S)\).

(b\('\)) Exact mechanism — nonflatness (a sharper sufficient certificate).

(supply theorem ). [Lean] scale:bounded (proved for a given finite menu \(Q\); an unbounded-scale menu is the open sufficient target) coord:other:lcm-ray-totient.

(c) Precise scope. Flatness is a genuine necessary consequence of rationality — it is a statement about what rationality of \(S\) would force, conditional on rationality, not an unconditional fact about \(S\). Nonflatness is an unconditional sufficient certificate mechanism, information-theoretically half the depth floor of the pairwise \(\mathrm{certifiedKill}\) (one-sided versus two-sided radius charging), but it has been proved only for individual finite menus \(Q\); no menu of unbounded scale has been supplied. Neither direction decides #249: flatness gives a contrapositive route (exhibit any cone nonintegrality at arbitrarily large \(t\) and rationality is refuted) and nonflatness sharpens the certificate needed, but the underlying producer obligation — a nonintegral tail difference at cofinally many scales — is unchanged. Note also the coordinate warning from the manuscript’s own Appendix C (): cone flatness is a necessary consequence, and only the sharper diagonal-pincer / full-target-avoidance normal forms (, ) are an exact \(\mathrm{iff}\) with irrationality.

(d) Salvage. The argmin/Helly-avoidance combinatorial-geometry technique behind cone-nonflatness is a reusable pattern for any modular-residue pincer argument with more than two points, in any coordinate. The rank-2 second-difference certificate family built on the same window apparatus was independently tested and found not to be a shortcut over rank 1 (measured, not merely conjectured: at \((h,N)=(1,8)\), rank-1 fires at depth 8 while no rank-2 certificate exists at depth \(\le8\); ) — an explicitly flagged dead end not to re-attempt without new information.

The Mahler defect: dyadic totient-kernel finite rank per level, infinite rank overall

(a) Route as conceived. A finite-linear-algebra shortcut to #249: find a bounded-depth linear relation among the dyadic totient-kernel channels \(n\mapsto\varphi(2^jn+r)\) that would compress the infinite family to a finite-dimensional space, from which a rationality-forcing contradiction (or a genuine rank obstruction) might be extracted.

(b) Exact mechanism.

; consequently the full infinite family spans an infinite-dimensional \(\mathbb Q\)-space, . A companion impossibility result closes the natural repair attempt directly: a bounded compressed-adjoint certificate — a triple \((Q,A,\mathrm{boundary})\) with \(Q\cdot v\cdot A=\mathrm{boundary}\), \(|\mathrm{boundary}|<Q\cdot v\), \(A\ne0\) — is provably impossible, . [Lean] scale:uniform (holds for every \(e\); existence side is unconditional, via Mathlib’s CRT + primes-in-AP machinery) coord:binary-digit (dyadic totient-kernel — not the Möbius coordinate).

(c) Precise scope — coordinate-relative, stated explicitly by the source module. This does not show irrationality of \(S\). It proves the dyadic-kernel side is infinite-rank; the module’s own docstring names the missing input as “a rationality-side finite-rank compression, or equivalent contradiction.” The companion necessary-consequence-of-rationality theorem, \(\neg\mathrm{Irrational}(S) \implies \exists v>0,\exists U:\mathbb N\to\mathbb Z,\ \mathrm{IsTemperedBinaryOrbit}(\varphi,v,U)\wedge\forall e,\ 2^e-1\le\mathrm{finrank}_{\mathbb Q}\,\mathrm{span}(\mathrm{range}( \mathrm{canonicalCarryKernelFamily}(U,e)))\) (), shows the SCALE side is finished — the \(2^e-1\) floor holds for all \(e\) with a uniform proof — but the opposite inequality (a rationality-side rank upper bound) is exactly what is missing, and its absence is the entire open content here. A third, independent coordinate exhibits the same coordinate-relative phenomenon: the Möbius-incidence companion matrix \(U_N(i,j)=\mu((i+1)/(j+1))\) if \((j+1)\mid(i+1)\) else \(0\) is lower triangular with diagonal \(1\), hence \(\det U_N=1\) for every \(N\), hence its jet-evaluation map is injective — a finite “incidence quotient” compression is impossible at any finite horizon in the Möbius coordinate too (). Both natural finite truncations — dyadic-residue and Möbius-incidence — turn out to have no nontrivial kernel, in two completely different coordinates. That is strong evidence any winning finite-linear-algebra shortcut, if one exists, must live in a genuinely third coordinate or use an infinite/growing-parameter construction, not evidence that no shortcut exists at all.

(d) Salvage. and are fully generic finite-rank linear-independence infrastructure — the indexed family is a free variable, reusable for any finite-rank obstruction argument on either problem (e.g. testing independence of Mersenne-indexed sequences for #257 via an explicit nonzero minor). The CRT+Dirichlet evaluation-forcing technique (make one channel prime, force every other channel through a fresh arithmetic-progression prime) is a reusable construction pattern independent of the totient specifics.

Further closed routes, catalogued for completeness

The following additional no-gos and route-pruning results were read in full and are recorded here in compressed form; each follows the same (a)/(b)/(c)/(d) discipline as above but is presented as a table row for space.

One identity, and what it does to every surviving route

Write \(S=\sum_{n\ge 1}\varphi(n)/2^n\), \(R_N=\sum_{m\ge 1}\varphi(N+m)/2^m\) for the local tail (), and \(\Phi_N=\sum_{n\le N}\varphi(n)2^{N-n}\in\mathbb{Z}\) for the integer prefix, so that \(2^N S=\Phi_N+R_N\). For \(h\ge 1\) set \[\alpha_h \;:=\; (2^h-1)\,S .\]

The second identity and the character form are landed: and . The recurrence \(R_{N+1}=2R_N-\varphi(N+1)\) is one line from the definition and is used below only for intuition [Math].

This is not a new fact — it is two landed Lean theorems read together — but reading them together has a consequence the corpus never draws. The first-harmonic block sum, which is the analytic frontier of #249, is a lacunary exponential sum in a single real variable. The following proposition makes the transfer exact, including the truncation budget.

[Math] . The proof uses only landed lemmas; formalising it is a variant of with the constant \(21/25\) replaced by the real-part constant \(89/100\) and the room factor \(16\) by \(1024\). Nothing here is an improvement of the analytic requirement; it is a change of coordinate that makes the requirement legible.

[Math]. This threshold is worth staring at. A single digit change in every ninth position, in one block per scale, for each fixed \(h\), would settle Erdős #249. What is actually true, numerically, is far stronger.

Route 1: a constant-saving cancellation over a dyadic block

Route 2: the four-term pivot budget

Route 3: uniform quantitative escape at primes

Route 4: depth-locked full-depth escape

Route 5: the rationality-side rank bound remains open