bibkey: oeis2026a392698
authors: OEIS Foundation Inc.
year: 2026
title: OEIS A392698
doi: null
url: https://oeis.org/A392698
claim: The partition-count conjecture on A392698 requires an index shift; the target is the number of distinct-part partitions of n+1.
strata_touched: []
license: citation-only
triage: anchor

OEIS A392698

Provenance and scope

Skill context: lean4, within the caller’s consensus-rnd:sshx implementation task. One Codex worker reads sources, explores proofs and runs local checks. No independent review or multi-model consensus is claimed. The caller’s hand proof and enumeration are input evidence, explicitly distinguished from worker checks. Baseline: c3c261a08c95c414417288ea9cac43ba629f42af. No atom identifier was supplied, so show-atom and atom coverage are not applicable. The explicit OEIS brief supplies the source obligation.

This is a first-tier recent OEIS conjecture. Before creating a module, try pinned Mathlib binding and inspect every A-number in the source comment, formula and xref. A successful binding stops implementation; an already published equivalent statement leads to a Library-only result. Otherwise the required endpoint is the unbounded count equality, including n=0. A partial structural module is not an authorized endpoint.

The proposed escape witness is the odd/even structural decomposition of integer alternating partial sums, preregistered by the caller. Its use in an elaborated count proof and all four clause 3.2 conditions remain to be checked.

Source correction

The worker directly opened revision 6 of A392698 on 2026-09-09. Both comment and xref say these partitions are counted by A000009 without a shift. The entry’s DATA contains 3 and 4, whose reversed prime-index partitions are [2] and [1,1]. Both satisfy the defining condition, so the weight-two count is 2, whereas A000009(2)=1. The task concerns the corrected statement with A000009(n+1); the unshifted source sentence is not a proved result.

For decreasing positive q, use integer s_0=0 and s_j=q_j-s_(j-1), and require s_1,…,s_k to be pairwise distinct. The zeroth term is excluded. The source examples are [2,2,1] -> [2,0,1] and [3,2,2,1] -> [3,-1,3,-2].

Evidence

The first command was make lean-cache-ensure, exit 0. Its complete receipt:

{"status":"present","worktree":"/Users/chronoai/trureturing-a394454-centralbinom","donor":null,"method":"none","reason":null,"stamp_miss":null,"pin_sha256":"sha256:6c4c682ffba051b5744fe7a75ccc99d7f3b20227b3b026f392f3315be0adaa4e","clonefile_errno":null,"clonefile_errnos":[],"clonefile_attempts":0,"clonefile_cleanup_error":null,"mathlib_missing_olean_files":0,"mathlib_missing_olean_samples":[],"archive_status":"not_attempted","archive_mode":null,"archive_skip_reason":"project olean state is warm","archive_reason":null,"archive_producer_commit_sha":null,"archive_workflow_run_id":null,"mathlib_olean_state":"warm","mathlib_olean_probe_error":null,"project_olean_state":"warm","project_olean_probe_error":null}

Read CLAUDE.md, both agent briefs, agents/CONTEXT.md and both complete Compositions modules. The checked-out HEAD is exactly the supplied baseline; the worktree was clean. PR #6585 supplies the seven-file delivery template. The pre-existing caller probe targets positivity of the integer alternating sum of an odd-length prefix. Its reported outcome is open, 44 seconds; that one-term search is not a proof-shape classification.

Initial source fetch succeeded at the JSON URL below. At this first checkpoint, repository, Mathlib, ecosystem and full xref checks were still in progress; the later sections record their outcomes. An initial combined rg command named the nonexistent Mathlib Partition.lean path and exited 2; its output is not counted as a successful Mathlib search. The actual partition files are Partition/Basic.lean, GenFun.lean and Glaisher.lean.

Verified locator

• URL: https://oeis.org/A392698
• Opened JSON: https://oeis.org/search?q=id:A392698&fmt=json
• Checked on 2026-09-09: revision 6, definition, examples, DATA, comments and xref; author Gus Wiseman, Jan 26 2026, creation Jan 29 2026.
• Equivalent shifted conjecture: https://oeis.org/A392703
• Opened JSON: https://oeis.org/search?q=id:A392703&fmt=json
• Checked on 2026-09-09: revision 16, comment beginning “For partitions instead of compositions”; its status word is “appear”.

Unclaimed

No general theorem or count identity has been proved in Lean in this attempt. No claim of provability, exhaustive literature search, publication priority, or implication to any larger conjecture is made. The caller did not perform a targeted literature search. Pages not yet opened are ASSUMED-UNVERIFIED.

Xref decision checkpoint

