Tebni's OEIS A350759 prime congruences

Mélika Tebni's OEIS A350759 revision 17 lists these COMMENTS conjectures:

For all p prime, (a(p) + a(p+1) - 2) == 0 (mod p),
a(p+1) == 1 (mod ((p+1)*p)).

Its FORMULA line is the exponential generating function exp(-1 + (1 + x)*(1 - log(1 + x))). The resolved Lean statement is D5/S3/Arith/Congruence/TebniA350759PrimeCongruences.claim: an integer sequence with that exact EGF exists, and every such sequence satisfies both congruences. The settling declaration is D5/S3/Arith/Congruence/TebniA350759PrimeCongruences.result, which proves claim.

Statement echo

The Lean sourceSeries is the published formal EGF, with PowerSeries.log ℚ interpreted as the formal log(1+X) and PowerSeries.subst taking the inner series first. IsSourceSequence a states that the EGF of the integer sequence a : ℕ → ℤ, with coefficients cast to ℚ, equals sourceSeries. The first conjunct of claim is existence of such an a; its second conjunct quantifies every such a, every natural p, and Nat.Prime p, then asserts Int.ModEq (p : ℤ) (a p + a (p + 1) - 2) 0 and Int.ModEq (((p + 1) * p : ℕ) : ℤ) (a (p + 1)) 1. The natural product is formed before its cast to ℤ, and the prime p=2 is included.

The source gives a concrete unbounded prime-congruence problem rather than a finite data fit. The module freezes the universal statement and records the published source attribution. The Library note is Library/RecurrenceComposition/tebni2022a350759.md; no DOI or arXiv identifier was found for this OEIS source.

Issue #22481 preregistered the two COMMENTS assertions as open. The bounded literature screen found no complete proof that subsumes both assertions. Paul D. Hanna's rising-factorial expansion in OEIS A176118 is prior art used by the argument. Literature completeness remains ASSUMED-UNVERIFIED; this dossier makes no global absence or priority claim.

The proof first obtains the exact rising-factorial expansion of the source EGF. After factorial scaling, the coefficient at every index n is 1+n*z for an integer z: the index-zero term is 1 and every other term is divisible by n. The exact differential equation for the source EGF gives an exponential generating-function convolution. For a prime p, interior binomial coefficients vanish modulo p; the endpoint is handled by Wilson's theorem, with p=2 handled in the same formal development. The all-index residues at p and p+1, together with coprimality of consecutive integers, yield the product modulus and the first congruence.

A failure of the Lean result, a source-sequence witness violating either congruence, or an invalid coefficient identity would falsify the settlement. Finite agreement alone is insufficient: the result quantifies over every natural index and every prime. The neighbouring statements listed below remain outside this result.

The kernel-checked result is in D5/S3/Arith/Congruence/TebniA350759PrimeCongruences.lean and is mirrored by Blueprint/D5/S3/Arith/Congruence/TebniA350759PrimeCongruences.scribe.cs. The supplied experiment is the-omega-institute/trureturing-experiments commit 194bc6dca7aebc1b906bb0842ce09af84976336c, script docs/reports/egf-prime-congruences/check.py, SHA-256 bcae63556a4e42055a697b6dad06b89254186075caaee867a777ac0797221375, exit code 0, final line ALL_CHECKS_OK. It reproduces all 24 OEIS data terms and a(9)=1000, compares the EGF and recurrence through 220 and expansion/Stirling through 60, and checks all 47 primes through 211; these are corroboration, not the universal proof.

The single typed settlement claim is OpenProblemResolutionClaim(tebni350759, Proved), attached to result only. The admission basis is open-problem-resolution (#22481; Proved); utility is none. The result has proof_shape: content and an unfinished escape audit tracked in issue #22632; no declared_validated status is asserted without the required CI current-job DTR reading.

What the settlement shows

• All-index mechanism — proved: every factorial-scaled coefficient of sourceSeries is integral and equals 1+n*z for an integer z, for every n including n=0. The unique k=0 term is 1; all other scaled terms lie in n*Z.
• Prime mechanism — proved: the exact source differential equation gives an EGF convolution. Interior prime binomial coefficients vanish modulo p; Wilson's theorem settles the endpoint, including p=2.
• Both named assertions — proved: combining the all-index residues at p and p+1 with the prime-successor residue and coprimality of consecutive integers proves both source assertions.
• Finite corroboration — computed: the supplied checker gives the 24 OEIS terms and the finite comparison readings described in Evidence. These checks do not replace the universal proof.
• Sharpness of naive extensions — computed: dropping primality gives p=4 with a_4=1, a_5=-4, first residue 3 modulo 4 and second-difference residue 15 modulo 20. Strengthening the successor residue to modulus p^2 fails at p=7: a_8-1=-168 has residue 28 modulo 49.
• Surviving neighbouring questions — open: refined composite-index conditions, higher prime-power congruences with additional hypotheses, and primality-characterization claims for A345652 are not settled here.

The literature screen is bounded and its completeness is ASSUMED-UNVERIFIED. No worldwide absence, priority, or originality claim is made. The finite checker does not establish the universal theorem. Composite-index refinements, stronger prime-power congruences, and the A345652 characterization remain open.