bibkey: oeis2006a115809
authors: Antti Karttunen
year: 2006
title: "OEIS A115809: seventeen-times binary carryless multiplier condition"
doi: null
url: https://oeis.org/A115809
claim: "A115809 defines integers k satisfying 17*k = A048720(49,k) and asks whether it is a subset of A115801, whose defining condition is 9*k = A048720(25,k)."
strata_touched:
  - D5/S1/Digit/Admissibility/CarrylessSeventeenNineContainment
license: citation-only
triage: anchor

The seventeen-times containment question

A115809, revision 5, names the integers satisfying 17*k = 49 X k. Its comment specifies that * is ordinary multiplication and X is carryless multiplication in GF(2)[X], using A048720. The cross-reference asks: Cf. Subset of A115801 ? The author line attributes the entry to Antti Karttunen in 2006.

A115801, revision 20, defines the nonnegative integers satisfying 9*k = A048720(25,k). A048720, revision 62, defines binary polynomial multiplication over GF(2). The containment question therefore asks whether, for every natural number k, 17*k = C(49,k) implies 9*k = C(25,k). The same k occurs throughout, zero is included, and the other products are ordinary natural-number products.

The operation and question are from these entries. The universal containment proof uses a finite closed relation of carry states.

Verified locator

• Question: https://oeis.org/A115809 and https://oeis.org/A115809/internal, revision 5. NAME gives the seventeen-times condition, COMMENTS distinguishes ordinary and carryless multiplication, and CROSSREFS contains Cf. Subset of A115801 ?.
• Original question: https://oeis.org/history?seq=A115809, displayed initialization revision 1 from 2006. It contains the same condition, carryless clarification, subset question and initial zero.
• Target definition: https://oeis.org/A115801/internal, revision 20, NAME: Numbers k such that 9*k = A048720(25,k).
• Operation: https://oeis.org/A048720/internal, revision 62, NAME and FORMULA: two-input binary polynomial multiplication over GF(2), with binary exclusive-OR recursion.

Literature and library scope

The qualified literature scope comprises the OEIS records and displayed history above, arXiv exact-ID metadata, two inspected AI-OEIS papers, the complete pinned 492-item benchmark metadata/samples/mapping, and 38 published APN OEIS files. No exact answer was identified in the papers or exact-ID metadata; the benchmark and published APN files contain no target or alias ID. The papers report 44 APN proofs: the unread unpublished remainder, private or unindexed work, and semantically equivalent answers outside these reads remain outside the qualified scope. Current OEIS text retains the question; worldwide openness and priority are unverified. The bounded source qualification is recorded at https://github.com/the-omega-institute/trureturing/issues/23260.

Repository searches, including private D5 declarations, and lexical searches of mathlib at 56a005855ea17e0b0958f73ec801ae140b0a1679 identified no pre-existing exact answer within their search scope. The containment proof directly reuses existing generic carryless machinery. Accessible Loogle query https://loogle.lean-lang.org/json?q=%22carryless%22 returned count: 0 and hits: []; this covers declarations whose names contain carryless, not semantic equivalents or every third-party library. GitHub code search returned HTTP 401, and LeanSearch supplied no usable body; neither supplies a negative search result.