The source comment/formula/xref contains 42 distinct A-numbers, all requested individually at the prescribed JSON endpoint. In A392703 the worker opened this explicit comment:

For partitions instead of compositions we appear to have A000009(n), trimmed A000009(n+1); see A392698.

This is already a published equivalent statement of the corrected target. The word “appear” matters: it is a conjectural statement, not a proof. Under the brief’s explicit rule “if an equivalent statement is found, only write a Library note”, this attempt is downgraded to Library-only. No Lean module, frozen state, Problems theorem entry or resolution claim is created. The worker will finish the remaining xref inspection and the required pinned-Mathlib bind-only attempt before finalizing this note.

The source correction is therefore independently supported by another entry of the same author. Neither that support nor the finite DATA check resolves the conjecture. No published proof has been identified at this checkpoint.

Completed xref inspection

The worker extracted the set with the structured query [.[0] | (.xref[]?, .formula[]?, .comment[]?) | scan("A[0-9]{6}")] | unique. The result contains exactly 42 identifiers. Each was fetched separately with curl -fsSL --max-time 25 'https://oeis.org/search?q=id:<ID>&fmt=json'; all 42 fetches exited 0 and returned parseable entries with the requested number. The source itself was also retained, for 43 JSON snapshots in the runner attempt directory. No recursive closure of the xrefs was requested or claimed.

The following is the complete inspected set. The worker read every entry’s name, comments and formulas, and searched the additional xref/reference/link fields for the target, first sums, alternating sums and distinct partitions. “Other” below means no equivalent target assertion identified in those inspected fields; it does not certify the contents of linked papers.

A392704 explicitly defines reversed partitions as weakly increasing. Some rank xrefs in this family mix the reversed and non-reversed cases. This note uses A392703’s explicit partition comment and A392698’s decreasing-part definition; it does not identify A392704 with the requested count.

Pinned-library attempt and proof shape

Repository search, fixed baseline: rg -n -i 'A392698|distinct.*alternating|alternating.*distinct|first.sums' D5 -g '*.lean' returned 7 lines, in the existing first-sums module and two unrelated files. The positive control rg -n '\b(firstSums|IsFirstSums)\b' D5/S1/Words/Compositions returned 17 lines. These are textual search receipts, not semantic dependency claims. Both complete neighboring modules were read; neither states this integer alternating-prefix characterization or the shifted count.

The two neighbor state identities were read from Golden/Frozen/state: ChoosableInitialIntervals has sha256:2406015af8528d11f15b1a7cd4ea422f1b83e81c2f4a47c1c55482ebbc0a8d30; FirstSumsPartitionCharacterization has sha256:84e432b8912426418215248825fc502114361397419f3c4016f7a62859a1e5ed. They are examples of local style, not direct proof dependencies. Their scopes are initial-interval representatives and natural first-sums with a lower bound of two, respectively.

Pinned Mathlib is db584cd6d46c92f209a44c0f1c829460d327499d (v4.33.0). Inspected Partition/Basic.lean, the partition-related hits in GenFun.lean and Glaisher.lean, and Analysis/SpecificLimits/Normed.lean’s alternating series theorems. Nat.Partition.distincts gives the right-hand finite set; card_odds_eq_card_distincts is Euler’s same-weight identity. The alternating series bounds require a limit and global monotonicity; those facts are not provided by the target’s finite-list hypotheses. None of these displayed statements directly supplies the required odd-prefix strict positivity. One intermediate path query also named nonexistent Analysis/SpecificLimits/Alternating.lean and exited 2; the successful full Mathlib rg and subsequent Normed.lean read replaced that invalid query.

After the Mathlib inspection, authenticated public GitHub code searches for "A392698" language:Lean (limit 20) returned 0 paths, and "alternating" "partition" language:Lean (limit 30) returned 30 candidates, mostly alternating forms, group theory, list definitions and mirrors. These are bounded discovery results; the broad query reached its limit and does not establish absence in the Lean ecosystem. No third-party library was imported. Target-specific formalization stopped at the xref decision.

The worker’s first BindOnly.lean had invalid ASCII binder syntax and exited 1 before elaboration; it is not a negative mathematical result. The corrected probe uses forall x, List.Mem x q -> 0 < x. It imports only Mathlib, retains the exact integer prefix target, and tries exact?, simp_all, omega and aesop in separate solve branches. It exited 1 with an unsolved target and an aesop exhaustion warning. The target elaborated successfully. Outcome: open, not a successful binding and not evidence that no library composition can prove it.

