bibkey: oeis2026a392694
authors: OEIS Foundation Inc.
year: 2026
title: OEIS A392694
doi: null
url: https://oeis.org/A392694
claim: Reversed partitions with weakly increasing zero-based partial alternating sums are conjectured to be counted by A000009.
strata_touched:
  - D5/S1/Words/Compositions/ZeroPrependedFirstSumsOddParts
license: citation-only
triage: anchor

OEIS A392694

Provenance and preregistration

Skill context: lean4; this Codex implementation worker works on the caller’s fixed baseline b679dd557c19ecad635daaa617b588d0ef4321d9, branch lane/math/a392694-oddparts. No independent review seat has run here. The caller supplied the mathematical reparametrization and numerical checks through n=15; those are caller evidence, not a kernel proof. The caller did not conduct a literature search. No atom identifier was supplied, so the explicit OEIS brief is the source obligation and show-atom is inapplicable.

The preregistered escape witness is a weight-preserving bijection between qualifying reversed partitions and odd-part partitions: successive increments of the increasing positive first-sum preimage become multiplicities of descending odd parts. The first increment must be positive. Only after testing bind-only closure and checking source cross-references may an implementation of this new bridge proceed.

Source

The complete JSON entry was opened on 2026-09-09, revision 7, author date January 25, 2026. Its conjecture reads:

Conjecture: Reversed integer partitions of this type (with weakly increasing 0-based partial alternating sums) are counted by A000009.

The entry defines a reversed partition as a finite weakly increasing sequence of positive integers, and first sums as adjacent sums. This is a first-tier 2026 OEIS comment conjecture, subject to the proof search below.

Initial checks

The initial make lean-cache-ensure exited 0 before any Lake invocation:

{"status":"present","worktree":"/Users/chronoai/trureturing-a388711-choosable","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 completely, agents/CONTEXT.md, both supplied agent brief notes, and both existing Compositions modules. The general adjacent-sums definition FirstSumsPartitionCharacterization.firstSums already exists; any implementation will import it. Its frozen module state is sha256:84e432b8912426418215248825fc502114361397419f3c4016f7a62859a1e5ed. Its characterization assumes decreasing parts and preimage entries at least two, so that theorem does not state the present target.

Pinned Mathlib is db584cd6d46c92f209a44c0f1c829460d327499d (v4.33.0). Opened Partition/Basic.lean and Partition/Glaisher.lean. The endpoint signature is Nat.Partition.card_odds_eq_card_distincts (n : ℕ) : #(odds n) = #(distincts n). Here odds n = restricted n (¬ Even ·) and distincts filters parts.Nodup. The count uses a multiset of positive parts summing to n.

Unclaimed

The unbounded theorem is now kernel-proved for the explicit source predicate. No mathematical novelty, exhaustive literature search, first-publication priority, or implication to a larger conjecture is asserted. Pages not individually opened are ASSUMED-UNVERIFIED. The caller’s derivation and checks were not a kernel proof; the caller did not conduct the literature search. The independent A392698 lane is outside this worker’s scope.

Verified locator

• URL: https://oeis.org/A392694
• Opened machine-readable entry: https://oeis.org/search?q=id:A392694&fmt=json
• Scope checked on 2026-09-09: complete entry, including all comment, formula (absent), and xref fields; all 32 referenced entries were fetched in full.

Bind-only and cross-reference audit

The scratch probe a392694-bind-only.lean exited 1. Direct application of Euler gives a type mismatch; rewriting with Euler and unfolding both predicates leaves an equality of two different filtered cardinalities. This is not a proof that every bind-only approach fails. It identifies the remaining bridge rather than treating the Euler endpoint as the target. The inspected endpoint prints exactly the standard three axioms.

Textual D5 discovery used rg -n -i '\b(partial.alternating|zero.prepended|reversed.partition|firstSums|A392694)\b' D5 --glob '*.lean': 10 hits, confined to the existing first-sums module and one unrelated alternating-binomial comment. The same-boundary positive control rg -n '\b(firstSums|IsFirstSums)\b' D5/S1/Words/Compositions gives 17 hits. These are candidate-discovery readings, not a semantic absence proof.

The full Mathlib keyword search found alternating binomial sums, topology, inclusion-exclusion and Leibniz’s series, but no matching first-sums theorem. A separate YoungDiagram inspection found the existing conjugation mechanism transpose and equivListRowLens; it must be reused if that representation is chosen. Public GitHub Lean searches (limit 30) for "partial alternating", "firstSums", and "zero-prepended" each returned zero paths. The broader "odd" "partition" "bijection" query returned 24 candidates, including known Euler/Glaisher implementations, not an exact first-sums match. No dependency was added. Google and DuckDuckGo searches returned browser/challenge pages, not usable search results; no search-complete claim is made for those engines.

The exact A-number set was extracted from all comment/formula/xref fields of A392694: 32 distinct identifiers. Python urllib initially received 403 for all 32. The standard curl client then successfully retrieved all 32 complete JSON entries using the requested id search URLs; no fields were truncated. Original bytes, SHA-256 hashes and revisions are retained in the attempt directory (xref-curl-receipts.json). Read the complete relevant name/comment/reference/link/formula/xref fields, with the following findings. Only a proof of the actual target triggers the literature downgrade; conjectural restatements do not.

A392707 says: “For weakly instead of strictly increasing we have A392694, apparent count A000009.” This is a conjectural restatement, not a published proof. A000009 contains genuine classical proofs for odd/distinct partitions and a symmetric-unimodal interpretation; neither supplies the source’s first-sums correspondence as an already proved statement. The linked Arndt book was also checked as recorded below. All linked pages not individually opened remain ASSUMED-UNVERIFIED.

Implementation route after search

Opened the linked Arndt site and its full fxtbook PDF (978 pages), extracted its text, and inspected the A000009 passage at printed pages 348-350. Equations 16.4-22 through 16.4-25 concern classical odd/distinct partitions; they do not identify zero-prepended first sums. The target is therefore not downgraded on this evidence. No first-publication priority is claimed.

Before implementation, the concrete representation of the preregistered bridge is fixed as Ferrers conjugation: reverse s into decreasing row lengths, transpose its Young diagram, and replace each column height h by 2*h-1. A column of height k-i+1 occurs exactly t_i times, so this is the caller’s same odd-multiplicity map. Existing YoungDiagram.transpose and YoungDiagram.equivListRowLens will supply conjugation; the new live obligation is weight preservation for the first-sums map and the inverse correspondence. Positivity in the row-length subtype forces the leading increment and excludes padding with fictitious zero rows. The empty diagram handles n=0.

The first implementation fragment now compiles (fragment-1c.log, exit 0): fixed-start first sums are injective; increasing positive preimages give increasing positive images; the exact sum identity retains the last entry; Young-diagram transposition preserves the sum of row lengths. Initial compiler diagnostics exposed argument-order and lemma-name errors plus an unreduced arithmetic lambda, all repaired. No target count is claimed yet.

The second fragment compiles without diagnostics (fragment-2c.log, exit 0). It constructs the full equivalence between qualifying lists and decreasing positive odd lists, and proves preservation of total weight. Conjugation is Mathlib’s existing equivalence; the new row_weight proof combines the exact first-sums identity with the odd-column identity. The inverses use positivity and oddness explicitly. List-map rewriting and equivalence unfolding errors in fragment-2/2b were repaired; no target cardinality theorem is claimed at this checkpoint.

The complete unbounded count now compiles without diagnostics (fragment-3b.log, exit 0). card_zeroPrependedFirstSums_eq_odds restricts the weight-preserving equivalence to total n and transports sorted lists to Nat.Partition n. card_zeroPrependedFirstSums_eq_distincts composes that result with the pinned Euler theorem. No extra hypotheses, finite cutoff, sorry, or private axiom were introduced. The full repository gates remain pending.

The worker independently enumerated all increasing positive partitions for n=0,…,15 using Python integer subtraction for the alternating recurrence. The 137 qualifying instances have zero weight violations and no duplicate odd images; at each n, their actual image set equals the full odd-part set. Qualifying, odd, and distinct counts are all 1,1,1,2,2,3,4,5,6,8,10,12,15,18,22,27. This agrees with the caller’s readings. The scripts and complete rows are in numerical-check.py and numerical-check.json in the attempt directory. For y=[2,4,4], s=[2,2,2], t=[2,0,0], and the image is [5,5], all of weight 10; Euler’s binary-multiplicity map sends this to the distinct partition [10]. For y=[2,3], the unique recurrence gives s=[2,1], failing at 2 <= 1. At n=0 the empty partition is present and each of the three counts is 1. These finite checks are evidence only, not the unbounded proof or new frozen finite-instance declarations.

Declaration shape and admission

added_hypotheses: []; utility: none (unbounded symbolic mathematics). The first-sums bridge was not available at the fixed baseline; the initial Euler-only attempt did not close it. Source and target use the same n.

The companion fulfills the source’s explicit A000009 obligation. Its directed consumer-to-prerequisite edge is card_zeroPrependedFirstSums_eq_distincts -> card_zeroPrependedFirstSums_eq_odds. The endpoint’s two-line composition does not make the baseline source target bind-only: the new bridge is essential and was not a frozen premise there.

The escape witness satisfies the four requirements:

1. Dependency closure: Fintype.card_congr consumes the partition equivalence; its restriction to sum n uses firstOddEquiv_sum, which uses row_weight. The bijection and the weight theorem are elaborated constants in that path.
2. Not a frozen projection: the imported frozen module only supplies the adjacent-sums definition. Its decreasing-list characterization cannot yield the increasing-list weight bijection. The new induction for firstSums_sum, inverse construction, and column weight calculation supply facts absent from the Euler cardinality identity and frozen premises.
3. Not definitionally the conclusion: the witness concerns an equivalence of list subtypes and preservation of their sums. The public conclusion is an equality of two finite partition cardinalities.
4. Live use: removing weight preservation prevents restricting the bijection to partitions of n. Removing invertibility prevents cardinal transport. Neither is a discarded conjunct or an unused import. The Euler theorem alone identifies odd and distinct counts, not the source filter.

Direct external frozen dependency for both public results (the endpoint via the bridge): GID D5/S1/Words/Compositions/FirstSumsPartitionCharacterization, module statement_id sha256:84e432b8912426418215248825fc502114361397419f3c4016f7a62859a1e5ed. The actual reused definition is .firstSums, declaration statement_id sha256:e5254a293a82bdc518976d3ebd84a9cdaaa0b56b0ffb7cdb261299e242ac7ca2. Scope: adjacent sums only; no use of its decreasing-part characterization. The pinned Mathlib Euler and YoungDiagram declarations are upstream prerequisites, not repository frozen-node identities.

Repository validation

make lean LAKE_JOBS=3 exited 0, reporting 12763 build jobs completed. The project-wide log includes pre-existing warnings in other modules; the new module’s fragment-3b.log has no diagnostics. Problems has exactly the required eight sections and its Evidence includes both caller and worker readings. Scribe supplies authored formulas for the definition and both theorems. The subsequent report, ledger, emission, and publication receipts follow.

The final axiom audit exited 0. Both public theorems print exactly [propext, Classical.choice, Quot.sound] (final-axioms.log); no sorryAx or custom axiom occurs. The audit imports the built module, rather than copying its statements into a separate model.

make lean-report LAKE_JOBS=3 exited 0. Canonical raw report SHA-256: 9f7eb9cdb4b6f2fa41a41865c35fa6cf06b864bd9c76e04b08d89ab5aa9feebd. ledger-align --add D5/S1/Words/Compositions/ZeroPrependedFirstSumsOddParts.lean --candidate-lean-report .lake/build/stratalint/raw-lean-report.json exited 0: selectors_considered=3881, changed=0, added=1, unchanged=3880, conflicts=0. It generated the v5 accepted event sha256:00fef2b1990b41228bd8a7ad1acea02e890cc4ae2c93f5d33a94e89f91dc787e and module state sha256:ed9931fda009a0f0f65219c7b66312b2a95a05a0154e65fe4e899c8d80e6792f. The event’s sole external prerequisite is the frozen first-sums module.

The first make emit exited 2 because the Library note incorrectly used the Problems-only triage value theorem. The canonical Library value is anchor, as in the frozen family template. This metadata error also caused the reference-resolution diagnostics; the Library value was corrected before rerunning emission. No Lean or frozen bytes were altered by this correction.

Fetched and read dev at 9b24956f07bc93856f0ec14fee132151461d93ce before publication. A scoped keyword check across Compositions, Library/Words, and Problems found only the known first-sums definition and documentary mentions, no duplicate A392694 implementation. git merge-tree --write-tree HEAD origin/dev exited 0 with no conflict. This checks the sampled dev tree, without rebasing the implementation away from its fixed source baseline.

The corrected make emit exited 0 (make-emit-2.log). Read back the emitted Markdown: all three authored formulas match the Lean definition and two counts, and the endpoint carries the proved problem-resolution marker. The seven-file delivery matches PR #6585, whose merged body and file list were also opened. No new domain or aggregate hand-maintained registry exists.

The additional imported-module #print audit (elaborated-proofs.log) exited 1: the two public declarations printed, but textual names of private declarations contain a numeric name component that the command parser rejected. The preceding checkpoint incorrectly recorded this audit as exit 0; that reporting error is corrected here. The public count body already shows the live use of firstOddEquiv_sum, and the endpoint shows the new count bridge and Euler identity. A direct environment lookup is used below to inspect the private declarations without the textual-name parser.

The first raw environment lookup used ConstantInfo.value! with its default allowOpaque=false, which emits PANIC for theorem bodies even though this scratch process returned exit 0. That output is rejected as validation (elaborated-environment.log). The corrected audit uses the checked value? true interface and Expr.getUsedConstants; it exited 0 without errors or panics (elaborated-dependencies.log). It confirms the actual constant edges count -> firstOddEquiv_sum -> row_weight -> firstSums_sum, and endpoint -> new bridge plus the pinned Euler declaration. These were audit-script errors only; the production proof and all repository gates remained unchanged.