bibkey: oeis2026a392707
authors: OEIS Foundation Inc.
year: 2026
title: OEIS A392707
doi: null
url: https://oeis.org/A392707
claim: Strictly increasing zero-based partial alternating sums are conjectured to be counted by A053251.
strata_touched:
  - D5/S1/Words/Compositions/StrictFirstSumsGapfreeOddParts
license: citation-only
triage: anchor

OEIS A392707

Verified locator

https://oeis.org/A392707, full JSON entry revision 10, retrieved on 2026-09-09. The comment field contains the quoted conjecture about strictly increasing zero-based partial alternating sums and A053251. The source record is A392707.json in the attempt, with its byte hash and retrieval URL in oeis-manifest.json. The related endpoint https://oeis.org/A053251 was also opened in full, revision 76: its first comment gives the gapfree odd interpretation and its first formula gives the psi expansion. These locators attest to the stated source text, not to a published proof of the new combinatorial bridge.

Provenance and preregistration

Skill context: lean4, in the caller’s consensus-rnd:sshx implementation stage. One Codex worker performs source investigation, implementation and self-checks; no independent review or multi-model consensus is claimed here. The source baseline is 6570b0d7f865b56f0fdc678f961396cff6e25f81, branch lane/math/a392707-gapfree-odd. No atom identifier was supplied: the explicit OEIS brief supplies the obligation, so show-atom is inapplicable.

The initial preregistration required checking this first-tier 2026 conjecture for published proofs before implementation. Conjectural restatements do not count as proofs. The preregistered candidate escape witness is the restriction of the odd-part correspondence to strictly increasing preimages: every increment is positive exactly when every odd part from 1 to the largest part occurs. The proposed live construction must preserve weight, be invertible, and handle the empty partition. The target is equality of the two partition counts for every n. First test closure by pinned Mathlib and frozen interfaces alone; if it is bind-only, stop without a new module.

Initial receipts

Read CLAUDE.md in full, agents/CONTEXT.md, both agent brief notes and all four existing Compositions modules. The required sibling import is D5.S1.Words.Compositions.ZeroPrependedFirstSumsOddParts; its frozen module statement_id is sha256:ed9931fda009a0f0f65219c7b66312b2a95a05a0154e65fe4e899c8d80e6792f. It is precisely PR #6600, merged at the pinned baseline. Its source declares the equivalences, weight lemmas and first-sums auxiliary lemmas private. Its public cardinality theorems concern all weakly increasing preimages; they do not expose a restriction predicate on the bijection. Semantic interface probes and the bind-only assessment will be recorded below. The existing adjacent-sums definition will be imported, never redefined; the weak predicate will likewise remain at its unique existing address.

make lean-cache-ensure exited 0 before any Lake invocation. Receipt: status=present, method=none, stamp_miss=null, both project and mathlib olean states warm, missing mathlib oleans 0, clonefile attempts 0. Full receipt: a392707-impl-0909/attempt-1/lean-cache-ensure.log.

Unclaimed and remaining scope

The unbounded combinatorial count theorem has now been kernel-checked. The caller’s reparametrization and checks n=1,…,15 were supplied mathematical/computational evidence, not a kernel proof. The caller’s psi series interpretation was initially ASSUMED-UNVERIFIED; its occurrence on A053251 is now source-verified, as recorded below. The combinatorial theorem does not formalize equality with the coefficients of the mock theta function. No full formal OEIS conjecture resolution, exhaustive literature search, novelty, first-publication priority, or larger-conjecture implication is claimed. Unopened linked pages remain ASSUMED-UNVERIFIED.

Source and xref receipts

Fetched both roots and every A-number in their comment/formula/xref fields as full JSON entries on 2026-09-09: 53 distinct referenced IDs, 54 entries including A392707, all HTTP 200. Full bytes, SHA-256, revision, URL and status are saved in a392707-impl-0909/attempt-1/oeis-manifest.json and the individual Axxxxxx.json files. The first unencoded requests returned HTTP 403; the successful equivalent query uses search?fmt=json&q=id%3AAxxxxxx.

