Arbitrary finite survival
For every L, some finite seed survives at least L greedy transitions.
No solution is claimed. The official problem remains open. The singleton seed [7] has been verified for one million generated steps, but a finite computation cannot establish infinitude.
1. Recurrence
Given a finite increasing history of primes q1,…,qn, append the least prime among the candidates qn+qi−1. The state is terminal if all historical candidates are composite. Problem 472 asks whether some finite seed produces an infinite greedy trajectory.
For the singleton seed [7], all generated terms are 1 modulo 6. Write q=6x+1. The active recurrence becomes
xn+1 = xn + xi, provided 6(xn+xi)+1 is prime.
2. Durable results
Arbitrary finite termination
For every L, some two-prime seed makes exactly L transitions and then stops.
Semantic core
Greedy steps, terminality, covers, blocker classes, normalization, and regeneration interfaces are Lean-checked.
Static shells fail
CRT constructs fresh blockers against every fixed finite shell; growing rooted information is necessary.
The finite theorems use finite-complexity linear forms in primes for their analytic existence input. Lean checks the elementary recurrence layer conditional on an explicitly named analytic hypothesis; it does not pretend to reprove Green–Tao–Ziegler.
3. What the falsifiers removed
- Long survival, winner rank, dormant-pool size, and fixed phase complexity can all be programmed before termination.
- Literal anchors and predetermined winners hide fixed-gap or thin-sequence prime conjectures.
- First-order modular cover counts lose to overlap; exact covers restate nontermination.
- Unsigned semiprime and factor-energy statistics do not control adversarial bilinear signs.
- Fixed-depth archives, popular gaps, and independent source/target marginals admit CRT or permutation countermodels.
The surviving object is global and rooted: a coefficient built from the actual birth history of the singleton orbit, with memory growing linearly in the current rank.
4. Current F280 target
Let Q be a normalized frontier and P(z)=6z+1. On the broad interval
JQ = {z : Q+⌊Q/2⌋+1 ≤ z ≤ 2Q},
take the 18%-age historical chord coefficient c(z). Filter it by the fixed wheel
W23 = 5·7·11·13·17·19·23 = 37,182,145,
retaining only P(z) coprime to W23. Call the result cW, and let bW be the flat coefficient with the same mass on all wheel survivors in JQ.
With a strict cube-root roughness threshold, every rough label in the relevant interval is either prime or a product of two primes. Therefore, exactly,
Π(u) = R(u) − S(u),
where R is rough mass, S is rough-semiprime mass, and Π is prime mass. It is sufficient to prove at a hypothetical first terminal row that
(R(bW)−R(cW))+ + (S(cW)−S(bW))+ < Π(bW).
The prime number theorem in arithmetic progressions gives Π(bW)>0 for sufficiently large Q. The inequality would then force Π(cW)>0, producing a prime endpoint and contradicting terminality.
5. Finite evidence and control
| rank | mass | prime mass | flat Π | budget |
|---|---|---|---|---|
| 4,908 | 86 | 26 | 42.1117 | .382594 |
| 10,000 | 798 | 430 | 369.8065 | .053328 |
| 20,000 | 4,622 | 2,285 | 2,027.5406 | 0 |
| 40,000 | 11,792 | 5,000 | 4,912.5533 | .001415 |
Across all 38,692 audited rows from rank 1,309 through 40,000, the selector has no structural zero, no prime-empty row, and no budget failure; the largest observed budget is 0.923228708. The known prime-empty 20%-age control at rank 4,908 has budget 1.394526796, so the inequality is not an automatic artifact of the ledger.
Finite means finite. These values are calculated using complete primality/factor information to audit the proposed inequality. They do not prove that it holds on future rows or at a hypothetical terminal row.
6. Exact next theorem
Flat rooted centered-selector theorem. There are constants η>0 and N0 such that at every hypothetical first terminal row n≥N0 of the literal singleton-[7] trajectory, the wheel-filtered 18%-age selector has positive mass and
(R(bW)−R(cW))+ + (S(cW)−S(bW))+ ≤ (1−η)Π(bW).
This is a new rooted parity statement. A proof likely needs one lower-sieve scalar for the rough shortage and one fixed, centered prime-times-prime estimate for the semiprime excess. It does not require an unrestricted adversarial Type-II norm.
7. Method and trust
The project uses AI as a conjecture-and-falsification engine: propose an executable invariant, search for terminating and synthetic countermodels, formalize the surviving deterministic implication in Lean, audit the necessary analytic theorem against primary literature, and label every remaining oracle dependency. The purpose is not to turn a plausible transcript into a proof; it is to make logical failure cheap and explicit.