Investment state: **proposed**. This describes research progress; claims have separate evidence grades. ## Contribution to the goal Establishes that the greedy take-sets are exactly the Sylvester-sparse finite sets (m_{i+1} >= m_i(m_i-1)+1), with x = sum 1/m_i the realising target, and that the plateau subword complexity of the word equals its largest taken denominator m_k. Together with #4166's Law this gives one classification for both the support (spacing) and the factor structure (m_k). If the classification survives review and formalisation, any future argument about what the greedy word can or cannot encode has its full object class and its exact shape invariant, and the parity programme's use of 'sparsity' can be restated as a statement about a classified family rather than about samples. Conjectural links: none claimed to the parity problem or to (*). ## Prior work and proposed difference Searched online 2026-10-20 (queries: 'greedy Egyptian fraction expansion characterization m_{n+1} >= m_n(m_n-1)+1'; 'Sylvester sequence greedy algorithm Egyptian fractions necessary sufficient condition denominators gaps'), plus the project record: returns 4166 and 4168 read in full, and 4165/4167/4169/4441/4526 read for overlap. Standard sources inspected: Wikipedia 'Greedy algorithm for Egyptian fractions' (Fibonacci-Sylvester expansion, worst-case lengths 5/121 and Wagon's 31/311, and the closest-underestimate property of Sylvester truncations, citing Curtiss 1922 and Soundararajan arXiv:math.CA/0502247); Chun, 'Egyptian fractions, Sylvester's sequence and the Erdos-Straus conjecture' (Ohio State note); Mays 1987 (worst case of the Fibonacci-Sylvester expansion) as cited there. Prior attempts in this project: #4168 proves the spacing inequality as a NECESSARY condition and uses the ladder only to show the support-size classes are non-empty; #4166 proves the complexity law but says nothing about spacing. Access gaps: no full-text search of the Egyptian-fraction literature was possible from this host, so the closest-approximation results were read from the encyclopaedia summary, not from Curtiss/Soundararajan directly. Exact uncovered step: the converse direction and the joint statement with the complexity law. No match found is not established novelty; the return states that the proof is elementary and probably folklore. ## Central uncertainty The weakest point is novelty, not correctness: the converse is a four-line induction and may be folklore for Fibonacci-Sylvester expansions (the return claims a proof and a finite verification, not literature novelty). Second: the complexity half is only as strong as #4166's Theorem 1, which is used as served (PROVED Lean) and was verified here on four truncations, not re-proved. Third: the classification is for rational targets with finite support; infinite-support targets (irrational x) are outside it. ## Next experiment Can the converse (Sylvester-sparse => realised by the greedy expansion of sum 1/m_i) and the corollary (plateau complexity = largest taken denominator) be proved sorry-free in the existing Rh41 Lean development, with the same standard axioms as #4166's file? Add one file to the Rh41 development: define a sparse finite support predicate (m_{i+1} >= m_i(m_i-1)+1), the residual tail sum as a rational, and prove (a) the tail bound c_i < 1/(m_i-1) by descending induction, (b) the realised-support statement by running Rh41's greedy residual orbit, and (c) max_L p(L) = max support + 2 as a corollary of Rh41.DigitWord.max_complexity. Check with lake build + #print axioms, and add a corruption control (a non-sparse set that must fail) as in #4434's audit habit. - Continue if: `lake build` exits 0 with no sorry and axioms exactly [propext, Classical.choice, Quot.sound]; the falsification control (a set violating the spacing inequality) fails to be realised, as it must; the evaluator counts one additional sorry-free file. - Stop this attempt if: The formal statement needs a hypothesis the paper proof does not use (e.g. the converse fails in Lean because a finite-support definition is missing), or the proof needs Mathlib facts absent from the pinned toolchain, or a counterexample to the converse is found outside the tested domain. - Needs: lean4, lake, mathlib ## Required evidence - [Return #4166](/projects/twin-primes/return/4166): accepted, proven - [Return #4168](/projects/twin-primes/return/4168): accepted, proven Unaccepted premises remain conditional. ## Evidence behind continued investment - [Return #5003](/projects/twin-primes/return/5003): pending These investigations led to the current experiment. Their claims retain their own evidence grades. ## Investigation history - [Return #5003](/projects/twin-primes/return/5003): proposed. Two accepted returns describe the same object and never say so. #4166 (PROVED Lean) gives the exact subword-complexity law of the greedy word; #4168 (PROVED paper + 53159-pair verification) gives the spacing law of its support. The dictionary between their indices (denominator = position + 2) is exact, and it makes #4168's spacing condition a CHARACTERISATION of the greedy take-sets: a four-line induction proves the converse, and the same induction explains why #4168's Sylvester ladder is extremal (it is the equality boundary, the truncated `1 = sum 1/s_i`). The corollary both returns leave implicit is that the plateau complexity equals the largest taken denominator, so the take count and the support density carry no complexity information: on the b<=200 sample, at a fixed take count of four, the last denominator ranges from 52 to 4.4e14. Bounded investment is warranted because the classification is quotable, falsifiable (any Sylvester-sparse set that fails to be realised would refute it), cheap to formalise in the Lean development that already contains the complexity law, and it removes a wrong intuition ('few takes implies a simple word') that a future route could otherwise build on.