A392707 revision 10 explicitly states:

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

A053251 revision 76, first comment:

Number of partitions of n into odd parts such that if a number occurs as a part then so do all smaller positive odd numbers.

Its first formula is exactly:

G.f.: psi(q) = Sum_{n>=1} q^(n^2) / ( (1-q)(1-q^3)…(1-q^(2n-1)) ).

Thus the caller’s proposed psi expansion and combinatorial interpretation are now source-verified, not new observations. This source verification is not a Lean proof of the series identity. The constant term needs separate accounting: A053251(0)=0, whereas the present combinatorial classes include the empty partition and have count 1 at zero. The psi correspondence is restricted to positive n, or uses the series 1+psi(q).

A392694 and A392703 repeat the strict-count claim conjecturally (“apparently” and “we appear to have”). A122129/A122130/A122134/A122135 cite published Gordon/Connor proofs of alternately strict partition interpretations; those statements do not mention the zero-based first-sums restriction. A000009 explains conjugation between ordinary gapless and distinct partitions, a classical ingredient distinct from the weight-preserving first-sums bridge. No proof of the target bridge was located in the examined entry fields; this is not a claim of exhaustive literature search.

GitHub code search for "A392707" language:Lean and "gapfree" language:Lean returned 0 paths. "mock theta" language:Lean returned one file, opened at tomdif/RamanujanLean/RamanujanTau/MockTheta5.lean: bounded fifth-order q-series computations, not the third-order psi or the target correspondence.

Interface probe

The warm-tree compiler accepted the existing public firstSums, firstSums_length, IsZeroPrependedFirstSums and the weak cardinal theorem. It rejected the ordinary qualified names firstOddEquiv, firstOddEquiv_sum and firstSums_injective as unknown identifiers: they are private to the sibling. Full diagnostics are in interface-probe.log. No frozen module has been modified and no duplicate firstSums or weak predicate has been introduced.

Complete retrieval inventory (entry revision and full-response bytes):

The standard module / import all route also failed: Lean rejects importing this legacy non-module sibling from a module-system file. A successful compiler probe (private-reuse-probe.lean, exit 0) instead uses a local term elaborator to resolve the uniquely named frozen constant in the imported environment. It returns that existing Expr.const; it does not copy a definition, add an axiom, or assert a theorem. This permits genuine reuse of the sibling’s Rows, conjugate, oddify, fixed-start injectivity, firstOddEquiv, weight proof and partition/list equivalences. The code must report this private-interface coupling explicitly; a public upstream API would remove the need for the local lookup. The predecessor is frozen at the pinned source, and is not edited. The sibling’s public cardinal theorem prints exactly propext, Classical.choice and Quot.sound.

Implementation checks

The bind-only attempt (bind-only-probe.lean) exited 1: even after unfolding, the weak theorem counts nonnegative increments and all odd partitions, whereas the target counts positive increments and exact initial odd support. The remaining property on the frozen bijection is not supplied by either public weak-count theorem. The exploratory simp call on elaborated private function terms was also rejected as a non-proposition; that diagnostic is not evidence of mathematical impossibility.

Fragment 1 is kernel-checked (warm lake env lean, exit 0): height_mem_iff says that column height h occurs exactly when the row length drops strictly between h-1 and h; strict_rows_iff_heights characterizes strict rows by the complete positive interval of column heights. The initial compiler error was an incorrectly used rwa inside a side condition, fixed without changing any statement. These are the new facts used to restrict the frozen equivalence, not a reproof of its weight or invertibility.

Independent Python enumeration (numerical-check.json) used integer subtraction and tested n=0,…,15. Counts are 1,1,1,1,2,2,2,3,3,4,5,5,6,7,8,9. All 60 qualifying instances have equal source/image weights, no duplicate images, and exact image-set agreement with gapfree odd partitions. A053251 agrees at n>=1 and differs at zero. Positive witness: y=[1,3,6], s=[1,2,4], odd image=[1,1,3,5], sum 10. The gapped odd partition [1,5] has weak preimage s=[1,1,2], giving y=[1,2,3] and sum 6; it misses 3 and fails strictness at the repeated 1.

