bibkey: oeis2026a382427
authors: OEIS Foundation Inc.
year: 2025
title: OEIS A382427
doi: null
url: https://oeis.org/A382427
claim: Constant-block partitions with distinct sums exist exactly when the parts have an ordering with distinct maximal run sums.
strata_touched:
  - D5/S1/Words/Compositions/ConstantBlocksDistinctRunSums
license: citation-only
triage: anchor

OEIS A382427

Verified locator

Canonical entry URL: https://oeis.org/A382427.

On September 10, 2026 the worker fetched the complete JSON entry at https://oeis.org/search?q=id:A382427&fmt=json, revision 13, including all fields without truncation. The entry is authored March 26, 2025 and created March 28, 2025. Offset is zero. Its exact name is:

Number of integer partitions of n that can be partitioned into constant blocks with distinct sums.

Its exact conjectural comment is:

Conjecture: Also the number of integer partitions of n having a permutation with all distinct run-sums.

The complement A381717, revision 15, explicitly states the pointwise iff and still labels it Conjecture. A382876, revision 22, defines run-sums by splitting a sequence into maximal runs and taking their sums. Its zero-set link to A381636 is still phrased as an appearance, not a proved result.

Provenance and preregistration

Skill: lean4. Carrier: this Codex worker in the supplied worktree on lane/math/a382427, starting from dev commit 006b4f90f1125181e888425f1e3875a1230c8c94. Division: one worker handles source inspection, proof, diagnostics and Scribe; no independent review is claimed. The four named frozen Compositions siblings and CLAUDE.md were read. No atom identifier was supplied, so the explicit OEIS brief is the source obligation; atom ingestion and cover are not applicable.

Before creating the module, the worker preregistered this escape witness in the runner report: a minimum-block decomposition satisfies the color count bound because an overrepresented color admits a distinct-sum merge. The largest same-color sum plus each of the remaining same-color sums gives more candidates than there are other-color blocks. Then construct an ordering with adjacent colors different. The final proof follows this preregistered route; finite enumeration is only diagnostic.

The caller’s proposed implication for an arbitrary decomposition was explicitly ASSUMED-UNVERIFIED. It is false: split three ones into lengths 1 and 2. The block sums are 1 and 2, but the maximum color count is 2 and the total block count is 2. Merging gives a valid single run of sum 3. The minimum-block restriction is the substantive missing step.

Ordered search and bind-only attempt

The complement A381717 was fetched and read first. All 35 distinct A-numbers in A382427’s comment/formula/xref were then fetched using the exact https://oeis.org/search?q=id:<A-number>&fmt=json form and read in full:

A000009, A000041, A000688, A001055, A006171, A045778, A047966, A050361, A265947, A279784, A279786, A295935, A300383, A300385, A317141, A326535, A353864, A355743, A381453, A381455, A381633, A381635, A381636, A381716, A381717, A381718, A381990, A381991, A381992, A381993, A382075, A382079, A382203, A382301, A382876.

The full responses total 207555 bytes. No field was discarded; readable views split only between complete fields. Truncated tool displays were reread. The target-relevant comments remain conjectural; no proof of this target was found in the entries. Classical partition identities in other entries do not establish the required realizability implication. The search does not recursively claim coverage of all xrefs of all xrefs.

The frozen D5 search used 382427|381717|run.?sums|constant blocks|rearrang|adjacent.*equal. It found no matching target. Pinned Mathlib and Batteries List, Multiset, and Combinatorics sources were searched for rearrangements, adjacent-color chains, run sums and constant blocks. The Mathlib pin is db584cd6d46c92f209a44c0f1c829460d327499d, Lean v4.33.0. An initial Mathlib search before cache setup had unavailable paths and is not counted as a negative result; searches were repeated after ensure. The positive API control is List.splitBy_flatten: it reconstructs maximal runs from nonempty constant lists with different boundary values. No direct balanced color ordering or target equivalence was located in this scope.

