h277403 div10

Paul D. Hanna's sole COMMENTS conjecture in OEIS A277403 states:

a(n) is divisible by 10 for n>2 (conjecture).

The NAME field states:

E.g.f. satisfies: A(x - Integral A(x) dx) = x + Integral A(x) dx.

The FORMULA field introduces the primitive:

Let G(x) = Integral A(x) dx, then e.g.f. A(x) also satisfies:

The source is revision #21, with offset one and example beginning $A(x)=x+2x^2/2!+10x^3/3!+90x^4/4!+\cdots$. There is no source DOI, arXiv identifier or page number. The preregistration is #21746.

Statement echo

All declarations below belong to D5.S1.Recurrence.Residue.HannaIntegralCompositionDivTen.

| Source clause or interpretation | Lean counterpart | Scope | | --- | --- | --- | | Rational formal EGF | IsSolution parameters A, G | Every pair of rational formal power series | | Example has zero constant term | First conjunct of IsSolution | $A(0)=0$ | | Zero-constant formal integral | Second and third conjuncts of IsSolution | $G(0)=0$ and $G'=A$ | | Displayed defining equation | Fourth conjunct of IsSolution | $A(x-G(x))=x+G(x)$ | | Exponential coefficients, offset one | First conclusion of claim | $n![x^n]A\in\mathbb Z$ for every $n\ge1$, concluded rather than assumed | | Sole COMMENTS conjecture | Second conclusion of claim, proved by result | $n![x^n]A\in10\mathbb Z$ for every $n>2$ |

The existing IntegralEGFComposition.eCoeff supplies the literal factorial-scaled coefficient expression. The existing QuarticEGFFixedPoint.encode constructs rational series from coefficient sequences. Neither definition is duplicated. No integrality or desired congruence is assumed in IsSolution.

The settling node is D5/S1/Recurrence/Residue/HannaIntegralCompositionDivTen.result. It proves the entire published conjecture with the binding source interpretation. Its admission basis is open-problem-resolution (#21746; Proved).

The conclusion concerns every index. Finite agreement with the sequence does not establish it. Rational substitution does not permit factorial denominators to be inverted modulo ten. The proof therefore transports integral coefficient sequences and uses uniqueness over a commutative ring.

The private composition_top proves that changing the top outer exponential coefficient changes the composition coefficient by exactly the same amount, when the lower outer coefficients agree and the inner linear coefficient is one. The private seq_unique applies this identity by strong induction. The private a_equation verifies an integral recursively constructed solution; source_equation proves all four source clauses for the encoded series sourceA and sourceG.

For $P=x+x^2$ and $J=x^2/2+x^3/3$, the consumed polynomial identity is

$$P(x-J)-x-J=-\frac53x^3-\frac5{12}x^4+\frac13x^5+\frac19x^6.$$

The private residual_identity proves this identity; residual_coeff proves the exponential coefficient formula. The private p_mod makes the polynomial coefficient sequence a solution modulo ten. Ring-homomorphism transport (seq_map) and seq_unique identify it with the integral solution's reduction. The public result concludes integrality and divisibility for every source pair.

A rational source pair satisfying all four clauses and an index $n>2$ without an integer multiple-of-ten exponential coefficient would contradict result. The stronger assertion of divisibility by twenty fails for the independently computed value $a(3)=10$.

The mathematical evidence is the Lean module and its frozen module state record at Golden/Frozen/state/D5/S1/Recurrence/Residue/HannaIntegralCompositionDivTen.lean.json. The Scribe displays both public definitions and the full settling proposition.

The independent experiment is docs/reports/hanna-a277403-div10/ at de4bf43c9af7cabb0e9a46c584267cf950fb8beb. The verified immutable check.py was executed as python3 /tmp/op-h277403/experiment-check.py (exit 0); its SHA-256 is e1f1bb9fb343a3ac3f40d8e878fefc07e49ca10d4f6977701a81e4cff159e777. The script reproduces all 23 published terms at indices 1 through 23; independent rational substitution agrees through degree 24; integral and modular recursions modulo 2, 5 and 10 agree through degree 60, with divisibility checked at indices 3 through 60. It computes the complete polynomial residual, whose degree is at most six. These finite checks do not replace the all-index proof.

Escape audit unfinished: #22179 covers the sole new public theorem result. No valid Reg mirror is delivered. A faithful dependent-family registration still requires source reconstruction, variation, sensitivity and observational dependence evidence for the full universal rational-series and integer-witness telescope.

What the settlement shows

1. Proved, kernel-checked: composition_top, a_equation, seq_unique, p_mod and result give the all-index congruence through a unique integral triangular lift and a polynomial solution modulo ten. They use no factorial inverses modulo ten.
2. Proved, kernel-checked: the triangular identity composition_top and uniqueness seq_unique hold over arbitrary commutative rings; seq_map transports solutions through any ring homomorphism between such rings.
3. Proved, kernel-checked: source_equation proves that sourceA and sourceG satisfy all four source clauses. This nonvacuity evidence occurs on result's proof path.
4. Computed: the experiment in Evidence gives $a(3)=10$. Hence $20$ does not divide every $a(n)$ for $n\ge3$. Evidence kind: the exact arithmetic experiment and its recorded command, exit code and SHA-256.
5. Computed: the complete residual exponential coefficients in degrees three through six are $-10,-10,40,80$, zero elsewhere, with gcd $10$. Evidence kind: the complete polynomial calculation in that experiment; $\gcd(10,10,40,80)=10$.
6. Open: other Hanna parameter equations, additional congruences beyond consequences of divisibility by ten, and any literature novelty claim. No such extension is asserted by result.

The arbitrary-ring lemmas permit comparison in another modulus only after proving that the complete residual vanishes in that modulus. They do not assert that every modulus works. No source theorem explicitly depending on this conjecture was identified in the records read in #21746; the related functional identities retain their stated scope.

The bounded literature screen in #21746 read the source, related OEIS records, Hurwitz-series background and later OEIS settlement collections. It located no proof or refutation of A277403. Literature completeness is ASSUMED-UNVERIFIED: OpenAlex and Semantic Scholar returned HTTP 429, and the arXiv queries and indexed full-text checks were not an exhaustive corpus scan.

Bibliographic completeness and a novelty claim remain unverified for the stated search limitations. The unfinished escape registration is tracked in #22179; it is not a claim of validated registration. Other parameter equations and stronger congruences remain outside this settlement.