bibkey: oeis2025a388724
authors: OEIS Foundation Inc.
year: 2025
title: OEIS A388724
doi: null
url: https://oeis.org/A388724
claim: Column sums of strictly superdiagonal reversed partitions are conjectured to be A000245, with an index shift.
strata_touched: []
license: citation-only
triage: anchor

OEIS A388724

Verified locator

https://oeis.org/A388724, complete JSON revision 12, retrieved 2026-09-09. The formula field states: “Conjecture: Column sums are A000245.” The definition uses one-based strict inequalities y_i > i. The source was created in September 2025; the generating function is dated October 4, 2025. The caller’s 2026 dating is corrected to the retrieved source date.

https://oeis.org/A000245, complete JSON retrieved on the same date, has offset 0 and DATA 0,1,3,9,28,90,…, with formula a(n)=C(n+1)-C(n). Consequently the proposed column identity is column(k)=A000245(k-1) for k>=1; column(0)=0. The caller’s supplied 0,0,1,3,… is the column sequence including k=0, not A000245 at its actual OEIS offset.

Preregistration and provenance

Skill context: lean4, within the caller’s consensus-rnd:sshx implementation stage. One Codex worker performs investigation, implementation and self-checks; no independent review or multi-model consensus is claimed. Baseline: 7547debb97761296d4d934b9c87ada4b90729cea; branch lane/math/a388724-catalan. No atom ID was supplied; the explicit OEIS brief supplies the obligation. Read CLAUDE.md, both agent brief notes and all five Compositions modules.

The proposed main theorem counts all weakly increasing natural lists, including empty, satisfying i+1 < y[i] <= k at every zero-based index i. The target cardinal is catalan k. First attempt only pinned Mathlib and frozen declarations with normalization; a successful bind-only reduction stops implementation without a new module. Otherwise the proposed new formal content is a Catalan decomposition or a bijection for these lists. The mathematical Catalan counting fact is classical folklore, not a claim of a new mathematical theorem. The possible contribution is formalizing it in the needed shape and closing the recorded OEIS column assertion.

The literature decision depends on a proof, not mere prior occurrence: a published proof of the bridge triggers a Library-only outcome; conjectural restatements do not. The completed xref investigation and resulting decision are recorded below.

Cache receipt

make lean-cache-ensure exited 0: status=present, method=none, stamp_miss=null, project_olean_state=warm, mathlib_olean_state=warm, mathlib_missing_olean_files=0. No cold bare lake invocation was made. The receipt and untruncated root JSON files are in the worker-owned attempt: /var/folders/wv/ht3wzsj138b4sxl3q4t0xdr40000gn/T/consensus-rnd/sshx/a388724-impl-0909/attempt-1.

Published proof and decision

Decision: Library-only; published-proof specialization. This is a literature stop, not a successful bind-only probe or a new open-problem resolution claim. The full publisher HTML was opened: M. Archibald, A. Blecher, S. Elizalde and A. Knopfmacher, Subdiagonal and superdiagonal partitions, Afrika Matematika 36, article 77 (2025), DOI https://doi.org/10.1007/s13370-025-01282-0. Crossref and the publisher give publication date 2025-04-07, before A388724. The relevant proved statements are Theorem 2.3 and its proof, together with Lemma 1.3 and its proof. This decision is based on those proofs, not on the title, a matching sequence, or an unproved OEIS formula.

Here is the complete specialization. Fix k>=2. Subtract 1 from each part of a nonempty strict-superdiagonal increasing partition y of maximum k. The resulting positive increasing partition x has x_i>=i and maximum m=k-1. Adding 1 is its inverse. Thus strict maximum k and weak maximum m are equinumerous, across all weights; weight preservation is unnecessary.

The proof of Theorem 2.3 establishes a bijection from weak superdiagonal partitions with largest part m to pairs (P,h), where P is a Dyck path of semilength m and 0<=h<ell(P). Here ell(P) is the number of final E steps. It appends E steps to the partition boundary until (m,m), and records how many were appended. Its explicitly proved inverse deletes those final steps. Therefore the desired column count is L_m = sum_{P in D_m} ell(P).

Let C(z)=sum_{m>=0} C_m z^m and F(z,x)=sum_{m>=0} sum_{P in D_m} x^ell(P) z^m, with ell(empty)=0. Specializing the polynomial recurrence proved in Lemma 1.3 at q=1 gives F(z,x)=1+xzF(z,x)C(z), hence F(z,x)=1/(1-xz*C(z)). Differentiate the finite row polynomials in x and evaluate at x=1:

L(z) = sum_{m>=0} L_m z^m
     = z*C(z)/(1-z*C(z))^2 = z*C(z)^3.

The Catalan equation C=1+zC^2 implies z^2C^3=(1-z)*C-1. Coefficient comparison yields L_m=C_(m+1)-C_m for every m>=0. This is exactly A000245(m), by its verified defining formula and generating function. Consequently

column(0)=column(1)=0,
column(k)=C_k-C_(k-1)=A000245(k-1)  for k>=1.

For a list counted by the caller’s bounded family B_k, a nonempty length r satisfies r<y_r<=k, so r<k. There are finitely many such lists. The empty list gives B_0=1; every other list has a unique maximum j in 1..k. Thus B_k=1+sum_{j=1..k}(C_j-C_(j-1))=C_k, including B_1=1. This proves the caller’s Proposition A as a mathematical consequence of the cited published proof. The paper does not explicitly name A388724 (it predates the entry), and the coefficient specialization above is written here, not quoted as a numbered corollary from the paper. The stronger weighted enumeration and its bijection are already proved there; no new combinatorial argument is needed to obtain the column identity.

The choice of route is therefore the published Dyck-path bijection: it already records maximum part and the exact fibre size ell(P), which makes the strict case a parameter shift followed by Catalan algebra. A new inductive counting proof would reprove this known enumerative content. Per the task’s explicit downgrade instruction, no Lean module, Scribe resolution claim, Problems theorem dossier, freeze or cover is created.

The printed OEIS generating function fails its own data

All fields of A388724 were read, including the Rascoe formula and program. As literally printed, putting q=1 and writing C_j=Ca(j,1) gives

P_0=1,
P_m=t/(1-t) * sum_{j=1..m} t^j*C_(j-1)*P_(m-j),
S=sum_{m>=1}P_m=t^2*C(t)/(1-t-t^2*C(t)).

This formal specialization is coefficientwise valid: ord_t(P_m)>=m+1, so only finitely many m contribute to a fixed t coefficient. Its first coefficients are 0,0,1,2,5,13,36,105,320,1011, whereas the actual columns are 0,0,1,3,9,28,90,297,1001,3432. In particular [t^3]S=2, not 3. More locally, the printed bivariate formula misses q^5*t^3, which is the valid partition [2,3]. Thus the printed formula does not imply the column conclusion and is not used as proof.

The displayed PARI program uses pl[m-j]/(1-tq^(m-j)) instead. With pl representing Pr, this is not the P(m-j) defined in the formula: that P contains the additional factor tq^(m-j). The observation identifies the specific discrepancy; this worker has not edited OEIS or asserted which historical transcription caused it. The published proof above is independent of this error.

Complete OEIS cross-reference receipt

Both roots’ comment/formula/xref fields contain 60 distinct A-numbers; including A388724 itself gives 61 complete entries. Every entry was fetched from https://oeis.org/search?q=id:Axxxxxx&fmt=json and saved unmodified, with all fields retained. oeis-manifest.json records the exact URL, file, byte size, revision and SHA-256 for each. All 61 final receipts have status=ok. The initial Python urllib requests received HTTP 403; the same URLs fetched successfully with curl. The failed manifest is retained separately. No missing response was treated as an empty entry.

A388724 contributes these 34 references: A000009, A000041, A000245, A000700, A001522, A003106, A003114, A025157, A052335, A052337, A064428, A114088, A115720, A115994, A227543, A237979, A238352, A238394, A238395, A238873, A238875, A352828, A352830, A352833, A355529, A368100, A370585, A370592, A370593, A387118, A387880, A388710, A388711, A388713.

A000245 contributes these 26 references: A000108, A000344, A000588, A001006, A001392, A001622, A002057, A003517, A003518, A003519, A005322, A007001, A007054, A009766, A014137, A030237, A033184, A047072, A059365, A067323, A099039, A099364, A106566, A130020, A154558, A214292.