Fragment 2 is kernel-checked (exit 0, no diagnostics): the exact support predicate GapfreeOdd m := exists k, forall x, x in m iff exists i<k, x=2*i+1 is transported through the existing oddify and conjugate functions. The forward/backward support proofs include both endpoints, and the empty case is covered without a positive-length assumption. The resulting firstOddEquiv_gapfree restricts the original frozen firstOddEquiv; its proof reuses the original rowFirstEquiv and firstSums_injective constants. No bijection or adjacent-sums definition has been copied.

Fragment 3 closes the main unbounded theorem card_strictFirstSums_eq_gapfreeOdd for every natural n (exit 0, no diagnostics). strictPartitionEquiv restricts the existing firstOddEquiv with its existing sum theorem, then uses the existing firstListEquiv and oddListEquiv. Subtype flattening uses Mathlib’s Equiv.subtypeSubtypeEquivSubtype. Added hypotheses: none. The mock theta coefficient identity is not a theorem of this module.

Proof shape and dependency identities

The sole public theorem card_strictFirstSums_eq_gapfreeOdd has proof_shape: content, admission_basis: escape-witness, and added_hypotheses: []. Its statement identity in the canonical Lean report is sha256:440cc80253340ed1191005aa0d47e59c32666842ae8542743ca71999467e6ef1. The escape witness is height_mem_iff, realized by the explicit column d.rowLen h at a strict row drop. This is the diagram form of the preregistered positive-increment/full-support restriction.

The four semantic criteria are assessed as follows:

1. Dependency closure: the witness is used by strict_rows_iff_heights, then strict_rows_iff_interval, row_gapfree, firstOddEquiv_gapfree, strictPartitionEquiv, and the public cardinal theorem.
2. Non-projection: the weak correspondence provides weight and invertibility, but no theorem identifying the image of strict preimages. The proof constructs a column of each required height from a strict drop, and derives the reverse strict drop from a column witness. This construction is absent from the examined frozen interfaces; the failed bind-only probe is evidence about that attempted route, not an exhaustive impossibility proof.
3. Non-definition-equivalence: the witness relates row lengths and column membership in an arbitrary Young diagram; it is neither an alias nor a restatement of equality of two filtered partition cardinalities.
4. Live path: the property equivalence is the argument to Equiv.subtypeEquiv restricting the original bijection. No unused conjunction or discarded proof component inserts the witness. Without this property proof the restriction cannot be formed by the attempted frozen bindings alone.

These are semantic self-assessments for review, not machine certification of proof shape. Computational content is none: the repository declarations are general predicates, unbounded diagram lemmas, and a weight-indexed equivalence/count theorem. The local elaborator only resolves imported constants; it is not a numerical checker or a certified finite instance. Concrete computations are scratch evidence outside the repository module. All other computational-utility fields are not-applicable(kind=none).

The direct imported frozen GID is D5/S1/Words/Compositions/ZeroPrependedFirstSumsOddParts, with module statement_id sha256:ed9931fda009a0f0f65219c7b66312b2a95a05a0154e65fe4e899c8d80e6792f. The following declaration identities are read from the canonical report for that frozen source (all helpers in the table are private):

The existing public weak predicate has statement_id sha256:4cfbc60d3cfa7d0c42d9339ea24d21050e04919a48605281ef22d35ac443ad41. The transitive imported GID D5/S1/Words/Compositions/FirstSumsPartitionCharacterization has module statement_id sha256:84e432b8912426418215248825fc502114361397419f3c4016f7a62859a1e5ed; its public firstSums declaration has statement_id sha256:e5254a293a82bdc518976d3ebd84a9cdaaa0b56b0ffb7cdb261299e242ac7ca2. Pinned Mathlib is db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0. Mathlib supplies Young-diagram membership and length lemmas, subtype equivalences and finite-cardinality transport. Keyword search for mock.?theta|gapfree|gapless|firstSums|partial alternating across that pinned Mathlib returned no matches (mathlib-search.log); the broader ecosystem search results are recorded above.

