bibkey: oeis2026a388711
authors: OEIS Foundation Inc.
year: 2025
title: OEIS A388711
doi: null
url: https://oeis.org/A388711
claim: Gus Wiseman conjectures that partitions with choosable initial intervals are counted by superdiagonal reversed partitions with the same sum and number of parts.
strata_touched:
  - D5/S1/Words/Compositions/ChoosableInitialIntervals
license: citation-only
triage: anchor

OEIS A388711

The task is a first-tier recent OEIS comment conjecture, with source baseline d527e3081957dbd440ca634d821e98b868abf534. The supplied source reads:

Conjecture: Also the number of superdiagonal reversed partitions of n into k parts, where a sequence (y_1, …, y_k) is superdiagonal iff y_i >= i for all i = 1..k.

We say that a set or sequence of nonempty sets is choosable iff it is possible to choose a different element from each set. For example, ({1,2},{1},{1,3}) is choosable because we have the choice (2,1,3), but ({1},{1,2},{2}) is not.

The initial interval attached to a part x is {1,…,x}. Increasing order is the reversed-partition convention. Indices in Lean start at zero, so the superdiagonal bound must be i+1. Positive representatives are required even when the list contains zero.

Provenance and preregistration

Skill context: lean4; implementation by this Codex worker in the supplied worktree, with no independent review seat at this checkpoint. The caller’s enumeration and literature search are reported below as caller evidence. No atom identifier was supplied: the explicit OEIS implementation brief is the source obligation, so show-atom is not applicable to this task.

The caller preregistered the sorted-list SDR equivalence as the proposed escape witness for the counting identity. Its necessary direction restricts an injective representative map to the first i+1 positions and proves that its image lies in {1,…,y_i}; cardinal comparison forces i+1 <= y_i. Its sufficient direction constructs the representatives i+1. Bind-only inspection must finish before a Lean module is created.

Search log

• 2026-09-09, worker: git rev-parse HEAD returned the exact baseline above. Read CLAUDE.md, both agent brief notes, agents/CONTEXT.md, and the complete existing Compositions module FirstSumsPartitionCharacterization.
• Worker: rg -n -i 'superdiagon|initial interval|distinct representative|choosable|A388711' D5 -g '*.lean' returned 5 matching lines: Tribonacci Names, two Sumfree comments, a Jacobi matrix comment, and GoldenResource layers. None states the target SDR characterization. This is a bounded textual search, not a coverage proof.
• Positive control: rg -n '\bfirstSums\b' D5/S1/Words/Compositions -g '*.lean' returned 10 matching lines. Both commands use rg alternation/boundary support; no unsupported git grep -E word-boundary syntax was used.
• Environment discrepancy: .lake is absent in the supplied worktree at the first inspection, despite the brief’s prior ensure report. The worker will use make lean-cache-ensure before any Lean compilation.
• Caller report, 2026-09-09: four web keyword groups including “initial intervals SDR sorted a_i >= i” found no published statement of this partition-count identity. General Hall theory and SDRs are classical. The underlying initial-interval criterion may be a familiar folklore consequence of Hall; it must not be presented as a new mathematical theorem.
• Caller report: exhaustive backtracking for choosability and direct checks of superdiagonality agreed cell by cell for n=1,…,13, also agreeing with OEIS DATA after aligning its k=0 and n=0 entries.
• Worker directly fetched https://oeis.org/search?q=id:A388711&fmt=json: the name, choosability definition, initial-interval definition and conjecture match the brief. The response has revision 7, author date September 23, 2025 and creation time September 25, 2025. Thus the brief’s 2026 attribution differs from the opened source; the requested bibkey is retained, but the bibliographic year is corrected to 2025. The first-tier classification (2024-2026) is unaffected.
• Preliminary public Lean index check, using authenticated gh search code with language:Lean, limit 20: "superdiagonal" returned 2 matrix-related paths; "choosable" returned 5 distributed-protocol paths. These are candidate-discovery results, not semantic coverage conclusions. Ordered Mathlib inspection and the subsequent ecosystem check remain pending.

Limits

