# Erdős–Straus induction search task graph

The proof search uses the graph-engineering diamond pattern. Evidence branches may run independently; none may publish a universal claim. One verifier owns the merge.

```mermaid
flowchart LR
  I[Artifact integrity] --> A[Arithmetic transfer branch]
  I --> B[Bounded-shift branch]
  I --> C[Probability / mass-gap branch]
  I --> D[Literature compatibility branch]
  A --> V[Independent proof-obligation verifier]
  B --> V
  C --> V
  D --> V
  V --> M[Merge surviving lemmas]
  M --> H{Human publication gate}
  H -->|all universal premises proved| P[Universal theorem]
  H -->|any premise sampled, circular, or open| O[Open obligation record]
```

## Branch contracts

### Arithmetic transfer

Produce a total reduction for every remaining prime `p ≡ 1 (mod 24)`, a strictly decreasing rank, and an exact witness transformer. A quotient or anchor is not a reduction unless a witness for the smaller instance is actually consumed to build the witness for `p`.

The Type-II scaling branch now supplies a genuine transformer:

```text
4/q = 1/x + 1/(qb) + 1/(qe)
                     │
                     │ p = q + 4(L - 1)x
                     ▼
4/p = 1/(Lx) + 1/(Lpb) + 1/(Lpe)
```

For `L >= 2`, the parent has `q < p/2`. The remaining totality obligation is
not the algebra: it is proving that every hard prime admits an interior
Type-II certificate to which this transformer applies. Exact finite coverage
through `10^8` supports that target but does not discharge it.

### Bounded shift

Falsify or support candidate finite-shift covers. Any finite computation is evidence only. A surviving bound becomes a theorem only with a symbolic proof that every admissible prime is covered.

### Probability / mass gap

Seek an exact proof that the zero-witness set has mass zero under a full-support instance distribution, or prove a structural lower mass gap for every nonempty failure set and an exact upper bound below it. Confidence intervals and density-one statements do not pass.

### Literature compatibility

Check that a proposed lemma is stronger than known finite, density, or fixed-depth results and does not contradict known blind families.

## Verifier questions

1. Is the rank demonstrably well-founded?
2. Does every nonbase prime enter exactly one proved branch?
3. Does the transformer use only proved lower-rank witnesses and exact arithmetic?
4. Is totality proved rather than inferred from observed coverage?
5. Can the final witness be checked independently by `4xyz = p(xy+xz+yz)`?

## Stop rule

Stop and retain an open obligation if any branch relies on:

- a finite search bound without a universal theorem;
- “almost all,” density one, or sampled 100% success;
- a reduction whose output is not strictly lower rank;
- a transformer that assumes the target instance already has a witness;
- a fixed shift or finite shift family whose total coverage is only empirical.

Two synthesis rounds are allowed before the task returns to the open-obligation state. A publication claim requires a separate human gate after independent checking.
