slug: oeis-a091190-somos-prime-integrality
bibkey: hanna2004a091190
doi: null
url: https://oeis.org/A091190
triage: theorem
motivation_gids:
  - D5/S1/Recurrence/Invariants/SomosPrimeIntegrality

The Somos prime integrality family in OEIS A091190/A091200

Problem

More generally, given A(x) satisfies xA(x)^p = B(xA(x^p)) where B(x) = x/(1-p*x), then it appears that A(x) is an integer series only when p is prime.

For every natural $p\ge 2$, a rational solution with $A(0)=1$ exists for $xA(x{)}^p=B(xA(x^p))$, where $B(x)=x/(1-px)$. Every such solution has integer coefficients if and only if $p$ is prime. The coefficientwise expression for $B$ is inlined in IsGF.

Statement echo

Motivation

The externally stated OEIS conjecture is preregistered in #18793. The settling declaration is D5.S1.Recurrence.Invariants.SomosPrimeIntegrality.result; its admission basis is open-problem-resolution (#18793; Proved).

Gap

The preregistration records the OEIS source and literature screen. The checked entries cite no proof. Literature-screen completeness is ASSUMED-UNVERIFIED. The mathematical gap is discharged by the settling declaration under the displayed coefficient rings and normalizations.

Route

The geometric denominator identity gives the residual $A^p(1-pxA(x^p))-A(x^p)$. Prime Frobenius congruence makes integral corrections possible through the shared lifting construction. At a composite exponent the low-degree differential recurrence gives a contradiction modulo the least prime divisor. General.prime_of_integral is the necessity step used by result.

Falsifier

A prime exponent with a nonintegral normalized solution or a composite exponent with an integral normalized solution contradicts result.

Evidence

The Lean module and its Blueprint Scribe carry the exact statement. The axiom closure is contained in {propext, Classical.choice, Quot.sound}. The frozen module record is Golden/Frozen/state/D5/S1/Recurrence/Invariants/SomosPrimeIntegrality.lean.json. Escape audit unfinished: #19794; no compiled registration is delivered.

Publicized owner audit targets under #19794: D5.S1.Recurrence.Invariants.AbsoluteReciprocalGeometricParity.agree_mul; D5.S1.Recurrence.Invariants.CubicFifteenSubstitutionParity.agree_iff; D5.S1.Recurrence.Invariants.CubicFifteenSubstitutionParity.agree_pow; D5.S1.Recurrence.Invariants.CubicFifteenSubstitutionParity.agree_subst_order; D5.S1.Recurrence.Invariants.CubicFifteenSubstitutionParity.power_two_one. Four-slot registration is unfinished for each target.

Experiment

Pinned experiment. Command: python3 check.py in that directory; exit 0; script SHA-256 4af4904971adab029c3b7b91644f6a4ab789f41c203eff909726101f246257e5.

Computed: for prime $p\le 29$, integrality holds through order 14 when $p<10$ and through order 8 otherwise. For composite $p\le 30$, the first noninteger coefficient occurs at the least prime factor $q$ and equals ${\prod }_{i<q}(1+ip)/q!$. At $p=25$ the value is $424099/5$. The first 14 terms match A091190 and A091200.

Declaration classification

Same-delivery helpers are expanded for classification; consumed bind-only helpers are proof organization. The table names live consumers and the surviving construction or induction witness.

Triage

What the settlement shows

Proved in Lean: the assertion covers every exponent $p\ge 2$ and every normalized rational solution, with rational existence for all those exponents and both directions of integrality iff primality. The low-degree obstruction supplies the necessary direction. A uniform location or formula for the first noninteger coefficient remains outside the formal conclusion.

ASSUMED-UNVERIFIED

Literature completeness and originality are not established. The other source families and uniform extensions marked open above are outside this settlement. Four-slot escape registration remains unfinished under #19794.