Ordered library inspection, worker, 2026-09-09: Mathlib HEAD is db584cd6d46c92f209a44c0f1c829460d327499d (v4.33.0), matching the manifest. The regex superdiagon|choosable|initial intervals|distinct representative|parking.function over Mathlib returned 3 Hall documentation lines. The Hall theorem inspected is Finset.all_card_le_biUnion_card_iff_exists_injective; it leaves the arbitrary-subfamily union cardinal inequalities. The general cardinal lemma is Fintype.card_le_of_injective; List.Pairwise.sortedLE supplies monotonicity of list lookup. No frozen D5 theorem is a direct dependency (GID/statement_id: none). The cache ensure returned exit 0, seeded by clonefile with both layers warm and no missing Mathlib oleans.

After this Mathlib inspection, public GitHub Lean searches (limit 20) for "initial intervals", "superdiagonal" "partition", and "parking" "function" returned respectively 5 Abel-summation paths, 0 paths, and 11 protocol or complexity paths. No matching target theorem was found in this searched scope. These path-level candidates were not imported; no third-party dependency is added. The direct Hall-instantiation and normalization probe is now staged outside the repository at /tmp/a388711-bind-only.lean.

The bind-only probe returned exit 1: direct Hall instantiation has right side forall s, s.card <= (s.biUnion intervals).card, not the desired index bound; definition-only simp leaves the full SDR/index equivalence unsolved. This failure alone is not an impossibility proof. Together with the inspected upstream statements, it identifies the missing live construction: restrict the representative map to a prefix, bound its image, and apply cardinality. The implementation proceeds with proof_shape: content and admission_basis: escape-witness, subject to kernel verification. The proposed witness remains exactly the prefix argument preregistered by the caller. The general Hall theorem is not needed in the final module.

First local implementation compile returned exit 1 with three elaboration errors: implicit Fin bounds in congrArg and two unreduced function applications in arithmetic goals. The next revision supplies the Fin type and explicit successor arithmetic. No failing proof is described as kernel verified.

The second compile returned exit 0. The sorted-list equivalence and the same-sort count equality both have only propext, Classical.choice and Quot.sound in their printed axiom closures. The next revision adds order invariance via Mathlib’s List.perm_comp_forall₂, transporting the nodup list of representatives, and uses it on the live count path: descending parts on the left, ascending reversed parts on the right. Named consumer direction: card_choosable_eq_superdiagonal -> choosableInitial_congr_perm.

The first permutation revision exposed one cast-normalization error in List.get_ofFn; adding the upstream Fin.cast_mk rewrite addresses that specific goal. The prefix theorem remained verified in this compile. The next validation is the full repository Lean entry point with LAKE_JOBS=3.

make lean LAKE_JOBS=3 returned exit 0 (12,749 jobs). All three public theorems printed only the standard three axioms. Two local style warnings (one long digest line and show changing a goal) are removed before the final report. The Problems entry keeps exactly its eight template sections; the Scribe source uses typed author formulas for all three theorem nodes.

The final-source make lean LAKE_JOBS=3 also returned exit 0, with no local style warnings. Initial boundary probing already computed SDR witness counts (1,0) for [3,2,1]/[4,1,1] and (1,0) for []/[0], but failed to synthesize a Decidable instance for the opaque Superdiagonal definition. The scratch probe now supplies that instance by unfolding the exact predicate; the production definitions and theorem statements are unchanged.

Per-declaration proof shape

All direct frozen dependencies below are none: no GID/statement_id from a baseline-frozen D5 module is imported or used. Pinned Mathlib dependencies are upstream declarations, not frozen D5 prerequisites. New declarations in this same module are inlined for classification.

For choosableInitial_iff_superdiagonal, all four clause 3.2 checks hold: (i) Lean #print shows prefix_capacity directly in the elaborated forward implication; (ii) it constructs the prefix restriction and its bounded image, facts absent from the frozen prerequisites and not a direct instance of the general cardinal theorem; (iii) the statement takes a particular injection, its bounds and one index, and is not definitionally equivalent to the entire existential equivalence; (iv) its cardinal bound is returned as the forward result, so beta/zeta/iota reduction cannot discard it. Removing this step leaves the necessary direction unproved. The reverse direction also constructs the positive representative function i+1 on its live path.

For card_choosable_eq_superdiagonal, the same four checks hold separately: (i) #print shows Finset.filter_congr calling the new equivalence, whose forward implication calls prefix_capacity; (ii) neither cardinal/filter congruence nor the permutation theorem supplies the missing prefix bound; (iii) a local bound for a list prefix is not definitionally equivalent to an equality of partition counts for arbitrary n,k; (iv) filter congruence uses both directions of the equivalence, and the required predicate implication retains the prefix argument after eliminating unused terms. Without it the current proof cannot identify the two filters by bind-only operations.

