{"id":5003,"job_id":9917,"problem_id":1,"lane_id":3,"type":"explore","user_id":1,"model":"deepseek-v4-flash","provider":"deepseek","report_md":"# Cross-lane synthesis: one greedy word, two exact laws — #4166's complexity law and #4168's Sylvester-sparsity\n\nJob **#9917** (explore, lane `formalize`, stage `discover`, general mode). Attempt\n``. Documents and exact computation only; no sieve, no Lean run\n(no Lean toolchain installed on this host, see §9).\n\n**Headline.** #4166 and #4168 are about *the same word*: #4166's greedy digit word (take `1/(n+2)`\niff it fits) and #4168's greedy word (take `1/m` at `m=n+2` iff it fits). Neither return says so;\n#4168 indexes by *denominator* `m`, #4166 by *position* `n=m-2`. Identifying the two indices does\nthree things: (A) it transfers #4166's machine-checked complexity law verbatim to #4168's object;\n(B) it exposes that #4168's Sylvester-sparsity is not only necessary but **sufficient** — a\nfour-line induction classifies the greedy take-sets exactly, with #4168's Sylvester ladder as the\nattained boundary; (C) it yields the invariant both returns leave implicit: the word's plateau\ncomplexity is *exactly its largest taken denominator*, so the number of takes and the support\ndensity carry no complexity information at all. All of this is checked in exact arithmetic below\n(11/11 checks, corruption control OK).\n\n## 1. The two accepted results, at their rungs\n\n**#4166** (paper, `author_rung: proven`; folder `002-greedy-digit-word`). Setup (§2): `r_0=x`,\n`r_{n+1}=r_n-1/(n+2)` iff `r_n >= 1/(n+2)`, `w(x)=δ_0δ_1...`; support `S={a_0<...=max(span,a_m+1)`,\n\n p(L) = min(a_m+1, N-L+1) + [L <= N-a_m-1].\n\n**Corollary 4** (PROVED Lean, `Rh41.DigitWord.max_complexity`): if `N>=2a_m+2` then `max_L p(L)=a_m+2`.\n\n**#4168** (paper, `author_rung: proven`, lane `formalize`'s neighbour `rh47`). Setup (§2): the same\nrule on the same alphabet, support written as *denominators* `A(x)={m=n+2 : 1/m taken}`, i.e. the\ngreedy Egyptian expansion. **Theorem (Sylvester-sparsity)** (§3.1, PROVED (paper), VERIFIED with\n`0 violations in 53159 consecutive pairs`): `m_{i+1} >= m_i(m_i-1)+1`. Consequences stated there:\n`|A|>=20` forces `max A >= s_20` (106 721 digits); support density `≈3.9e-5`; take count\n`O(log log N)` (quoted from `rh41`); measured maxima `11` (sample A: `b<=200`) and `18` (sample B:\n400 random `b in [1e6,1e12]`). #4168 §3.7/§5 records `R4` (Lean formalisation of its barriers) as\n**open**: the `rh47` Lean layer is empty.\n\nThe two returns cite disjoint local histories: #4168 quotes `rh41`/`rh42`/`rh46`; #4166 *is* the\n`Rh41` Lean development (`Rh41__DigitWord.lean`, `Rh41__GreedyResidual.lean`, ...).\n\n## 2. The dictionary (the missing link)\n\n#4166's position `n` and #4168's denominator `m` satisfy **`m = n+2`**; hence\n\n a_m(#4166) = (max A(#4168)) - 2, a_0 = (min A) - 2, span = max A - min A.\n\nVerified exactly (R1): #4168's own counterexample target `x=30/103` reproduces\n`A=[4, 25, 793, 907545, 1482547361100]`, `residual 0`, so `a_m = 791` in #4166's indexing.\nThe greedy rule's least admissible denominator is `ceil(1/r)` (exact integer arithmetic), which is\nalso how #4168's probe computes the chain; `0` violations of that agreement appear below.\n\n## 3. Theorem A (transfer) — conditional on #4166, verified here\n\n**A.** For every rational `x in (0,1)` and every truncation length `N` with support inside\n`[0,N-1]`, #4166's Theorem 1 and Corollaries 2–4 hold for the word `w(x)` of #4168 with\n`a_m = max(A∩[1,N]) - 2`. In particular, at the plateau (`N>=2a_m+2`),\n\n max_L p(L) = a_m + 2 = max A. (A)\n\n*Why.* The rule is identical term by term; the dictionary is a change of variable. No hypothesis of\n#4166 mentions the alphabet beyond `1/(n+2)`.\n\n*Checked* (R6, brute force against the definition, never against the formula): ladder `k=3`\n(`a_m=5`, `N=12`, 7 values of `L`), ladder `k=4` (`a_m=41`, `N=84`, 43 values), #4168's witness\n`30/103` at `N=2000` (`a_m=791`, 1209 values), a random target `83/199` at `N=400` (390 values):\n**0 mismatches**. (A) verified at `k=1..4` (R7): `max_L p(L) = 2,3,7,43 = s_k`. Note what the\ncontrol shows: moving an *interior* support element does **not** change `p(L)` — that is the\ntheorem's content — while moving the maximum does (M2a/M2b).\n\n## 4. Theorem B (converse) — the piece neither return states\n\n**B.** A finite set `S={2<=m_1<...= m_i(m_i-1)+1` for all `i`.\n\n*Proof.* (⇒) is #4168's theorem: after taking `1/m_i` the residual is `< 1/(m_i(m_i-1))` (the same inequality\nas in the induction below, at `i+1`), so no denominator `<= m_i(m_i-1)` can follow.\n(⇐) Let `c_i = Σ_{j>=i} 1/m_j` (`c_{k+1}=0`) and prove `c_i < 1/(m_i-1)` by descending induction.\nBase: `c_k = 1/m_k < 1/(m_k-1)`. Step: from `c_{i+1} < 1/(m_{i+1}-1)` and\n`m_{i+1} >= m_i(m_i-1)+1`,\n\n c_i = 1/m_i + c_{i+1} < 1/m_i + 1/(m_i(m_i-1)) = 1/(m_i-1).\n\nEvery inequality is strict because the base is strict and the sum is finite. Now run the greedy rule\non `x=c_1 < 1` (so `x<1` since `1/(m_1-1)<=1`). At each stage the residual is `c_i`, and two facts\nhold: `c_i >= 1/m_i`, so `1/m_i` is admissible; and `c_i < 1/(m_i-1)`, so for **every** denominator\n`m <= m_i-1` one has `1/m >= 1/(m_i-1) > c_i`, and no smaller denominator is admissible. Hence the\ntakes are exactly `m_1,...,m_k`, in order, and the residual after the last is `c_{k+1}=0`. ∎\n\n*Sharpness (why #4168's ladder is extremal).* The strictness in the induction fails exactly at the\ninfinite Sylvester sequence, for which `c_i = 1/(m_i-1)` identically (classical: `Σ_i 1/s_i = 1`,\nso `1/s_1 = 1/2 = 1/(s_1-1)` and the tail of `s` is again a Sylvester tail). #4168's ladder\n`x_k=(s_{k+1}-2)/(s_{k+1}-1) = Σ_{j<=k} 1/s_j` is precisely that boundary truncated, which is why\nits support is exactly `{s_1,...,s_k}` and why **the spacing inequality is attained at every\nconsecutive pair of the ladder** (R3: 15 equal pairs for `k=6`; #4168 states the inequality, not\nits attainment). So B does not merely invert #4168: it identifies the extremal family as the\ntruncated boundary of the proof.\n\n*Checked* (R9a): over **all 4095 non-empty subsets** of `{2,...,13}`, exactly **39** are\nSylvester-sparse and exactly the same 39 are realised — no sparse set unrealised, no realised set\nnon-sparse. (R9b): **all 10 693** Sylvester-sparse sets with `max S <= 300` are realised, with\n`S` recovered from `x=Σ1/m_i` by the greedy rule and residual exactly `0`.\n\n## 5. Corollary C — the invariant both returns leave implicit\n\n**C.** For every rational target and truncation with `N >= 2*max A - 2`:\n\n max_L p(L) = max A = m_k, and the plateau is p(L) = m_k for max(span,m_k-1) <= L <= N+1-m_k.\n\nSo the word's peak complexity is **its largest taken denominator** — not the number of takes, not\nthe density. Measured consequence (R8, real targets with `b<=200`): at fixed take count `k=4`\n(`5811` targets) `max A` ranges from `52` to `4.44e14`, so the predicted plateau complexity ranges\nfrom `54` to `4.44e14` — twelve orders of magnitude at the *same* `k`. At fixed `k=3` (`6223`\ntargets) the range is `12 … 8.89e7`. #4168's headline `density ≈3.9e-5` and #4166's `a_m` are\ntherefore different functions of one word: density tracks `|A|`, complexity tracks `max A`, and\nSylvester-sparsity constrains only the gaps between consecutive takes, leaving `max A` almost free\n(any sparse set is attained, by B).\n\n## 6. What this changes, and what it does not\n\n* It gives #4168's Sylvester-sparsity the status of a **classification** (B), not only a necessary\n condition, and explains its extremal ladder as the equality boundary of the proof.\n* It makes #4166's theorem **applicable to #4168's object without re-proving anything** (A, C), and\n identifies the single quantity — `max A` — that both returns treat implicitly (`a_m` there,\n \"forces `max A >= s_20`\" here).\n* It says a word-shape statistic cannot be a proxy for the take count or for density: **at fixed\n `k` the plateau complexity is unbounded over the class** (R8), and **every** sparse set is\n attained (B, R9). Any future use of \"few takes ⇒ simple word\" or \"density ⇒ information\" is\n refuted by Corollary C plus Theorem B.\n* It does **not** touch the parity problem. #4168's B1/B2/B3 verdicts are about `λ`-values at\n support positions and about the `ζ` budgets; #4166's law is about the *shape* of the word (factor\n counts). C constrains factor-based statistics only; it implies nothing about\n `Σ_{n<=x} λ(n)λ(n+2)`. The `O(log log N)` take-count quote in #4168 is consistent with, not\n derived from, B (B gives the same order via `s_k <= N+1`).\n* It leaves #4168's `R4` cheaper than it looks: the *complexity* half is already machine-checked in\n #4166's Lean development (`Rh41`), and B's proof is four lines of `Nat`/`Finset` arithmetic\n (see the proposed next step).\n\n## 7. Machine check (this run)\n\n`check_du.py` (attached) — exact `Fraction`/integer arithmetic, no floating point in any decision;\n`python3 check_du.py` → **11/11 PASS, exit 0** (`check_du.out`), `python3 check_du.py --corrupt` →\n**CONTROL RESULT: OK, exit 0** (`check_du.control.out`). Checks: R0 chain completeness (no\ntruncation), R1 dictionary witness, R2 ladder supports, R3 sharpness, R4 exhaustive `b<=200`\n(19 900 targets, 48 840 consecutive pairs, 0 violations, max `|A| = 11`), R5 random\n`b in [1e6,1e12]` (300 targets, 3 034 pairs, 0 violations, max `|A| = 17`, histogram\n`7:7 8:14 9:35 10:60 11:65 12:54 13:36 14:17 15:6 16:3 17:3`), R6 transfer, R7 corollary at the\nladder, R8 take-count/complexity spread, R9a/R9b the converse.\n\n**Cross-check against the accepted record:** R4 reproduces #4168's sample-A maximum `11` exactly, and\nR5's maximum `17` is consistent with its sample-B `18` at a smaller sample (300 against 400).\n\n**A defect this check found in itself, disclosed.** The first version of `greedy_support` capped the\nchain at `1e18`; `44/53`'s seventh take is `6.97e20`, so supports were silently truncated and the\nsample maximum came out `7` instead of `11`. It was caught *because* #4168 records `11`; the cap was\nremoved, R0 (completeness, residual exactly `0`) was added, and the mutation control extended with a\nspecificity case (an interior move that must **not** fire, M2a) beside the must-fire cases M1, M2b,\nM3, M4.\n\n## 8. What a reviewer must check\n\n1. **The dictionary** (§2): `m = n+2`, and #4166 §2's `S` is a set of *positions* while #4168 §2's\n `A` is a set of *denominators*. One line each; if this is wrong, A and C fall and only B stands.\n2. **Theorem B's induction** (§4): the two inequalities `m_{i+1} >= m_i(m_i-1)+1` and\n `c_{i+1} < 1/(m_{i+1}-1)` giving `c_i < 1/(m_i-1)`; strictness at the base; finiteness used for\n strictness throughout. A counterexample to B would be a Sylvester-sparse set not realised by\n `x=Σ1/m_i`; R9a/R9b found none, so a refutation would have to be outside `{2..13}`/`max<=300`.\n3. **Corollary C's hypothesis**: `N >= 2a_m+2` is #4166's Corollary 4 hypothesis, not a new\n assumption; without it the plateau can be empty (their §3.1 example: support `{0..199}`, `N=259`,\n `max_L p(L)=60`, not `201`). Also check the translation `a_m+2 = max A` (the `+2` of the position\n index against the denominator index).\n4. **The theorem is elementary.** B is very likely folklore for greedy Egyptian expansions; this\n return proves it here and verifies it finitely, and does **not** claim literature novelty. The\n contribution claimed is the *identification* of the two objects, the exactness of #4168's\n condition, and Corollary C.\n5. **R8's numbers are properties of the sample `b<=200`** with `a_m<=60` brute-forced; larger `a_m`\n values are predicted by Corollary 4, whose proof is #4166's.\n\n## 9. What is not claimed\n\nNo progress on the twin prime conjecture, the parity problem or `(*)`; no statement about\n`Σλ(n)λ(n+2)`. No Lean artifact: this host has no Lean toolchain (`lean`, `lake` and `elan` are absent), so #4168's `R4` is *not* discharged here and #4166's theorem is used as\nserved. No audit of #4166's or #4168's Lean/paper proofs beyond reading their statements; no claim\nthat the two returns' *authors* intended this connection. No new measurement of `λ` or of primes.\n`cpu_hours 0.0` — the checker is wall-clock `≈13.5 s` single-threaded, no registered process; exact\ninteger arithmetic only. Usage is **unmeasured**, not zero.\n\n## 10. Relation to the named returns\n\n- **#4166** (reused, its Theorem 1 and Cor 2–4 are the engine of A/C).\n- **#4168** (reused and sharpened: `⇒` is its theorem; B adds `⇐`; C uses its indexing).\n- **#4165** (checked for overlap): `corrSlice(h,a,N)=corr(h,N)` for `N+h= 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.","uncertainty_md":"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.","contribution_md":"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 (*)."},"next_step":{"method":"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.","compute":{"ram_gb":4,"disk_gb":2,"cpu_hours":0},"failure":"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.","success":"`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.","question":"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?","budget_hours":1.5,"required_tools":["lean4","lake","mathlib"],"required_sources":[]},"depends_on":[4166,4168],"evidence_md":"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."},"research_route_id":343,"verification_plan":{"cost":{"ram_gb":1,"disk_gb":1,"minutes":1,"cpu_hours":0.01,"judgment_minutes":15},"claim":"Finite instances of: a finite set S={2<=m_1<...= m_i(m_i-1)+1; and #4166's Theorem 1 holds verbatim for #4168's word under the dictionary m = n+2.","scope":"All 4095 non-empty subsets of {2..13}; all 10693 Sylvester-sparse sets with max element <= 300; all a/b with 2<=b<=200; 300 random targets with b in [1e6,1e12] (seed 20261020); four truncations for the complexity law (ladder k=3 and k=4, target 30/103 at N=2000, target 83/199 at N=400).","tools":["python3"],"inputs":[],"checker":"046e4092c1084ce2c4a06eee6e9cd93756ee4ec39a0cf7294e55f2b3336f9015","command":"python3 check_du.py","targets":["check_records.json"],"coverage":"sample","expected":"stdout ends with 'checks: 11 fails: []' and 'RESULT: PASS', exit status 0; the records show R9a subsets=4095 sparse=39 realised=39, R9b sparse_sets_max_300=10693 failures=[], R4 violations=0 max_support_size=11, R5 violations=0.","manifest":[{"path":"check_du.py","role":"checker","sha256":"046e4092c1084ce2c4a06eee6e9cd93756ee4ec39a0cf7294e55f2b3336f9015"},{"path":"check_records.json","role":"target","sha256":"663231a0d90ef0b87625df14dbda583e7795ca2fb713d273cc403c021681e47a"}],"supports":"Passing establishes exactly the finite instances above with exact arithmetic and a mutation control; it does not prove the general theorem (proved on paper in the report, section 4), does not re-prove #4166's law, and says nothing about infinite-support targets.","comparison":"Exact equality of the realised support with S and of brute-force p(L) with the formula; no tolerance is used anywhere (all quantities integer or rational).","assumptions":"Exact Fraction/integer arithmetic; the greedy rule takes the least denominator ceil(1/r); the support is complete (residual exactly 0, check R0); #4166's Theorem 1 is used as served.","coverage_md":"Exact inclusive domain as in scope: every non-empty subset of {2,...,13} (2^13-1 = 8191/2 -> 4095 subsets of size>=1); every Sylvester-sparse set with max element <= 300 (10693 sets, max size 4); every a/b with 2<=b<=200 and 1<=a= m_i(m_i-1)+1; and #4166's Theorem 1 holds verbatim for #4168's word under the dictionary m = n+2. Scope: All 4095 non-empty subsets of {2..13}; all 10693 Sylvester-sparse sets with max element <= 300; all a/b with 2<=b<=200; 300 random targets with b in [1e6,1e12] (seed 20261020); four truncations for t… (shortened; full text on the return)","Assumptions declared by the author: Exact Fraction/integer arithmetic; the greedy rule takes the least denominator ceil(1/r); the support is complete (residual exactly 0, check R0); #4166's Theorem 1 is used as served.","Why the check supports the claim, as the author argues it: Passing establishes exactly the finite instances above with exact arithmetic and a mutation control; it does not prove the general theorem (proved on paper in the report, section 4), does not re-prove #4166's law, and says nothing about infinite-support targets.","Coverage declared by the author: sample, not decisive. Exact inclusive domain as in scope: every non-empty subset of {2,...,13} (2^13-1 = 8191/2 -> 4095 subsets of size>=1); every Sylvester-sparse set with max element <= 300 (10693 sets, max size 4); every a/b with 2<=b<=200 and 1<=a= m_i(m_i-1)+1; and #4166's Theorem 1 holds verbatim for #4168's word under the dictionary m = n+2.","scope":"All 4095 non-empty subsets of {2..13}; all 10693 Sylvester-sparse sets with max element <= 300; all a/b with 2<=b<=200; 300 random targets with b in [1e6,1e12] (seed 20261020); four truncations for the complexity law (ladder k=3 and k=4, target 30/103 at N=2000, target 83/199 at N=400).","assumptions":"Exact Fraction/integer arithmetic; the greedy rule takes the least denominator ceil(1/r); the support is complete (residual exactly 0, check R0); #4166's Theorem 1 is used as served.","supports":"Passing establishes exactly the finite instances above with exact arithmetic and a mutation control; it does not prove the general theorem (proved on paper in the report, section 4), does not re-prove #4166's law, and says nothing about infinite-support targets.","coverage_md":"Exact inclusive domain as in scope: every non-empty subset of {2,...,13} (2^13-1 = 8191/2 -> 4095 subsets of size>=1); every Sylvester-sparse set with max element <= 300 (10693 sets, max size 4); every a/b with 2<=b<=200 and 1<=a