# Erdős--Straus proof-search literature audit

**Audit date:** 2026-09-04  
**Scope:** sources that could support a direct certificate or a strict
witness-preserving descent for primes `p == 1 (mod 24)`.

## Sources that survive the proof boundary

### Complete parameterizations

1. **Dahan, _Sieve dimension and search depth for the Erdős--Straus
   conjecture, n ≡ 1 (mod 24)_**  
   <https://arxiv.org/abs/2608.24035>

   Theorem 3.9 gives an exact Type-II criterion: a prime `n` has a Type-II
   solution exactly when there are `u,a >= 1` and a divisor
   `s | an+u` with `s == -1 (mod 4ua)`.  This is directly useful as a
   certificate verifier.  The paper proves strong fixed- and growing-depth
   exceptional-set estimates, but explicitly leaves open whether the
   all-depth Type-II exceptional intersection is empty.  Its Euclidean
   quotient is a search coordinate, not a smaller Erdős--Straus instance.

2. **Bello-Hernández, Benito, Fernández, _A Divisor Parametrization for the
   Erdős--Straus Conjecture_**  
   <https://arxiv.org/abs/2606.10922>

   Theorem 5 proves completeness of the `fab` divisor identity for the scaled
   three-denominator representation.  Proposition 20 proves a genuine
   translation invariance, preserving an existing certificate under
   `n -> n + 4abk`.  It does not prove that every target lies in one of the
   resulting progressions.  This makes it a sound transport component, not a
   total descent theorem.

3. **Elsholtz and Tao, _Counting the number of solutions to the
   Erdős--Straus equation on unit fractions_**  
   <https://arxiv.org/abs/1107.1010>

   The Type-I/Type-II parameterizations and average solution counts are sound
   structural inputs.  Average abundance cannot establish pointwise
   nonemptiness for every prime, so these estimates do not close the universal
   quantifier.

### Congruence and factorization structure

4. **Xu, _Congruence Classes of Supporting the Erdös-Straus Conjecture I:
   Tame Solutions_**  
   <https://arxiv.org/abs/2605.23601>

   Xu derives many exact congruence families and identifies finite "wild"
   primes outside the tame subfamily.  The families improve the direct branch
   inventory but do not provide a total cover or a witness transformer from a
   lower instance.

5. **Lean-verified offset construction**  
   <https://github.com/carlok/erdos-straus-offset-lean>

   The formal development checks the positive divisor split, certificate
   reconstruction, fixed-divisor transport under `n -> n + 4pdk`, and the
   least transport period.  It explicitly makes no universal claim.  This is
   strong confirmation that transport algebra is not the missing step;
   progression coverage is.

## Claimed proofs that do not pass the audit

### Bradford 2026

<https://arxiv.org/abs/2602.11774>

The paper derives valid congruence families, then states that the remaining
task is to show they form a covering system.  It does not supply that covering
proof; noticing several initial primes cannot discharge the universal claim.

### Dyachenko 2025

<https://arxiv.org/abs/2511.07465>

The proposed affine-lattice closure depends on Lemma 9.24 and Proposition
9.25.  Their proof independently chooses representatives for the two
coordinates of a rectangle and then assumes one diagonal shift realizes both.
This is false.  For example, with

\[
L=\{(u,v)\in\mathbb Z^2:u+v\equiv0\pmod2\},
\]

the claimed diagonal period is one, yet the unit rectangle containing only
`(0,1)` does not meet `L`.  Thus the advertised unconditional step cannot be
used without a new transverse lattice bound and additional arithmetic input.

## Relevant current working frontier

The public CENTL/Free Computation Foundation repository contains an extensive,
explicitly non-closing signed-divisor/Kneser program:
<https://github.com/chasebryan/centl/tree/main/research/erdos-straus>.

Useful checked ideas include:

- exact signed-divisor target formulations;
- quadratic-character and Kneser defect classifications;
- an external-nonresidue factor cycle for every hard prime;
- explicit counterexamples showing that a whole external cycle can fail at
  every vertex even though another shift solves the prime;
- consecutive-shift state analyses whose remaining step is joint
  incompatibility, not local classification.

These working notes reinforce the same boundary found independently here:
quadratic nonresidues and transport create structured candidates, but neither
forces the required divisor placement at some shift.

## New synthesis from this audit

The exact Type-II scaling lemma in `type-ii-scaling-descent.md` supplies a
strict transformer

\[
(q,x,b,e)\longmapsto
\bigl(p=q+4(L-1)x,\ Lx,\ Lpb,\ Lpe\bigr).
\]

The universal problem can now be asked as one sharply delimited statement:

> Does every hard prime have an interior signed-divisor hit at some admissible
> shift, leaving a nontrivial anchor factor available for strict scaling
> descent?

The exact answer is **yes for all 719,781 hard-class primes below `10^8` in
the present computation**.  It also survives deterministic sparse probes of
`100,000` Mordell-hard primes beginning at `10^15` and `5,000` beginning at
`9*10^17`.  It remains **unproved universally**.  This is the best surviving
route found in the audit.