There are no delivered public Lean declarations, so there is no per-theorem proof-shape table to certify. Conservative clause 3.2 admission screening of the unproved candidate is bind-only: direct frozen dependencies none, escape_witness null, admission_basis none. This is not a claim of a found bind-only proof. The four proposed-witness obligations are separately open: (i) no elaborated count-proof dependency closure exists; (ii) automation failure does not prove non-projectability; (iii) the proposed structural statement differs informally from a cardinal equality, but no final proof has been elaborated; (iv) no live count derivation using it exists. Therefore no content/admission or resolved-open-problem claim is made.

Worker boundary checks

Boundaries.lean, outside the repository, imports only Mathlib and defines the recurrence with an Int accumulator. Its kernel checks exited 0 and its evaluation output was exactly:

[2, 0, 1]
[3, -1, 3, -2]
[]
[2]
[1, 0]

The script checks Nodup for the first example, its negation for the second, and Nodup for [], [2] and [1,1]. It also checks distinctness of the two weight-three witnesses [3] and [2,1], and the weight-one singleton [1]. These are boundary diagnostics, not a general count proof or frozen finite certificate. The caller’s n=1..14 enumeration was subsequently included in the worker’s independent finite check below.

The brief’s prose says the even-position s-values are increasing. Its own formula s_2-s_4=q_3-q_4 >= 0 instead says decreasing; the stated B=-s increasing convention is correct. The worker’s Lean diagnostic checks [4,3,2,1] -> [4,-1,3,-2], where the even values are -1,-2. This sign-wording correction does not alter the requested distinctness condition.

Unformalized bijection route

The worker noticed the following simplification while reading the source. This is a mathematical derivation in prose, not a kernel-checked theorem, not an imported literature result, and not an OpenProblemResolutionClaim. Formal implementation remains stopped under the explicit Library-only rule.

For decreasing positive q, the two-step identity is s_j - s_(j-2) = q_j - q_(j-1) for j >= 3. Both parity subsequences of s are weakly decreasing. Odd-position s-values are positive, and even-position s-values are nonpositive, by the two-step sign argument in the brief. Thus the two subsequences cannot collide with each other. All s-values are distinct exactly when every within-parity step is strict, which is exactly q_2 > q_3 > … > q_k. In list notation the condition is strictness of the tail, while q_1 >= q_2 is allowed to be equality.

The map to strict partitions of n+1 is consequently [q_1,q_2,...,q_k] -> [q_1+1,q_2,...,q_k] for nonempty q and [] -> [1]. The first inequality becomes strict and the tail is already strict; the weight increases by one. Conversely, a strict positive partition p of n+1 is nonempty. Send [1] to [], and otherwise decrease its largest part by one. If p has at least two parts, p_1 > p_2 >= 1 ensures the decreased largest part stays positive and is at least p_2. If p has one part other than 1, its decrease is positive. The tail remains strict. These operations are inverse, including the n=0 singleton case.

This avoids the apparent Frobenius-weight obstruction: reconstruct q from the alternating sums, then increase only its largest part. From (A,B), the reconstruction interleaves q_(2i-1)=A_i-B_(i-1), q_(2i)=A_i-B_i with B_0=0. The route still requires a Lean proof of the strict-tail characterization, the partition-level forward/inverse maps, positivity, weight and inverse laws, and the resulting finite-cardinality equality. None is claimed as kernel-verified here.

The worker ran the independent recursive partition enumerator enumerate.mjs from the attempt directory; exit 0. It covered all 28,629 partitions of n=0,…,30. For every partition it checked the sign and monotonicity claims and equivalence of the alternating-sum Nodup condition with strictness of the tail. For each weight it compared the full image of the bump map with the complete independently filtered set of strict partitions of n+1, checked both inverse laws, and compared the counts with opened A000009 DATA. All checks passed. Counts for n=0,…,14 were 1,1,2,2,3,4,5,6,8,10,12,15,18,22,27. These finite checks are diagnostic only and do not prove the unbounded claim.

The same structured diagnostic verifies that the 42 requested response identifiers agree with the source-extracted set and records each response’s SHA-256 in enumeration.json. The complete JSON responses and scratch Lean files are worker-owned runner artifacts, not repository modules.

Delivery validation checkpoint

make lean LAKE_JOBS=3 exited 0, reporting 12,761 jobs. Its ensure receipt again reported both layers warm and zero missing Mathlib oleans. Existing module axiom and style messages were replayed; no D5 source changed in this attempt. make lean-report LAKE_JOBS=3 then exited 0, producing report SHA-256 5abd187439ffa3496e91fe1d627fc7e70e3a7000b786dd1c3c0adc986cd28828. make emit then exited 0 and reported emitted: 0 changed blueprint(s). No ledger-align is needed because there is no new declaration or OpenProblemResolutionClaim. The repository delivery is exactly this Library note; the Problems eight- section module template is inapplicable to the explicit Library-only branch.

