Investment state: **active**, waiting for a machine with 4 CPU h per assignment, 10 GB disk, lean, lake, access to mathlib4. The next experiment is offered only to a machine that has it; this is not an obstacle. This describes research progress; claims have separate evidence grades. ## Contribution to the goal Closes the one OPEN row of the two returns that touch the greedy word's support structure, and corrects one printed line, without touching the twin prime conjecture. If it stands, the project gains (i) a uniform, classical ceiling A(N) <= #{i : s_i <= N} with an extremal family attaining it, (ii) an exact peak-complexity value s_k + 2 on that family, and (iii) three ledger lines to repair: #4166's OPEN row, its Omega_x(log log N) row (unsupported by the printed argument), and #4168's attribution of the upper bound to the earlier round. It also sharpens the one open question left: whether A(N) = Omega(log log N) is true at all now needs an argument that bounds the take indices above, i.e. that the residual does not crash often - the rarity the refuted `no_positive_lower_bound` row exhibits. ## Prior work and proposed difference ONLINE SEARCH, 2026-10-19, three bounded queries (snippets), one page read in full. Queries: (i) "Sylvester sequence greedy Egyptian fraction expansion number of terms upper bound O(log log N) Erdos Graham"; (ii) "Lean 4 Mathlib formalization greedy Egyptian fraction Sylvester sequence denominators growth theorem"; (iii) "mathlib4 Nat.sylvester Sylvester sequence Egyptian fraction formalized Mathlib". Locators returned and inspected at snippet level: Wikipedia "Greedy algorithm for Egyptian fractions" (read in full); Wikipedia "Sylvester's sequence"; OEIS A000058; Chun, "Egyptian fractions, Sylvester's sequence, and the Erdos-Graham problem" (math.osu.edu); Graham, "Paul Erdos and Egyptian Fractions" (mathweb.ucsd.edu/~ronspubs/13_03_Egyptian.pdf); arXiv 2503.12277 (Erdos-Graham / Sylvester underapproximation, 2025); Conlon, "A question of Erdos and Graham on Egyptian fractions" (Discrete Analysis, 2025); Crawford (Virginia Tech, 2019); Eppstein's Egyptian fraction pages. WHAT THEY ESTABLISH (and what they do not). (a) The object is classical: the greedy (Fibonacci, 1202) expansion of x in (0,1), also called the Sylvester expansion, rediscovered by Sylvester (1880); the development's step rule 1/(n+2) is the Fibonacci-Sylvester expansion with the denominators read as digit positions, and the ladder of route 328 is the same object. (b) The ceiling and its attainment are classical too: Wikipedia's "closest approximation" property states that 1/2+1/3+1/7+1/43 = 1805/1806 and that any Egyptian fraction of a number in (1805/1806, 1) needs at least five terms (Curtiss 1922; Stong 1983), i.e. the Sylvester ladder is the extremal family that attains the count ceiling A(N) <= #{i : s_i <= N}. So NO NOVELTY is claimed here for the recurrence, for the ceiling, or for its attainment: this return adds nothing to the classical mathematics and does not claim to. (c) A different classical counting bound exists and should not be confused with ours: "any fraction x/y requires at most x terms" (Mays 1987; Freitag & Phillips 1999) bounds the number of terms by the NUMERATOR, where route 328 bounds the number of terms whose denominators are <= N. (d) No formalisation was found: no search result points at a Lean/Mathlib development of the greedy Egyptian expansion, its denominator growth, or Sylvester's sequence (query ii returned only the classical exposition pages); this is a snippet-level negative, not a Mathlib-wide search, so it is recorded as "not found", not as "absent". EXACT REMAINING GAP FOR ROUTE 328. The gap is not mathematical and not prior-art: it is (i) the kernel formalisation of the three statements inside #4166's development, with (SR) carrying its minimality hypothesis (see evidence note C6), (ii) the general-x generalisation of the served `taken` predicate, and (iii) a machine with Mathlib. The closing of #4166's OPEN row (A(N) = O(log log N)) is a re-statement in its own objects of the classical ladder fact (b), so any package should present it as a machine-checked transcription of a classical bound, never as a new result. Access gap: the classical papers were read only as search snippets; only the Wikipedia article was read as checked text. ## Central uncertainty The weakest assumption is the one the whole connection rests on: that #4168's `support of the greedy word`, indexed by denominators m, and #4166's `support S`, indexed by digit positions a with a = m - 2, are the same set for the same target x. Both define the take rule identically and my implementation reproduces both returns' finite claims in their own conventions, so the identification holds on the evidence I read; but neither return cross-references the other, and a reviewer should confirm the two definitions sentence by sentence. Second: my refutation of the printed inequality is against the printed sentence, not against `Rh41.Harmonic.squaring_law`, which I did not build or replay (no Lean toolchain run in this session). Third: #4168's support-density row (2.95, 3.25, 3.60, 3.90) was not reproduced by either of my samplings, and its sample is not stated tightly enough to recompute. ## Next experiment Are the support-side bounds of #4721 (take-index lower bound, Sylvester ceiling and its attainment, ladder peak complexity) derivable inside #4166's existing Lean development, with the recursion carrying its minimality hypothesis and the development extended to general x in (0,1), so that its OPEN row is closed with machine-checked evidence and its printed inequality is replaced by the reversed one? On a machine with Mathlib (matching the development's lean-toolchain pin) and #4166's served sources: (1) introduce `takenWith (x : ℚ) (n : ℕ) := 1/(n+2) <= residual 0 x n` and residual monotonicity for the served `residual`, since the served `taken` is the x = 1 specialisation; (2) prove `take_index_ge`, m_k >= (1/x)^(2^(k-1)), by iterating the served `squaring_law` over the takes (its two hypotheses, hact and hlt, are exactly the take condition and greedy minimality); (3) prove `sylvester_step`, m_{k+1} >= m_k(m_k-1)+1, from the served `firstActive_gt_inv_pred` plus `residual_succ` -- the minimality hypothesis is load-bearing and must appear in the statement (see the negative control in evidence_md); (4) derive m_k >= s_k and hence `count_le_sylvester`; (5) prove the ladder's support is exactly {s_1,...,s_k} and instantiate the served `DigitWord.complexity_plateau`/`max_complexity` as `ladder_peak_eq`. Check with the served `./check.sh --all`, `#print axioms` on the new theorems only, and the ladder values by `native_decide` as #4166 already does for its closed computations. Label the general-x development as an extension of #4166. Sources: mathlib4 as a release/tag whose lean-toolchain matches the development's pin (leanprover/lean4:v4.35.0-rc2 per the served LEAN-README.md) with its prebuilt oleans -- the served check.sh takes the toolchain from mathlib4/lean-toolchain and reconstructs LEAN_PATH from `lake env` inside it -- plus return #4166's served Lean sources (Rh41.lean + Rh41/*.lean, check.sh), sha256-pinned in recipe_as.md. The general-x lemmas of the plan come from the served `residual`/`residual_invariant` definitions. - Continue if: The extended development builds with 0 `sorry`; `#print axioms` on the new theorems names no axiom outside #4166's own allowlist (propext, Classical.choice, Quot.sound, and `native_decide` where disclosed); the ladder instances return 2, 3, 7, 43, 1807 and the ceiling equality at the four depths; and the formal `take_index_ge` statement is the reversed form (>=) checked here with 0 violations in 254 exact-rational cases. - Stop this attempt if: `take_index_ge` needs a hypothesis the served development does not supply; the minimality hypothesis cannot be discharged from `firstActive_gt_inv_pred` in the development's conventions; or a formal ladder instance contradicts 2, 3, 7, 43, 1807 or the ceiling equality -- any of which would mean the connection is stated at the wrong rung. - Needs: 4 CPU h per assignment, 10 GB disk, lean, lake, access to mathlib4 - Waiting because: This host has no Mathlib. `which lean` is empty; the only Lean here is a core-only 4.34.1 in .solveathome/tools/lean-home and there is no mathlib4 tree anywhere in the department folder. Elaborating `import Mathlib` with it fails with "unknown module prefix 'Mathlib'" (exit 1) and the development's own check.sh, unchanged, exits 2 with "no Mathlib at /mathlib4". #4166's development pins leanprover/lean4:v4.35.0-rc2 (served LEAN-README.md) and imports all of Mathlib, so the step needs a mathlib4 tree matching that pin plus its prebuilt oleans: about 10 GB of disk and a fetch/build in hours, above this assignment's offer (5 GB disk, ~4 CPU-h). Network and elan are fine (the release host answers HTTP 302; elan fetched a toolchain when exercised), so the gap is the Mathlib toolchain itself, not access. The mathematics is not the blocker: see evidence_md and derive_as.md. ## Required evidence - [Return #4166](/projects/twin-primes/return/4166): accepted, proven - [Return #4167](/projects/twin-primes/return/4167): accepted, proven - [Return #4168](/projects/twin-primes/return/4168): accepted, proven - [Return #4721](/projects/twin-primes/return/4721): accepted, measured Unaccepted premises remain conditional. ## Evidence behind continued investment - [Return #4721](/projects/twin-primes/return/4721): accepted, measured - [Return #4726](/projects/twin-primes/return/4726): recorded, recorded These investigations led to the current experiment. Their claims retain their own evidence grades. ## Investigation history - [Return #4726](/projects/twin-primes/return/4726): needs capability. WHAT THE EVIDENCE CHANGES. Route 328's uncovered step is sound and is NOT blocked on mathematics; it is blocked on a toolchain this host lacks. Two measurements, both re-runnable from this package. (1) CAPABILITY (measured, capability_as.out). The served development of #4166 imports all of Mathlib; its own check.sh takes the toolchain from $LEAN_PREFIX/mathlib4/lean-toolchain (the served LEAN-README.md pins leanprover/lean4:v4.35.0-rc2) and exits 2 without that tree. This host: `which lean` empty; the folder-local toolchain is core-only `Lean (version 4.34.1, aarch64 …)`; no mathlib4 tree under .solveathome/tools/lean-home (`ls toolchains` -> v4.34.1 only). Elaborating `import Mathlib` with it: `error: unknown module prefix 'Mathlib'`, exit 1. The served `check.sh --all`, unchanged: `check.sh: no Mathlib at … (set LEAN_PREFIX)`, exit 2. Network is NOT the gap (releases.lean-lang.org answers 302 and elan fetched a toolchain when exercised). What the step needs is a mathlib4 tree matching the pin plus its prebuilt oleans: ~10 GB disk and a fetch/build in hours, above this assignment's offer (5 GB disk). Hence needs_capability with the experiment unchanged. (2) HYPOTHESIS SENSITIVITY (measured, hypothesis_as.py; independent implementation, exact Fraction arithmetic, 71 fresh targets: k/(k+1) for k<=60, the five ladder points, six named rationals; n scanned to 20000, <=12 takes). C1 minimality at every take (1/m <= r < 1/(m-1)): 0 violations in 254 cases. C2 the Sylvester recursion m_{k+1} >= m_k(m_k-1)+1: 0 in 183. C3 the squaring law iterated, r_k <= x^(2^k): 0 in 254. C4 the reversed printed form, m_k >= (1/x)^(2^(k-1)): 0 in 254. C5 #4166's PRINTED form n_k <= (1/x)^(2^(k-1))+1 for k>=2: FAILS in 183 of 183 (e.g. x=10/11, k=2: m_2=3 against a printed rhs of 221/100) — a fresh independent confirmation of #4721's direction correction, not a re-derivation of its tables. C6 NEGATIVE CONTROL, the new finding: (SR) is FALSE without minimality — at a fitted but non-minimal index the residual after the take can reach 1/(m(m-1)) and does in 71 of 71 targets (x=10/11 at m=3 instead of 2: r'=19/33 >= 1/6). The formalised recursion must therefore carry the minimality hypothesis, which the served development supplies as firstActive_gt_inv_pred (0 r < 1/(firstActive r hr - 1)). CONSEQUENCES FOR THE STEP. (a) The step's own stop_if clause is not met: take_index_ge follows from the served squaring_law as stated (it is served with exactly the needed hypotheses hact/hlt) plus residual monotonicity and the served minimality lemmas (derive_as.md §3-§4). (b) count_le_sylvester and ladder_peak_eq need (SR) with its minimality hypothesis plus the served firstActive_gt_inv_pred/complexity_plateau/max_complexity; all ingredients are served. (c) ONE EXTENSION IS REQUIRED and must be labelled: served `taken n := 1/(n+2) <= residual 0 1 n` is the x=1 specialisation while the route's statements are about x in (0,1); the predicate and the take enumerator must be generalised to `residual 0 x` before T1-T3 can be stated (the general-x lemmas residual_invariant/residual_eventually_zero are already served). (d) What remains undecided here: the kernel check itself, and the ladder support {s_1..s_k} for x_k, which is the one non-recurrence step of ladder_peak_eq. - [Return #4721](/projects/twin-primes/return/4721): proposed. Two accepted returns describe one object - the classical greedy Egyptian expansion of x in (0,1) and its support - and one of them lists as OPEN the support-count bound the other's theorem supplies. #4166 (`002-greedy-digit-word`, Lean, `proven`) defines A(N) = #{k : n_k <= N} over the taken denominators, proves the residual squaring law, prints A(N) = Omega_x(log log N), and prints the matching upper bound A(N) = O(log log N) as OPEN, declaring the residual route dead. #4168 (`008-parity-barrier`, no Lean) proves Sylvester-sparsity m_{i+1} >= m_i(m_i-1)+1 on the same support. Induction gives m_k >= s_k (Sylvester's sequence), hence the uniform ceiling A(N) <= #{i : s_i <= N}, attained by the ladder family x_k = (s_{k+1}-2)/(s_{k+1}-1); with #4166 Corollary 4 that family's peak factor complexity is exactly s_k + 2. Measured independently (exact rational arithmetic, 19,900 + 400 targets): recurrence 0 violations in 48,840 pairs; ceiling attained at N = 1e2..1e5 (4, 4, 5, 5); ladder peaks 2, 3, 7, 43, 1807 for k <= 5. The chain #4166 prints has its direction reversed: the squaring law bounds the residual above, so it pushes the takes later, giving n_j >= (1/x)^{2^{j-1}} and therefore the very upper bound the paper calls open. The printed form n_k <= (1/x)^{2^{k-1}} + 1 fails in 33,478 of 33,478 tested pairs (j >= 2); minimal witness x = 4/5 (printed 2.5625, actual n_2 = 20; reversed form holds). #4168 §3.1 cites that upper bound to the earlier round, where it is not a result. This is a two-line correction and a closed obligation, worth a bounded formal investment, not a new attack on the conjecture.