# How an exact value of f(a,2) gets pinned down This note explains, through worked examples, how values like ```text f(5,2) = 3, f(4,2) = 6, f(2,2) = 254, f(34,2) = 18444 ``` are DETERMINED — not just bounded from below — and why the same procedure works at every even `a` where the value is finite. Throughout, `f(a,2)` is the largest `K` such that some finite increasing list `a = a_1 < a_2 < ... < a_n` has `2^K | a_1! + ... + a_n!`, and `v_2(m)` is the exponent of 2 in `m`. ## 0. The shape of every exactness proof An exact value is two separate finite facts: ```text LOWER: f(a,2) >= K one explicit list; checking it is modular arithmetic straight from the definition. UPPER: not f(a,2) >= K+1 an exhaustive finite decision: NO list works. ``` The upper side looks infinite (all finite lists) but is not, because of one observation: ```text Modulo 2^(K+1), every n! with v_2(n!) >= K+1 is zero. Terms that large can be added or removed freely without changing divisibility by 2^(K+1). Since v_2(n!) = n - s_2(n) -> infinity, only finitely many n matter. ``` So `f(a,2) >= K+1` is a finite subset-sum question modulo `2^(K+1)`, and a "no" answer is a theorem obtained by finite search. Everything below is this one idea at three different scales. ## 1. Worked example: f(5,2) = 3 (odd a — no search needed) **Lower.** The one-term list `[5]` gives `5! = 120 = 2^3 * 15`, so ```text f(5,2) >= 3. ``` **Upper.** Any admissible list starts at 5, and every later element is `>= 6`. Now ```text 5! = 120 == 8 (mod 16), n! == 0 (mod 16) for every n >= 6 (6! = 720 = 16 * 45, and each further factor keeps v_2 >= 4). ``` So EVERY admissible factorial sum is `== 8 (mod 16)`. It is never divisible by `2^4`: ```text f(5,2) <= 3, hence f(5,2) = 3. ``` That is the whole proof, and it is formalized end-to-end in `lean/S404_5_2_exact.lean` (theorem `f_5_2_eq_3`). **Why this settles every odd `a`.** For odd `a`, write `v = v_2(a!)`. Every later factorial contains the extra even factor `a+1`, so all of them are `== 0 (mod 2^(v+1))`, while `a!` itself is `2^v * odd`. The sum is pinned at exactly `v`: ```text f(a,2) = v_2(a!) for all odd a. ``` The deficit at the first blocked level can never be repaired by the tail. Odd `a` is the degenerate case where the game ends before it starts. ## 2. Worked example: f(4,2) = 6 (even a — the finite search, by hand) For even `a` the tail lives at the SAME 2-adic level as `a!` (because `a+1` is odd), so cancellation is possible and the value can run far above `v_2(a!)`. This is where search begins. **Lower.** There is a pretty identity (see the gallery): ```text a! + (a+1)! + (a+3)! = a! * (a+2)^3. ``` At `a = 4`: `4! + 5! + 7! = 24 * 216 = 5184 = 2^6 * 81`, so ```text f(4,2) >= 6 with witness [4, 5, 7]. ``` **Upper.** Decide `f(4,2) >= 7` modulo `2^7 = 128`. Since `v_2(8!) = 7`, every `n!` with `n >= 8` is `0 (mod 128)`: only the possible members 5, 6, 7 matter, plus the forced head 4. Their residues: ```text 4! == 24, 5! == 120, 6! == 80, 7! == 48 (mod 128). ``` Walk the candidates from the top, recording which residues a strictly increasing tail with entries `>= m` can reach mod 128: ```text entries >= 8: {0} entries >= 7: {0, 48} (take 7 or not) entries >= 6: {0, 80, 48} (80 + 48 = 128 == 0: the first genuine cancellation) entries >= 5: {0, 80, 48, 120, 72, 40} ``` Add the head `4! = 24` to each reachable tail residue: ```text 24 + {0, 80, 48, 120, 72, 40} == {24, 104, 72, 16, 96, 64} (mod 128). ``` Zero does not occur. No list from 4 is divisible by `2^7`: ```text f(4,2) <= 6, hence f(4,2) = 6. ``` This table-walk is formalized, stratum by stratum, in `lean/S404_4_2_exact.lean` (theorem `f_4_2_eq_6`). It is also exactly what the production code does — the hand computation above IS the gate DP at toy size. ## 3. Normalization: how the search is organized at scale Divide the defining sum by `a!`. With offsets `j` and ```text P_j(a) = (a+1)(a+2)...(a+j), W_J(a) = 1 + sum_{j in J} P_j(a), ``` a list `{a} ∪ {a+j : j in J}` certifies `f(a,2) >= v_2(a!) + v_2(W_J(a))`. Writing ```text g(a,2) = f(a,2) - v_2(a!) (the "extra depth" beyond a!), ``` the question becomes: how deep can `W_J(a) == 0 (mod 2^G)` be pushed? Two elementary lemmas make this finite and structured: ```text * offset truncation: if W_J(a) == 0 mod 2^G, the truncated set J ∩ [1, 2G+1] already works (long products carry v_2 > G). * determinacy: whether g(a,2) >= G depends only on a mod 2^G. ``` The DP then processes the tail level by level ("gates"): at each 2-adic level it keeps the set of reachable partial residues, exactly like the four-line table in section 2, except that the state sets are pruned and rescaled so that spike-depth runs stay small. For `a = 34` the reachable set never exceeds 64464 states even though the target is `2^18412`. ## 4. The same procedure at scale **f(2,2) = 254.** ```bash python3 scripts/p2_exact_search.py one --a 2 --p 2 --target 255 # -> Result: no witness (upper: f(2,2) <= 254) ``` The lower side is the 119-term list proved in Lean (`lean/S404_2_2_254.lean`). The value agrees with Lin's bound `f(2,2) <= 254` recorded on the Erdos Problems page — but the decision above is independent of it. **f(34,2) = 18444** (the largest exact value known). ```bash python3 scripts/p2_scaled_gate_search.py one --a 34 --extra-target 18412 --max-states 100000 # -> Result: witness exists (g(34,2) >= 18412, i.e. f(34,2) >= 18444) python3 scripts/p2_scaled_gate_search.py one --a 34 --extra-target 18413 --max-states 100000 # -> Result: no witness (g(34,2) <= 18412, i.e. f(34,2) <= 18444) ``` Both decisions take seconds. The passing run is then upgraded to an explicit certificate: ```bash python3 scripts/p2_scaled_witness.py one --a 34 --extra-target 18412 --output a34.txt --verify python3 scripts/verify_witness_file.py --a 34 --g 18412 --file data/a34_g18412_witness_indices.txt # -> PASS: 1 + sum n!/34! == 0 mod 2^18412 ``` The last command is deliberately dumb: it re-multiplies the ratios `n!/34!` modulo `2^18412` and checks the sum, sharing no code with the search. House rule for every published exact value: ```text lower side: explicit witness file, re-verified from the definition; upper side: the no-witness decision, re-run in a second, independently written DP implementation. ``` The same pipeline produced `f(1102,2) = 12633`, `f(3456,2) = 8275`, and `f(8190,2) = 16396`, whose witness files (except 8190) ship in `data/`. ## 5. Why this terminates — and the one thing it cannot do For each fixed `G` the decision `g(a,2) >= G` is finite. So IF `f(a,2)` is finite, running `G = 1, 2, 3, ...` eventually hits the first failure and the procedure halts with a two-sided certificate. Every even `a <= 256` has halted, and so have the deeper spikes 1102, 3456, and 8190 — but see the champion below for one that has not halted yet. In this precise sense f(a,2) is exactly determined at every a where it is finite — and the complete classification of all even classes with `g <= 24` (a finite certified computation over 174,640 residue classes) determines it simultaneously for MOST integers: the surviving fraction decays like `~ 11.5/G`. What the procedure can never do is certify `f(a,2) = infinity`. A witness only ever proves a lower bound; "no death at depth G" only says `g >= G`. The open core of Problem #404 at p = 2 is exactly: ```text Is f(a,2) finite for every positive even a? ``` The current champion illustrates the asymmetry: `a = 594` is certified ```text f(594,2) >= 66126 (g(594,2) >= 65536, verified 2026-07-06) ``` with deeper probes still running. Either some probe finally fails — and 594 joins the exact table with the largest value ever computed — or it never does, and no amount of computation will tell us.