The elaborated bind-only probe defined both source predicates and tried definition expansion and simp on the Nat.Partition iff. It returned exit 1 with the full existential equivalence still unsolved. Ancillary unknown API names in that scratch file are distinct from this meaningful failure. This alone is not an impossibility proof: inspection identifies the absent live content as the minimum-block merge and the color ordering construction. No frozen D5 dependency is imported or re-proved.

After local inspection, exact GitHub code searches with language:Lean for A382427 and “run sums” returned no hits. “constant blocks” returned two unrelated Kakeya refinement paths. No third-party dependency was added. General web search was inconclusive: Google returned a redirect page; Bing exact queries returned irrelevant results. These are recorded as limitations, not evidence of literature absence. The mandatory complete OEIS/xref inspection supplies the direct source status check.

Formal definitions and proof

HasConstantBlocks(m) quantifies over a finite set of pairs (v,c), each with v>0 and c>0. Their weights v*c are injective on the whole set, and the multiset sum of replicate(c,v) is exactly m. Distinct weights prohibit duplicate identical pairs, so this set encoding faithfully represents multiset block decompositions. Equal sums from either equal or different values are excluded. Multiplicity one permits exactly the singleton block.

runSums(l) is (l.splitBy (· == ·)).map List.sum. HasDistinctRunSums(m) requires a list l with (l : Multiset Nat) = m and Nodup(runSums(l)). This is existence of a permutation, with maximal runs; it does not count permutations or require all permutations to work.

The minimum is supplied by Nat.find on block count. In minimal_balanced, assume k same-value blocks and o other blocks with k>o+1. Let a be a block of maximum same-value weight. The k-1 candidates w(a)+w(b) are injective because old weights are injective. Positivity puts every candidate above every existing same-value weight. If all candidates occurred among the old weights, the candidate image would inject into at most o other-value weights, contradicting cardinality. A candidate outside that image supplies a merge. The proof checks positivity, injectivity, preservation of the multiset sum, and a decrease in cardinality. Thus 2k <= total+1.

order_colors uses strong induction on the finite set’s cardinality. Its invariant for forbidden first color p is 2k_c <= total+[c differs from p]. Choose a block whose eligible color has maximum cardinality. After erasing it, its own count decreases; two disjoint color fibers bound the remaining counts. The invariant therefore holds with the chosen color forbidden. Starting with p=0 is valid because block values are positive. The returned list is nodup, represents the same finite set, and has adjacent colors different. splitBy_flatten then certifies its expanded blocks as the actual maximal runs. The reverse direction encodes each actual run by head and length and reconstructs its constant entries from its equality chain.

The public pointwise theorem takes an arbitrary Nat.Partition(n); positivity comes from parts_pos. The count theorem identifies filters of the same finite universe, so counts partitions, not block decompositions or orderings.

Per-declaration proof shape

For the pointwise theorem, the four escape checks hold: (i) its elaborated forward implication calls blocks_to_runs, whose live path uses exists_balanced/minimal_balanced and order_colors; (ii) neither the imported finite cardinal lemmas nor run-splitting lemmas provide the merge or ordering; (iii) a local inequality for one color in a minimum decomposition is not definitionally equivalent to the existential iff; (iv) its result discharges the actual ordering precondition, so reduction cannot discard it.

For the count theorem, separately: (i) filter extensionality invokes the pointwise equivalence; (ii) filter/cardinality normalization supplies no realizability implication; (iii) the local merge lemma is not an equality of partition counts; (iv) after inlining the new local theorem, its forward construction is retained in the filter identification. It is content under the rule that same-deposit declarations are inlined, not treated as frozen. The three public definitions are the source predicates and observable run-sum transformation, not extra theorem claims. There are no standalone binding-only theorem deposits.

utility: none: both public theorems quantify over arbitrary n or partitions; all private lemmas are symbolic. No finite instance, enumerator or executable checker is deposited. Diagnostic code and numeric examples remain external. Other utility fields are not-applicable(kind=none).

Validation checkpoints