choosableInitial_congr_perm is the thin transport of Mathlib’s List.perm_comp_forall₂ and List.Perm.nodup_iff, after the existing get/ofFn and nodup/injectivity correspondence changes representation. It is a companion for the explicit source obligation that choosability is order-independent. The live dependency direction is card_choosable_eq_superdiagonal -> choosableInitial_congr_perm; it is not an independent deposit or novelty claim.

utility: none: every public result quantifies over arbitrary lists or n,k; the private helpers are likewise symbolic. There are no bounded enumerations, checkers, numeric reductions or certified finite instances in the module. The finite diagnostics are external scratch artifacts, not frozen declarations. The other computational utility fields are not-applicable(kind=none).

Boundary verification

The corrected Lean scratch probe returned exit 0. Exhaustive finite-function enumeration computes exactly 1 SDR for [3,2,1] and 0 for [4,1,1]. The sorted superdiagonal indicators are respectively 1 and 0. Empty-list and zero-part SDR witness counts are respectively 1 and 0, and their superdiagonal truth values are respectively true and false. The probe also kernel-checks both predicates on [1,2,3], [1,1,4], [], [0], and permutation transport for the two descending partitions of six. It proves that any Nat.Partition(n) with zero parts has n=0. No representative lower bound or one-based index offset was dropped. Logs are in the runner attempt directory (boundaries.log).

The Problems entry’s section headings were checked: exactly Problem, Motivation, Gap, Route, Falsifier, Evidence, Triage, ASSUMED-UNVERIFIED.

make lean-report LAKE_JOBS=3 returned exit 0. The source-bound raw report has SHA-256 8c290816084296ad6dae8245bdf8a7cacb4d10710fefae0405fb79c3c1fc483a. Its module source digest is 6c146b452d76f854614ce24f2177603f831f4103c8fa7169d1c785a68b817de2. All included theorem axiom closures are within the standard three; the semantic import list contains only Init and the three stated Mathlib modules. No private axiom, sorry, or extra source hypothesis is present.

Delivery checkpoint

The canonical ledger-align --add writer returned exit 0: selectors_considered=3874 changed=0 added=1 unchanged=3873 conflicts=0. The generated member statement identity is sha256:2406015af8528d11f15b1a7cd4ea422f1b83e81c2f4a47c1c55482ebbc0a8d30; the accepted event is sha256:f3877ae7e5693e17463ee578bcf051194d65e79e2e39e758b78b5a9b4583d36e. The event’s prerequisite_frozen_node_ids is empty, consistent with the per-declaration dependency report. make emit returned exit 0 and generated exactly this module’s Blueprint Markdown; no generated Markdown was edited.

Pre-PR duplicate check on fetched dev b2f83a3306b7aed53f1c2d2a3980a9855d3331af: git grep -n -i -P 'A388711|choosableInitial|superdiagonal reversed' origin/dev -- 'D5/**/*.lean' returned no lines. A positive-control rg with the same alternation syntax, \b(firstSums|IsFirstSums)\b on the existing Compositions module, returned 17 lines. git merge-tree --write-tree origin/dev HEAD exited 0 with no conflicts. These checks do not change the fixed implementation baseline. git diff --check also exited 0. The final diff has the requested seven files; PR and required-CI outcomes are recorded in the runner result.

The local proof and gate outcomes are recorded above. PR #6585 was opened through make pr-open with AUTO_MERGE=1; its terminal CI and merge outcomes belong to the runner report. The caller’s literature search is not exhaustive and does not establish that no published, private, or unindexed proof exists. ASSUMED-UNVERIFIED: the existence or absence of such other proofs. No novelty of the elementary SDR criterion, first-publication priority, or implication to a larger conjecture is claimed.

Verified locator

• URL: https://oeis.org/A388711
• Opened machine-readable entry: https://oeis.org/search?q=id:A388711&fmt=json
• Scope checked on 2026-09-09: name, choosability and initial-interval definitions, conjecture comment, author date and creation date (revision 7).

The first PR run failed its Scribe content check. The worker reproduced RED code=incomplete-library-locator locally: this note had its source URL in frontmatter and prose but omitted the template’s required locator section. This section supplies that missing source binding. The Lean proof and frozen identities are unchanged. The same Scribe entry point returned exit 0 after this fix: DESCRIBE_STATUS ... red=0 and markdown: judged=1 formula(s)=5 red=0.