bibkey: wu2023a367400 authors: Gus Wiseman; Chai Wah Wu year: 2023 title: “OEIS A367400: cardinality-sum-avoiding subsets” doi: null url: https://oeis.org/A367400 claim: “G.f.: (-x^3 + x^2 + 1)/(x^4 - 2x^3 + x^2 - 2x + 1).” strata_touched:

• D5/S3/Combinatorics/CardinalitySumAvoidingSubsets license: citation-only triage: anchor

OEIS A367400

The original entry is by Gus Wiseman, November 21, 2023. Its NAME is:

Number of subsets of {1..n} whose cardinality is not the sum of two distinct elements.

The formulas are explicitly introduced as conjectures by Chai Wah Wu, November 21, 2023:

a(n) = 2a(n-1) - a(n-2) + 2a(n-3) - a(n-4) for n > 3.

G.f.: (-x^3 + x^2 + 1)/(x^4 - 2x^3 + x^2 - 2x + 1).

The canonical definition takes the cardinality of the powerset of [1,n] filtered by the distinct-elements condition. The empty subset contributes one at every n, including n=0. An even-cardinality subset may contain its midpoint k/2: the prohibited pair must have two distinct elements.

The formal result proves the denominator-multiplied generating-function identity over Q[[X]]. The denominator has constant coefficient one, so this is equivalent to the quoted rational formal series. The recurrence is a coefficient consequence; it is not a separately retained theorem.

Verified locator

Official OEIS entry: https://oeis.org/A367400. The checked source is the internal page at https://oeis.org/A367400/internal.

Source and license

Official source: https://oeis.org/A367400/internal. Source readout at 2026-09-30 15:11 UTC: HTTP 200, with NAME, conjecture label, formulas and AUTHOR as quoted above. HTML SHA-256: 2a0b56602fc5b473a65c107d70aee87f667e293788f4d9ffddf7d654621c58c0.

The OEIS End-User License Agreement at https://oeis.org/wiki/The_OEIS_End-User_License_Agreement states that OEIS is available under Creative Commons Attribution Share-Alike 4.0 (CC-BY-SA-4.0). The citation-only field describes this note’s use of short attributed quotations; it does not change the OEIS license. Mathlib’s reused Lean sources are under Apache-2.0. No external Lean proof code is copied.

Literature scope

The source remains labeled a conjecture in the checked OEIS entry. The supplied bounded source scope comprises A367396, A112575 and Huang, arXiv:2501.07463v2; no exact original-count bridge is supplied from it. A shared generating-function denominator does not identify the underlying counting objects. Neither exhaustive literature absence nor publication priority is asserted. The counting bridge in the Lean module is a repository derivation from the original predicate.