bibkey: hanna2026a396804 authors: Paul D. Hanna year: 2026 title: OEIS A396804 — E.g.f. satisfies A(x) = x exp(A^4(x)) doi: null url: https://oeis.org/A396804 claim: The entry conjectures a(n) congruent to n modulo four for positive n; superscripts denote composition. strata_touched:
- D5/S1/Recurrence/Residue/IntegralEGFComposition
- D5/S1/Recurrence/Residue/QuarticEGFFixedPoint
- D5/S1/Recurrence/Residue/QuarticEGFModFour license: citation-only triage: anchor
A396804: the modulo-four conjecture
Source checked on 2026-09-09 via the OEIS JSON endpoint. The entry was created
2026-06-09 and the retrieved revision is 23. It explicitly defines
A = X exp(A∘A∘A∘A) and a(n) = n! [x^n] A, with offset 1.
The modulo-four sentence is still marked Conjecture. Its first ten terms
are 1, 2, 27, 820, 41005, 2933046, 277407235, 33008920904, 4775699432745, 819537205428010.
The old modulo-three pattern is explicitly refuted at n=5 in the entry. The replacement six-cycle is a separate conjecture, not the target here. The seven distinct direct A references are A000169, A140054, A396799, A396800, A396803, A396805, A396806; A000169 occurs twice in the xref field.
Verified locator
- Entry: https://oeis.org/A396804
- Independently retrieved JSON: https://oeis.org/search?q=id:A396804&fmt=json (2026-09-09, revision 23; created 2026-06-09).
- Checked scope: the name/defining equation and compositional-iteration convention; offset and first ten terms; the independent modulo-four conjecture in the formula field; and the seven distinct direct A references.
The retrieved source defines the rational EGF characterized in QuarticEGFFixedPoint. Its conjecture is the all-positive-index residue statement proved by QuarticEGFModFour.mod_four. This locator does not attribute the new proof to OEIS, and it does not claim an independent rereading of every linked entry or every historical revision.
Search and implementation record
The earlier triage is recorded in oeis2026triage0909. This implementation
independently reread its A396804 row and paragraph, and the main OEIS JSON.
The triage seat’s report of reading all fields of all seven linked entries,
its supporting-text review, and its n≤40 computation remain attributed
reports, not repeated independent checks by this worker.
The first bind-only search inspected the frozen ordinary-series theorem
CompositionalIterateCongruence and the separate EGF/ODE construction
ExponentialImplicitParityPeriodThree. Neither gives the required EGF
composition integrality or this congruence. Pinned Mathlib v4.33.0 declarations
PowerSeries.coeff_exp, PowerSeries.coeff_subst',
PowerSeries.derivative_subst, and
PowerSeries.constantCoeff_iterate_derivative were read. They supply
coefficient and derivative calculus, not the target theorem.
An authenticated GitHub code search for A396804 language:Lean returned
total_count=0; an arXiv API exact-phrase query for
iterative exponential generating returned totalResults=0. Google returned
an access interstitial and Bing returned irrelevant flight results, so these
two searches supply no negative literature evidence. No proof of the
target has been found within this bounded search.
Before implementation the proposed escape was retained: the EGF coefficients
of A∘A∘A∘A-X should be divisible by four. The refinement uses the integer
chain-rule recurrence underlying Bell composition. For F=X exp(X), the
planned square formula is
n=Σ_k binomial(n,k) k k^(n-k).
Modulo two this reduces to n*2^(n-1). Writing F∘F=X+2H, integral composition
congruence should give F^4=X mod 4; contraction then transfers this to A.
The three Lean units now compile this route without sorry or added axioms.
The first compiled unit establishes factorial-normalized multiplication and
the chain-rule composition recurrence over arbitrary commutative semirings,
its compatibility with ring maps and finite coefficient prefixes, and the
preservation of natural/integer EGF coefficients under valid substitution.
Its file check exited 0. The baseline make lean exited 0 (12797 jobs).
The ensure receipt was seeded/clonefile, with stamp_miss=null, both layers
warm; the subsequent source/olean set difference was 3 missing of 3961.
Implementation evidence
The second unit constructs a : Nat → Nat, proves
(a n : Rat) = n! * coeff n A, constantCoeff A = 0, the exact fourfold
equation, and existence and uniqueness over PowerSeries Rat. The third
proves mod_four for all n≥1 and fourth_coeff_divisible for all n≥2.
All four principal declarations print only propext, Classical.choice,
and Quot.sound. The final full make lean exited 0 (12800 jobs), with
no warnings after removing unused convenience declarations and wrapping
long lines. The canonical Lean report exited 0 (delta added=3, recheck=3), with
peak RSS 4,880,592 KB. Ledger alignment exited 0: added=3, changed=0,
unchanged=1, conflicts=0. make emit exited 0 and generated the three
canonical mirrors, including the typed proved-resolution link. PR status
is recorded by the remote gate and the worker result envelope.
Lean computes a(0)=0, a(1)=1, a(2)=2, a(3)=27, and both sides of the nonempty residue example: 27 mod 4 = 3 mod 4 = 3. It also computes the second EGF coefficient of the fourth iterate as 8, with 8 mod 4 = 0. These private/anonymous sanity checks are companions to the unbounded proof, not independently admitted finite instances or escape witnesses.
A separate Fraction/Horner implementation was run through n=34. All first ten values agree with the caller, all A and B EGF denominators are one, and both modulo-four checks have zero failures in their stated ranges. In particular B(2)=8, B(3)=180 and B(4)=7240. These are diagnostic finite checks, separate from the unbounded Lean proofs.
Admission account
All three modules have admission_basis: escape-witness and utility: none
(unbounded symbolic mathematics). The active path is the new integral
composition recurrence and its prefix/reduction lemmas, then the natural
contractive fixed-point construction, then the new fourth-iterate arithmetic
of F=X exp(X). linear_fourth_mod_four feeds the approximation invariant
and mod_four. The proposed B(A) divisibility is proved as a companion;
it is not used circularly as a premise of the target.
The first module has no D5 imports. The second directly imports the first; the third directly imports the second and uses both preceding namespaces. There are no pre-existing frozen D5 theorem dependencies. Exact candidate module identities and the public-theorem account are recorded below. The motivating GID in the dossier is context, not a proof dependency.
Public-theorem proof shapes
This is a human assessment, not a claim that machine admission classifies
proof shape. The comparison baseline is commit
74e9341e5e38615754f82e99430a257a21c5a26c; new local declarations are inlined.
Every row has module admission basis escape-witness. Bind-only rows are
companions, not independently admitted modules. Edges read consumer →
prerequisite. The integrality interface is also an explicit named obligation
of the implementation task, paired with the independently proved A_equation.
For direct frozen-module dependencies, E has none, P imports E, M imports P. These letters expand to the following exact GID and statement_id pairs; all were newly frozen in this attempt. The pre-existing frozen dependency set is empty for every row. Mathlib is pinned upstream, not a D5 frozen node.
- E:
D5/S1/Recurrence/Residue/IntegralEGFComposition,sha256:7659badce7f3a2bb9681521c575cf07726e51bb3ba90baa36231036c4405e667. - P:
D5/S1/Recurrence/Residue/QuarticEGFFixedPoint,sha256:05c8ee2d2a8eb1624df659d6581634873aafdcda010603c06e252caa930a7454. - M:
D5/S1/Recurrence/Residue/QuarticEGFModFour,sha256:8358b8725387a04efe1275f6b153e9ba8d10de315635e6b9950dc286b340babf.
| Public theorem | proof_shape | escape_witness or named companion obligation / edge |
|---|---|---|
E.eCoeff_zero | bind-only | eCoeff_composition → eCoeff_zero |
E.eCoeff_derivative | bind-only | eCoeff_composition → eCoeff_derivative |
E.eCoeff_mul | bind-only | eCoeff_composition → eCoeff_mul; factorial/Cauchy normalization |
E.eCoeff_X_mul | bind-only | QuarticEGFFixedPoint.step_coeff → eCoeff_X_mul |
E.eCoeff_exp | bind-only | QuarticEGFFixedPoint.step_coeff → eCoeff_exp |
E.eCoeff_X | bind-only | QuarticEGFFixedPoint.eCoeff_iterate → eCoeff_X |
E.eCoeff_composition | content | strong induction identifies the new integral recurrence with rational substitution; QuarticEGFFixedPoint.eCoeff_iterate → eCoeff_composition |
E.composition_map | content | strong induction transports the recursive composition through an arbitrary semiring homomorphism; QuarticEGFFixedPoint.iterate_map → composition_map |
E.composition_congr | content | strong induction proves finite-prefix locality including shifted outer coefficients; QuarticEGFFixedPoint.iterate_congr → composition_congr |
E.natural_subst | content | eCoeff_composition and composition_map construct natural witnesses; natural_subst → eCoeff_composition; companion to preregistered composition-integrality obligation |
E.integral_subst | content | eCoeff_composition and composition_map construct integer witnesses; integral_subst → eCoeff_composition; companion to preregistered signed composition-integrality obligation |
P.eCoeff_encode | bind-only | A_equation → eCoeff_encode |
P.eCoeff_ext | bind-only | fixed_unique → eCoeff_ext |
P.constantCoeff_encode | bind-only | A_equation → constantCoeff_encode |
P.encode_composition | content | IntegralEGFComposition.eCoeff_composition; QuarticEGFModFour.linear_fourth_mod_four → private composition associativity → encode_composition |
P.iterate_congr | content | induction on iteration count using new prefix-local composition; step_contract → iterate_congr |
P.iterate_map | content | induction on iteration count using new composition_map; QuarticEGFModFour.mod_four → approximation invariant → step_map → iterate_map |
P.iterateComp_zero_coeff | content | induction constructs valid zero-constant iterates; eCoeff_iterate → iterateComp_zero_coeff |
P.eCoeff_iterate | content | induction combines new recurrence/FPS equivalence with valid iterates; step_coeff → eCoeff_iterate |
P.step_map | content | iterate_map and IntegralEGFComposition.composition_map; QuarticEGFModFour.mod_four → approximation invariant → step_map |
P.step_contract | content | new iteration locality yields one-degree contraction; approximation_stable → step_contract |
P.step_coeff | content | eCoeff_iterate identifies the source operator with integral step; A_equation → step_coeff |
P.approximation_stable | content | induction applies one-degree contraction at every stage; a_agrees → approximation_stable |
P.a_agrees | content | approximation_stable; a_fixed → a_agrees |
P.a_fixed | content | diagonal construction plus one-degree contraction proves a fixed point; A_equation → a_fixed |
P.a_zero | bind-only | A_equation → a_zero; zero boundary |
P.integral_coefficients | bind-only | preregistered named task obligation: exact source coefficient identification; eCoeff_encode normalizes independently constructed a : Nat → Nat |
P.A_equation | content | a_fixed constructs the actual rational fixed point; unique_solution → A_equation |
P.fixed_unique | content | induction on all finite prefixes using step_contract; unique_solution → fixed_unique |
P.unique_solution | content | constructed A with A_equation and fixed_unique; source existence/uniqueness obligation |
M.square_coeff | bind-only | linear_fourth_mod_four → square_even → square_formula → square_coeff; normalized Mathlib substitution and factorial identities |
M.linear_fourth_mod_four | content | new square_even and integral lift: square=identity+2h; h composed with square=h mod 2; mod_four → approximation_mod_four → linear_mod_four_fixed → linear_fourth_mod_four |
M.mod_four | content | linear_fourth_mod_four and the all-stage natural approximation invariant; target all n≥1; no finite cutoff |
M.fourth_coeff_divisible | content | linear_fourth_mod_four and the approximation invariant transferred through iterate_map; companion to proposed B(A) divisibility; not a premise of mod_four |
ASSUMED-UNVERIFIED
No claim of exhaustive literature or Lean-library search is made. This Library note is an evidence record; the proof is in the named Lean modules. The triage seat’s seven-page review, supporting-text review and integer Bell computation to n=40 remain attributed reports; they have not been rerun. The worker independently read the main JSON and recomputed through n=34. Not every OEIS revision was inspected. A supplemental GitHub Hurwitz query returned candidates that were not inspected and supplies no absence claim.
Identification with OEIS uses its retrieved equation and initial terms; the Lean kernel does not authenticate the external page. No first-proof priority, independent review or model diversity is claimed. This is one Codex main thread using the lean4 skill; later runner reviews lie outside this worker’s evidence. No modulo-three conjecture is resolved here.