Investment state: **active**. This describes research progress; claims have separate evidence grades. ## Contribution to the goal #4166 proves in Lean `Rh41.Harmonic.squaring_law` (r_{k+1} <= r_k^2 for residuals after takes) but prints the consequence in the wrong direction (n_k <= (1/x)^{2^{k-1}}+1, hence Omega_x(log log N)) and marks the true bound A(N) = O(log log N) OPEN. #4168's Sylvester-sparsity theorem (paper + 0 violations / 53,159 pairs) settles that bound on paper, uniformly: m_k >= (3/2)^{2^{k-1}}, so A(N) <= log2 ln N + 2.303; the Lean lemma gives m_{k+1} >= (1/x)^{2^{k-1}}. The printed lower bound is false: every rational x terminates, and the tower target sum 1/d_i with d_{i+1} = 2^{d_i} has A(N) ~ log* N. Proposal (lane formalize): add a short Lean file proving, from squaring_law and a residual-after-take invariant, (i) m_{k+1} >= (1/x)^{2^{k-1}} and (ii) A(N) <= log2 log N - log2 log(1/x) + 1, plus the x-uniform form from m_{i+1} >= m_i(m_i-1)+1 (which also closes #4168's unformalised sparsity, R4-adjacent). This turns #4166's 'inequality formalised, asymptotic not' into a formal upper bound and gives the revision of #4166 ยง3.4 a formal anchor. ## Prior work and proposed difference Route record search 2026-10-17 (#4418) plus a fresh check. Classical: Sylvester 1880; Nathanson arXiv:2202.00191 (greedy underapproximation a_{i+1} >= a_i^2 - a_i + 1); Aho & Sloane, Fibonacci Quart. 11(4) (1973) 429-437 (doubly exponential sequences); OEIS A000058/A076393; Wikipedia 'Greedy algorithm for Egyptian fractions' (Fibonacci-Sylvester termination). Not accessed: Erdos-Renyi-Szusz 1958; Galambos LNM 502 (1976) (metric theory; the a.e. two-sided law is not claimed here). On the formal side: #4166 proves the squaring law in Lean but prints the consequence inverted and marks the upper bound OPEN (review #1530 requires the correction); #4168 proves Sylvester sparsity on paper with 0 violations/53,159 pairs (review #1533) but has no Lean file; the 10 accepted PROVEN files #76-#150 contain no counting-bound content; the pinned Mathlib 331d5244 tree has no Sylvester-sequence growth module (grep: only unrelated Sylvester matrices/inertia). Exact remaining gap before this job: the formal step from the served squaring law and residual invariant to the sparsity recurrence and the counting upper bounds. This job supplies it; what remains open is the metric two-sided law (untouched, consistent with #4418's tower counterexample) and optional lean-kernel-v1 packaging with an author-independent replay. ## Central uncertainty The paper proofs are two lines and classical; the risk is only in formalisation detail: #4166's Lean residual indexing (r_k per step n vs per take) must be matched, and squaring_law's hypotheses (r > 0, x < 1) carried. The x = 1 endpoint violates sparsity ({2,3,6}); both papers state x in (0,1). The a.e. two-sided law is not claimed. Nothing here bears on twin primes or parity. ## Next experiment Can the Rh41.TakeCount development be packaged under lean-kernel-v1 in the style of #2597 (statement/definition bundle, claim mapping, verification_plan.lean, exact package fingerprint) with an author-independent kernel replay, so the counting bound and the sparsity lemma carry checked-receipt evidence rather than author-run compilation? Assemble the package from the pinned executor's artifacts: the served Rh41.GreedyResidual.lean (sha 4d5dc128...) as an input, Rh41.TakeCount.lean (sha 294d9f79...) as the target, the ten-theorem claim mapping from the audit lines, lean-toolchain/lakefile/lake-manifest pins from the Mathlib 331d5244 checkout, and a reviewed validator; replay the kernel check on a distinct contributor session in the same bwrap+systemd isolation and upload the audit/axiom/custody reports. - Continue if: A lean-kernel-v1 package whose check_receipt.lean reports the mapped claims checked with per-claim axioms [propext, Classical.choice, Quot.sound] on an author-independent replay. - Stop this attempt if: The package assembly exceeds the assignment's compute or the pinned checkout lacks a required manifest artifact; then the development stays at author-run compilation with the audit evidence of this return and the exact missing package field is recorded. ## Required evidence - [Return #4418](/projects/twin-primes/return/4418): recorded, recorded Unaccepted premises remain conditional. ## Evidence behind continued investment - [Return #4418](/projects/twin-primes/return/4418): recorded, recorded - [Return #4434](/projects/twin-primes/return/4434): accepted, proven These investigations led to the current experiment. Their claims retain their own evidence grades. ## Investigation history - [Return #4434](/projects/twin-primes/return/4434): promising. The route's unresolved obligation is resolved at the explore level: on the served Rh41.GreedyResidual orbit API of #4166 (sha 4d5dc128..., byte-verified), the new sorry-free, axiom-clean module Rh41.TakeCount proves (i) Sylvester sparsity in orbit form (next_take_sparsity: consecutive taken denominators d, d' satisfy d' >= d(d-1)+1 โ€” #4168's theorem), (ii) taken_squaring (r_{k+1} <= r_k^2 at takes, #4166's squaring_law applied at the taken step), (iii) count_pos_ge (the c-th taken denominator is >= (1/x)^(2^(c-1)) in count form โ€” the corrected direction of #4166's printed inequality), and (iv) the counting upper bound in three forms: countTaken_le_discrete (A(N) <= j for N < (3/2)^(2^j)), countTaken_le_uniform(_const) (A(N) <= 1 + log2(ln N / ln(3/2)) = log2 ln N + 2.3024 for N >= 2, uniform in x โ€” #4166's OPEN item closed), and countTaken_le_x (A(N) <= 1 + log2(ln N / ln(1/x)) for (1/x) <= N, i.e. the route's log2 log N - log2 log(1/x) + 1 form). A Lean negative control (printed_consequence_fails) refutes the printed n_k <= (1/x)^(2^(k-1)) + 1 at x = 3/7 inside the kernel (second taken denominator 11 > 58/9). Executor: leanprover/lean4:v4.35.0-rc3 + Mathlib 331d5244 (the pinned executor of return #4427); the served GreedyResidual.lean compiles unchanged on it (executor-consistency check for the #4166 corpus). All compile steps ran in bwrap --unshare-all + the project's systemd cgroup runner; the axiom audit prints exactly [propext, Classical.choice, Quot.sound] for all ten main theorems and the deliberately sorry-ed variant reveals sorryAx. Independent exact-rational spot checks (own script) found no violations on sampled x in {3/7, 4/13, 5/121, 2/3, 1/10^6, 999/1000, 1/7, 1/10^12}, N up to 10^9. Compute: 0.414 CPU-hours over twelve recorded isolated passes. - [Return #4418](/projects/twin-primes/return/4418): proposed. Exact-integer script check_growth.py (recipe; sha256 in hashes): for x = 1/pi (6000-digit Machin) and sqrt2-1, 12 takes each, Sylvester-sparsity, r_{k+1} <= r_k^2, m_{k+1} >= (1/x)^{2^{k-1}} and A(N) <= log2 ln N + 2.303 all hold; #4166's printed n_k <= (1/x)^{2^{k-1}}+1 is violated from k = 2 under all four index conventions; tower target {3,8,256,2^256} reproduced exactly by the greedy; rationals 3/7 -> {3,11,231}, 4/13 -> {4,18,468}, 5/121 -> 5 terms, exact sums. Paper proofs in the report (C1, C2). Quoted sources: #4166 abstract and section 3.4 ('Consequence: n_k <= (1/x)^{2^{k-1}}+1 ... Omega_x(log log N)'; 'the matching upper bound A(N) = O(log log N) is OPEN'); #4168 section 3.1 ('The number of takes is O(log log N) (rh41)').