The relevant proof locator is present in A227543, A003114, A238873 and A238875. A387118 and A388711 contain different conjectural assertions; those do not constitute a proof of this target. A388713 concerns the weak version, A387880 the subdiagonal version, and A238394 the strict row sums. A000245 supplies the actual offset, Catalan difference and z*C(z)^3 formula. The other retrieved entries supply related partition, ballot, Catalan, transform or unrelated reference context; none is used to replace the published Theorem 2.3/Lemma 1.3 proof chain with a conjectural restatement.

Pinned library probe

The pin is Mathlib db584cd6d46c92f209a44c0f1c829460d327499d with Lean 4.33.0. Pinned Mathlib has Catalan/Basic.lean and Catalan/Tree.lean; the old Combinatorics/Enumerative/Catalan.lean is a deprecated import facade. The exact candidate declarations read in source are catalan_succ, catalan_succ’, catalan_eq_centralBinom_div, BinaryTree.treesOfNumNodesEq_card_eq_catalan and DyckWord.card_dyckWord_semilength_eq_catalan. The latter counts DyckWord subtypes of fixed semilength; it does not take the caller’s list predicate.

The five frozen Compositions modules were read in full. ChoosableInitialIntervals proves weak choosability/diagonal equivalence, with no Catalan count. The other four concern adjacent or alternating sums and odd/distinct partitions. Searching D5 for superdiagonal/subdiagonal/parking/Dyck and the pinned Mathlib for Catalan/catalan/parking-function/subdiagonal produced no existing list-family cardinal theorem or equivalence that closes Proposition A by direct instantiation and normalization. The relevant Mathlib candidate files were read. This is no bind-only closure found in the searched scope, not proof of nonexistence. No Lean closure was obtained or claimed. No direct frozen dependency is used in a new theorem, so the public-theorem inventory and frozen-dependency inventory of this change are empty; escape_witness and admission_basis are inapplicable to this Library-only decision. A broader third-party Lean search was not pursued after the published-proof stop condition was established; no search-complete claim is made for it.

Evidence

The worker independently enumerated positive weakly increasing partitions for n=0..11, applied the one-based strict predicate, and grouped by exact maximum. All 78 terms agree with the full A388724 DATA (including the caller’s first 65). Thus n=0..11 produces 78 triangular positions, not 65; the caller’s reported positive control is a prefix of that window. This independent finite calculation is not a Lean kernel proof.

For k=3 the actual bounded set is [], [2], [3], [2,3], [3,3]. The invalid list [2,2] fails at one-based i=2, since 2 is not greater than 2. At k=0 and k=1 only [] qualifies for the bounded set, and neither column has a nonempty witness, giving columns 0 and 0. A separate Dyck-prefix enumerator gives final-descent sums 0,1,3,9,28,90,297,1001,3432 for semilengths 0..8, agreeing with the shifted columns. The exact output is in enumeration-evidence.json in the attempt directory.

Not claimed

The caller reports a 65-term triangle positive control, column counts k=1..8 and bounded counts k=0..9, and explicitly reports having done no literature research. Those caller readings were not kernel proofs. The worker’s independent readings and literature investigation are distinguished above. No new Lean theorem or kernel proof of Proposition A or the columns was produced. No novelty, priority, new open-problem resolution, exhaustive literature absence, exhaustive third-party Lean search, independent review, multi-model consensus, or implication to a larger conjecture is claimed. Unopened papers linked by OEIS remain ASSUMED-UNVERIFIED. No OEIS correction was submitted. The paper’s weak maximum-part bijection and Lemma 1.3, rather than its different subdiagonal Theorem 3.2 alone, are the published evidence for the downgrade.

Delivery receipts

The prescribed local sequence passed: make lean LAKE_JOBS=3 (exit 0, 12774 jobs), make lean-report LAKE_JOBS=3 (exit 0), then make emit (exit 0, zero changed Blueprints). Report SHA-256: fcfd2c7189b6a9910d908443078e55b0dfa48067191d8e764b1990bfc352f1f3. These verify the unchanged Lean tree and the Library note’s repository integration, not a kernel proof of the target. No OpenProblemResolutionClaim is added, so ledger-align is inapplicable. Logs are make-lean.log, make-lean-report.log and make-emit.log in the attempt directory.

A fresh fetch still found dev at the pinned baseline 7547debb97761296d4d934b9c87ada4b90729cea; git merge-tree with the pushed research commit succeeded without conflict. The only tracked change is this Library note. The five-file Compositions directory is unchanged, and no new domain is created. Remote PR and final gate results are recorded in the worker result envelope after the canonical pr-open operation completes.