Pre-PR comparison used fetched dev efbcafc96707c57fe6a4f5380878e1286f2daf14: git merge-tree –write-tree origin/dev HEAD exited 0, with no conflicts. The repeated D5 search git grep -n -i -P 'A392698|distinct.*alternating|alternating.*distinct' origin/dev -- 'D5/**/*.lean' returned one unrelated graph-coloring comment, no target declaration. The implementation baseline remains the fixed c3c261a08c commit; no source was taken from the moving dev tree for the mathematical argument. git diff –check passed. The repository diff contains one added Library note and no changed or deleted pre-existing file.

The PR is opened through make pr-open with AUTO_MERGE=1. Its terminal required-check results and merge identity are recorded in the runner result, not predicted here. Runner artifacts are under a392698-impl-0909/attempt-1: the 43 source JSON snapshots, BindOnly.lean, Boundaries.lean, bindonly.log, boundaries.log, enumerate.mjs, enumeration.json, lean.log, lean-report.log, emit.log and result.json.

Corrected implementation brief, 2026-09-09

This section is new in the a392698-proof-0909 attempt, at fixed baseline b679dd557c19ecad635daaa617b588d0ef4321d9. The caller supersedes the earlier Library-only stopping rule: a conjectural equivalent statement is not a published proof. The existing 42-entry audit is retained without repetition. The previous worker supplied the mathematical strict-tail/bump route; the caller independently checked it finitely. Neither supplied a kernel proof. This worker uses the lean4 skill, implements directly, and claims no independent review or multi-model consensus at this checkpoint.

The preregistered escape witness is the equivalence between Nodup of the integer trimmed alternating sums and strict decrease of the tail. Its consumer is the unbounded equality with Nat.Partition.distincts (n+1). The first action, make lean-cache-ensure, exited 0 with this receipt:

{"status":"present","worktree":"/Users/chronoai/trureturing-a394454-centralbinom","donor":null,"method":"none","reason":null,"stamp_miss":null,"pin_sha256":"sha256:6c4c682ffba051b5744fe7a75ccc99d7f3b20227b3b026f392f3315be0adaa4e","clonefile_errno":null,"clonefile_errnos":[],"clonefile_attempts":0,"clonefile_cleanup_error":null,"mathlib_missing_olean_files":0,"mathlib_missing_olean_samples":[],"archive_status":"not_attempted","archive_mode":null,"archive_skip_reason":"project olean state is warm","archive_reason":null,"archive_producer_commit_sha":null,"archive_workflow_run_id":null,"mathlib_olean_state":"warm","mathlib_olean_probe_error":null,"project_olean_state":"warm","project_olean_probe_error":null}

The baseline is clean and exact. Both neighboring Compositions modules were read completely. Repeating the baseline repository keyword query from the previous search receipt gave 7 lines; its same-regex word-boundary positive control gave 17 lines. No target theorem is among the inspected statements. No atom identifier is supplied: the source obligation is this note and the explicit corrected OEIS brief. No show-atom or coverage claim is made. At this checkpoint no new Lean theorem, exhaustive search, priority, or larger-conjecture implication is claimed. Bind-only screening is next.

The new bind-only probe imports only pinned Mathlib and states the exact strict-tail equivalence for a positive decreasing natural list, with an integer accumulator. exact?, simp_all, omega and aesop did not close it; the log contains both unsolved directions after successful elaboration. This failed attempt is not an impossibility or exhaustive-search claim. The task-specific public GitHub code query "A392698" language:Lean (limit 20) returned no paths. The earlier broader ecosystem audit remains in force. No third-party result was imported or published proof located.

The new structural theorem trimmedSums_nodup_iff_strict_tail has now passed lake env lean D5/S1/Words/Compositions/TrimmedAlternatingPartitions.lean in the ensured warm tree, exit 0. Its axiom output is exactly propext, Classical.choice and Quot.sound. The forward proof uses an integer range invariant on strict lists; the reverse proof excludes equal adjacent tail parts using equal alternating sums two positions apart. No positivity or strictness of the first gap was silently added. This is a checked fragment; the full partition bijection and count remain to be implemented.

The full count theorem card_trimmedSums_eq_distincts now passes the warm-tree file check, exit 0, with only propext, Classical.choice and Quot.sound. Its proof constructs inverse maps on the two partition subtypes and applies Fintype.card_congr. The forward map changes [] to [1] and a::q to (a+1)::q; the reverse handles [1] separately and otherwise subtracts one from the maximum. Positivity, order, sums and both inverse laws are proved. The first compile exposed two implementation errors (a missing natural nonzero simplification and an unapplied Multiset.mem_sort relation argument); both were corrected before this successful check. No failed elaboration’s sorryAx output is counted as a proved theorem.