Full gate and witness receipts

make lean LAKE_JOBS=3 passed (exit 0, make-lean-2.log), with the new module built in 7.4 seconds on this warm tree. The first attempt failed because the Scribe formula lacked one closing parenthesis; it was corrected without changing Lean. Other build output contains cached warnings from unrelated modules, not diagnostics from the new Lean module.

make lean-report LAKE_JOBS=3 passed (exit 0, make-lean-report.log). Its canonical report hash is sha256:66d56178923d8332043c0f3bd0594b53ec39a8f5901e2d5fe4f2746eedbd9bf3. The report includes the new module with source hash sha256:c019ed20d3496475020dff8fbcf3fbda15c069bd05996b080cd01aa6436772ac. The main theorem has exactly propext, Classical.choice, Quot.sound; there is no sorry or added axiom.

The scratch file witnesses-and-axioms.lean also passed (exit 0). It checks the strict [1,2,4] preimage of [1,3,6], the gapfree [1,1,3,5] multiset, both weights 10, the gapped [1,5] exclusion, the non-strict [1,2,3] source, both empty predicates, and the symbolic length-one case for every a>0. An initial rfl for firstSums[0,a] needed unfolding by simp; the corrected run and standard-axiom output are in witnesses-and-axioms.log.

The repository’s deposit-evidence/proof-edges-template.lean, instantiated outside the repository as proof-edges.lean, passed on the warm tree. Its elaborated constant edges verify every edge of the dependency chain listed above, including public count -> strictPartitionEquiv -> firstOddEquiv_gapfree -> row_gapfree -> strict_rows_iff_interval -> strict_rows_iff_heights -> height_mem_iff. The proof-edges.log receipt confirms criterion (i); it does not mechanically decide the semantic non-projection or live-use criteria.

The canonical CLI ledger-align --add selected the new module and its frozen sibling, and passed: selectors_considered=2, changed=0, added=1, unchanged=1, conflicts=0 (ledger-align.log). The new module statement_id is sha256:b219f7062d1489c6f7713613d76bd968a07f470ba770dda55c0163642d8674a7; the accepted Freeze event is sha256:aadad4599084fc6773280b742bd22324db3eff1264e1cb2b2734bd755c077c2e. The canonical report and Freeze event also retain compiler-generated elaborator declarations; none introduces a mathematical axiom. No frozen predecessor was edited and Lean was not changed after freezing.

make emit passed (exit 0, make-emit.log), emitting exactly one changed Blueprint. Its formulas were read back: strictness is <, support is an exact iff, the count quantifies over all n, and both sides filter the same finite partition universe. The Problems dossier has exactly the required eight sections. No full-conjecture OpenProblemResolutionClaim is asserted.

A read-only fetch found dev at 1dfafe5e96353f0109d5e4b0d3c9db03782be6ab. Compared with the pinned start, that dev snapshot has no changes in the Compositions source/Blueprint directories. A targeted git grep -P for A392707/gapfree/gapless finds the already inspected documentary xrefs, and no additional target theorem. git merge-tree --write-tree --no-messages with that dev and implementation commit caabb06ea9 passed without conflict. The worktree retains the caller’s pinned source ancestry.

Remote content-check correction

PR #6605’s first run (34331753842) compiled the new Lean module in 15 seconds and produced its canonical report successfully. Its subsequent Scribe content check reported exactly one red finding: incomplete-library-locator on this note. The note already had the correct URL and full source evidence, but lacked the required Verified locator section binding that URL. That section is now present with the actually retrieved source revisions and field scope. No Lean, frozen identity, Scribe formula or source claim was changed. The failure receipt is ci-lean-verdict.log; the successful remote compilation and report receipt are in ci-lean-check-start.log.

The exact canonical scribe-content-checks.sh entry then passed locally against immutable dev 1dfafe5e96353f0109d5e4b0d3c9db03782be6ab (exit 0, scribe-content-checks.log), including KaTeX parsing of the three formulas in the one changed Blueprint: judged=1 formula(s)=3 red=0. The first remote run’s engineering job also finished successfully.