The runner attempt directory contains the complete source responses, enumeration.py/json, binding and API probes, compiler logs, and an ongoing report. The artifact directory is /var/folders/wv/ht3wzsj138b4sxl3q4t0xdr40000gn/T/consensus-rnd/sshx/a382427-impl-0910/attempt-1.

Cache ensure succeeded with status seeded, method clonefile, both layers warm, and zero missing Mathlib oleans. The actual post-ensure project difference was 8 missing modules among 3966 Lean sources; warm alone was not treated as validity evidence. Baseline make lean exited 0 in 39.84 s with RSS 5907759104 bytes. No LAKE_JOBS was set. The final proof build exited 0 in 10.83 s with RSS 1581121536 bytes (12803 jobs).

Each compiled logical unit was committed and pushed: color ordering, minimum-block balance, then the full pointwise and counting theorems. The full source compiles without warnings and both theorem axiom closures are exactly propext, Classical.choice and Quot.sound.

Independent Python algorithms compare the qualifying partition sets at n=0,…,11, not just cardinalities. They reproduce the OEIS DATA prefix 1,1,2,3,4,7,11,14,19,28,39,50. Empty decompositions and empty runs both give one qualifying partition at n=0.

The Lean scratch diagnostic imports the production module and uses its exact runSums definition and the unfolded left witness predicate. It exits 0 and computes the following witness counts (these count witnesses, not qualifying partitions, so the two columns need not be equal):

For the nonempty positive example, the blocks (1,1),(2,1),(3,1),(2,2) are directly checked against the production left predicate; the actual list 1,2,3,2,2 has computed run sums 1,2,3,4. Kernel examples establish both existential predicates on this multiset and on the empty multiset. The diagnostic also computes the three-ones counterexample to the caller’s balance observation and rejects repeated sums [1,1]. No native_decide or diagnostic axiom is introduced. The left finite search bounds c by the input multiplicity of v; the right search enumerates actual permutations. The extended Lean diagnostic also proves both actual Nat.Partition(0) filter cardinalities equal 1, using Mathlib’s unique empty partition.

The source-bound make lean-report exits 0 in 68.44 s. Its delta plan is changed=0, added=2, recheck=2. The producer supervisor reports peak RSS 4082848 KB; /usr/bin/time reports 3148152832 bytes, a different metric. The report digest is 01e4d59cb6be1b1170ae93ebac7e78fd3dbc53c105c650886d4020128fc83eb5; the module source digest is e4f5c98c7882352b8dd35d5040cea4e78d8f42e055bebb0f550e9fd8a84f7dfa. All 39 reported declarations have axiom sets contained in the standard three, and the report source digest matches the deposited source.

Canonical ledger-align with –add on this module alone exits 0: added=1, changed=0, conflicts=0. Its accepted event is cec534b0e9712cc4f3074eb434c84f5ba777edd9e5164b376eb354d133bb5d46. The pointwise theorem statement ID is sha256:db15fc59c3e42b65832331fdc5545a03231b7f53a8a9f987efa997261ddb6534; the counting theorem statement ID is sha256:f71d6ab8b62a9fe028a3aea0cb220f0db214190399f49b81b84ad948ad164dee. No previously frozen module is modified. Scribe emission and PR status are recorded in the runner result after their actual receipts exist.

The first PR’s complete content check exposed an incomplete locator: the section contained the JSON endpoint but omitted the exact canonical URL stored in frontmatter. Adding that URL binds the required locator. The same content-check script then exits 0 locally with describe red=0 and markdown: judged=1 formula(s)=5 red=0. Proof source and frozen identities are unchanged by this documentary correction.

Unclaimed

No exhaustive literature search, absence of all prior proofs, novelty of the familiar color-ordering criterion, first-publication priority, or independent multi-model review is claimed. The caller’s Section III observation was ASSUMED-UNVERIFIED and is refuted for arbitrary witnesses; only its corrected minimum-block version is used and proved. Finite data is not an unbounded proof. Source-to-definition fidelity is a documentary assessment; the kernel verifies the explicit Lean statements.