Per public theorem: trimmedSums_nodup_iff_strict_tail is content, with the private strict_bounds induction as its new intermediate fact; card_trimmedSums_eq_distincts is content, with the preregistered trimmedSums_nodup_iff_strict_tail as escape witness and the explicit inverse partition maps as additional construction. Both have direct frozen prerequisites [] and admission_basis escape-witness. Pinned Mathlib supplies list, sorting and finite-cardinality infrastructure, not this structural characterization or shifted bijection. The module has utility none: its public declarations define the recurrence and prove general symbolic statements; no bounded enumeration, checker or numerical certificate is being deposited.

Clause 3.2 for the count witness: (i) raisePartition and lowerPartition use the structural theorem to discharge the defining subtype predicates, and partitionEquiv is used by the cardinality proof; (ii) the structural proof contains the new two-step integer range induction and adjacent-collision argument, not a frozen projection or a Mathlib instance; (iii) a list Nodup characterization is not definitionally equal to the partition-cardinality equality; (iv) those predicate proofs are required by the two maps and remain on the live construction path. The structural theorem’s own strict_bounds witness likewise supplies the inequalities used by start_not_mem and nodup_from_strict_tail; its bound is not a restatement of Nodup. These are proof-shape judgments from the checked construction, not a claim that an automation failure proves absence of all alternative derivations.

Current implementation validation: make lean LAKE_JOBS=3 exited 0 with 12,763 jobs; make lean-report LAKE_JOBS=3 exited 0 and produced SHA-256 749b2266cdbaf9ab90343d9114c7cb6e96cce66a0f6f4586ca3da80b4de22752. Boundaries.lean imports the built module and exits 0, evaluating the five lists to [2,0,1], [3,-1,3,-2], [], [2], [1,0]. Kernel examples check both sides of the strict-tail criterion on the two supplied witnesses, distinguish whole-list strictness from tail strictness, and distinguish trimmed from untrimmed [1,1]. Separate kernel checks prove the left count at n=0 is 1 and the right count distincts(1) is 1. These worker readings are recorded in the Problems dossier’s Evidence section, without new dossier sections.

The compiler-API dependency probe now exits 0 and confirms that both trimmedSums_nodup_iff_strict_tail and strict_bounds belong to the elaborated count theorem’s transitive constant closure. It traverses declaration types and bodies through Lean.Environment, including theorem bodies with ConstantInfo.value? (allowOpaque := true). The first diagnostic omitted allowOpaque and therefore skipped theorem proofs; its false absence report was a probe defect, not a mathematical failure. This check establishes closure membership; the live-path and non-binding judgments above remain separate proof analysis.

ledger-align –add completed before emit, with selectors_considered=3881, changed=0, added=1, unchanged=3880 and conflicts=0. The new module state is sha256:dce800870bc3cce843668f62657af3511a25802775a5497220af70e2832978e2; the accepted event is sha256:fdbdc143bf1ed5ecdb759885d70b988b55fa646be58b7496951c03fdf4902a36. Its prerequisite_frozen_node_ids is []. The two authored public theorem statement identities are respectively sha256:375cdefdd995e98d90b9a2fb86f70188f486bf3be83fd03d8dc2282d7e676885 (structural) and sha256:511b3932db6e38b51c8853e9d40cf93d18a8edecb8319711f1c6992220535da2 (count). Compiler-generated recurrence equations are definitional companions, not separately claimed escape results.

make emit exited 0 and emitted exactly one changed Blueprint. Its initial failure was a Scribe FormulaIdentifier rejecting the dotted display name Nat.Partition.distincts; the display uses distincts with its full Mathlib name explicitly explained. The emitted formula, typed declaration handle and OpenProblemResolutionClaim all refer to the corrected shifted count. No harness, domain registry, frozen pre-existing Lean source or atom changed. This is a seven-file theorem delivery in the #6585 pattern, with the existing Library note extended rather than duplicated. There is no atom coverage transition because no atom was supplied.

Current unclaimed boundaries: no new source-xref audit, exhaustive literature search, proof of publication priority, equivalence to the unshifted source sentence, independent review, multi-model consensus or larger-conjecture implication is claimed. The hand mathematics is attributed to the previous worker and the caller’s independent finite confirmation; the new kernel proof is this worker’s contribution. PR status and final merge identity are recorded by the runner result, not anticipated here.