Bala's A193237 congruences modulo five and seven

Peter Bala's FORMULA line in OEIS A193237 states: “Conjectures: a(5n+4) == 0 (mod 5) and a(7n+5) == 0 (mod 7) (both checked up to n = 200).” The source is preregistered in #22112. The companion claim is #22113.

Write $T_j=j(j+1)/2$ and $F(x)=\sum_{j\ge0}(2j+1)3^j(-1)^{T_j}x^{T_j}$. The question concerns the constant-one reciprocal cube root $A(x)=F(x)^{-1/3}$ and every natural index, without a finite cutoff.

Statement echo

| Source clause or convention | Formal counterpart | Scope | | --- | --- | --- | | The displayed source series | BalaA193237ModFiveSeven.F | Its degree-$m$ coefficient sums the literal source weights over $j<m+1$ with $T_j=m$. The truncation is exact because $T_j=m$ implies $j\le m$. | | The constant-one reciprocal cube root | BalaA193237ModFiveSeven.IsGF | Rational power series with constant coefficient one and $A^3F=1$. | | A generating function exists | First conjunct of claim | An explicit integral inverse gives a rational normalized solution; the universal clause is nonvacuous. | | Coefficients of the sequence | Integer sequence quantified in claim | Every coefficient of every normalized rational solution equals the cast of its corresponding integer value. | | Modulo five | First divisibility in claim | $5\mid a(5n+4)$ for every $n\in\mathbb N$. | | Modulo seven | Second divisibility in claim | $7\mid a(7n+5)$ for the same universally quantified $n$. |

The existence and universal-integrality clauses make the source's normalized generating-function interpretation explicit. The source-specific definitions are literal; the shared proof uses BalaA193237ModFiveSeven.triangular with the source weights.

D5.S1.Recurrence.Residue.BalaA193237ModFiveSeven.result proves the full claim. Its admission basis is open-problem-resolution (#22112; Proved). Both family results are symbolic statements over all natural indices.

The source supplies finite evidence but asks for unbounded congruences. Integrality and rational uniqueness are needed to connect the residue calculation to every normalized rational solution.

The shared BalaA193237ModFiveSeven.resolve combines integral-root construction, triangular support, Frobenius and rational uniqueness. Its coefficient-contraction step applies D5.S1.Recurrence.Invariants.PowerSeriesNormalizedContraction.exists_unique_fixed. The A193237 result supplies the literal source weights and verifies their positive-degree divisibility by nine.

The claim would fail if no normalized rational solution existed, if a normalized rational solution had a nonintegral coefficient, or if either asserted divisibility failed at any natural index. The theorem has no finite cutoff.

The settling declaration is D5.S1.Recurrence.Residue.BalaA193237ModFiveSeven.result. The axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}. The Scribe displays the complete claim and attaches one Proved resolution claim to this result.

The escape audit is unfinished for BalaA193237ModFiveSeven.resolve and both family results; #22201 records the missing typed family realization, reconstruction, sensitivity and observational-dependence evidence. No declared_validated registration is claimed.

The independent finite check is the pinned experiment directory. The command python3 /Users/auric/trureturing-experiments/docs/reports/bala-a193237-a193236-mod5-mod7/check.py --bfile-dir /Users/auric/.op-scratch/op/bala193237/src exits $0$ and ends ALL_CHECKS_OK. The script SHA-256 is 7613bcfbf58f29e849b82b9e80a311bf05c535445c74477217e58e8e83a44ad7. The inputs are the stored official OEIS b-files, with SHA-256 4ba6b426b1b859a65152b1e764a60d1683f857f1eeb710c63fe4f11a9a07bde5 for A193237 and 5801e979042bf2f5d7a06e097706bcedeb4f60b2eebcc3fe4e98886eb524d06b for A193236. For each sequence, all b-file coefficients at indices $0\ldots1000$ agree; the congruence checks cover $n=0\ldots700$ modulo five and $n=0\ldots500$ modulo seven. The support and transfer checks reach degree $3505$. These are finite computations independent of the unbounded proof.

What the settlement shows

1. Proved, kernel-checked: both original unbounded OEIS claims, including existence and universal integrality under the literal binding definitions, by BalaA193237ModFiveSeven.result and BalaA193236ModFiveSeven.result.
2. Proved, kernel-checked private helper: for any integer weights $w$ and integral power series $A$, the assumption $A^3\operatorname{triangular}(w)=1$ implies both congruences. The private triangular_inverse_congruences in BalaA193237ModFiveSeven is used by resolve; it assumes neither desired congruence and does not need the divisibility-by-nine hypothesis.
3. Proved, kernel-checked private helper: for every integer power series $F$ with constant term one and positive-degree coefficients divisible by nine, an integral normalized reciprocal cube root exists. The private integral_inverse_of_nine, consumed by resolve, proves this general statement. The construction writes $F=1+9H$, obtains $U=H-3U^2-3U^3$ by coefficient contraction, forms $B=1+3U$ with $B^3=F$, and inverts $B$.
4. Proved, kernel-checked private helpers: modulo five, the weighted triangular series has support in ${0,1}$ and its cube misses residue four; modulo seven, its support is in ${0,1,3}$ and its square misses residue five. These are triangular_support_five, cube_support_five, triangular_support_seven and square_support_seven in the shared module. prime_power_support, mul_prime_power_vanish, transfer_five and transfer_seven give the Frobenius transfer. All these helpers occur on the settling proof's dependency path.
5. Computed: the experiment in Evidence checks both official b-files through index $1000$, with $701$ mod-five cases and $501$ mod-seven cases per source through degree $3505$, exit $0$, final line ALL_CHECKS_OK. Its command, immutable revision and script SHA-256 are specified there.
6. Open: other moduli, higher prime-power congruences and asymptotics are outside these conclusions.

The decisive mechanism is the missing-residue support followed by Frobenius. It is independent of the nonzero weights once an integral reciprocal cube root exists. Divisibility by nine is a sufficient construction hypothesis, not a claimed necessary condition. Rational uniqueness transfers the constructed integer coefficients to every normalized rational solution. The same route settles the companion sequence. No source result depending on the conjectures was identified in the recorded literature screen; no additional downstream theorem is asserted here.

Literature completeness is ASSUMED-UNVERIFIED. The screen in #22112 and #22113 covers both OEIS entries, relevant integrality papers, arXiv identifier and author searches, and bounded public-code and question-site searches. Rate-limited, capped and unusable searches do not establish absence of prior proof. The finite experiment has only its stated range. Four-slot escape registration is unfinished at #22201.