{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R741",
  "content_hash": null,
  "slug": "ssclt-artifact-bitpacked-dp",
  "type": "artifact",
  "title": "Bit-packed exact subset-sum computation through n=1000",
  "summary": "One Python integer stores the complete coefficient table in base 2^1001, allowing exact shift-and-add polynomial multiplication.",
  "relevance": "For Eventual monotonicity in a signed subset-sum local limit, record ssclt-artifact-bitpacked-dp (“Bit-packed exact subset-sum computation through n=1000”) supplies evidence or a replay used to check the packet. The record states: One Python integer stores the complete coefficient table in base 2^1001, allowing exact shift-and-add polynomial multiplication.",
  "relevance_source": "recorded",
  "body": "Set \\(B=2^{1001}\\) and encode \\(F_n(x)=\\sum_sc_{n,s}x^s\\) as the integer \\(P_n=\\sum_sc_{n,s}B^s\\). Every coefficient is below \\(2^n<B\\), so base-\\(B\\) digits never carry into each other. Multiplication by \\(1+x^n\\) is therefore the single exact operation\n```\nP_n = P_{n-1} + (P_{n-1} << (1001*n)).\n```\nA mask extracts the desired base-\\(B\\) digit. The program asserts known counts, constructs all cleared comparison margins, and requires every post-16 margin to be positive.\n\nThe canonical `n:count:variance` record has SHA-256 digest `c42ba94e917ea48f4c8761938c3e52989f5a01143bb0bc34dedd19425eb417dc`. The canonical `a,b:margin` record has digest `d28f8f888dedb6d9fb9f27858685d315a242c7276e9e73c40a0a47f0a15ac8b5`. The ten-line output digest is `1c970286ddadc5532e0766c4e36bd3acdb5c898d358435e9999f0108909831e2`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all central coefficients and adjacent normalized comparisons at positive admissible n through 1000",
    "bounds": {
      "maximum_n": {
        "min": 1000,
        "max": 1000
      },
      "central_coefficients": {
        "min": 500,
        "max": 500
      },
      "post_16_comparisons": {
        "min": 492,
        "max": 492
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_computation",
    "entrypoint": "join source_lines with newline and run with python3",
    "runtime": "CPython 3, standard library only; about 25 seconds on the reference workspace",
    "citation": {
      "url": "https://cs.uwaterloo.ca/journals/JIS/VOL16/Sullivan/sullivan8.html",
      "locator": "Inline CPython standard-library computation executed on 2026-07-24"
    },
    "outputs": "admissible_records=500 last_n=1000\npost16_comparisons=492 all_strict=true\ndecreases=3->4,8->11,15->16\ncount_n16=1314\ncount_n200=780463610226751719065842218999070243255558586796769387244\nnormalized_n16=0.775498980775123\nnormalized_n999=0.797525249765113\nnormalized_n1000=0.797525608979770\nrecords_sha256=c42ba94e917ea48f4c8761938c3e52989f5a01143bb0bc34dedd19425eb417dc\ncomparisons_sha256=d28f8f888dedb6d9fb9f27858685d315a242c7276e9e73c40a0a47f0a15ac8b5\n",
    "inline_source": [
      "from decimal import Decimal, getcontext",
      "from hashlib import sha256",
      "N=1000",
      "W=N+1",
      "MASK=(1<<W)-1",
      "poly=1",
      "records=[]",
      "for n in range(1,N+1):",
      "    poly += poly << (n*W)",
      "    if n%4 in (0,3):",
      "        target=n*(n+1)//4",
      "        count=(poly>>(target*W))&MASK",
      "        variance=n*(n+1)*(2*n+1)//6",
      "        records.append((n,count,variance))",
      "def margin(left,right):",
      "    a,ca,qa=left; b,cb,qb=right",
      "    return cb*cb*qb-ca*ca*qa*(1<<(2*(b-a)))",
      "comparisons=[(records[i-1][0],records[i][0],margin(records[i-1],records[i])) for i in range(1,len(records))]",
      "decreases=[(a,b) for a,b,m in comparisons if m<0]",
      "post=[(a,b,m) for a,b,m in comparisons if a>=16]",
      "assert len(records)==500 and records[-1][0]==1000",
      "assert len(post)==492 and all(m>0 for _,_,m in post)",
      "assert decreases==[(3,4),(8,11),(15,16)]",
      "by_n={n:(c,q) for n,c,q in records}",
      "assert by_n[16][0]==1314",
      "assert by_n[100][0]==1731024005948725016633786324",
      "assert by_n[200][0]==780463610226751719065842218999070243255558586796769387244",
      "record_raw=''.join(f'{n}:{c}:{q}\\n' for n,c,q in records)",
      "comparison_raw=''.join(f'{a},{b}:{m}\\n' for a,b,m in comparisons)",
      "rh=sha256(record_raw.encode()).hexdigest()",
      "ch=sha256(comparison_raw.encode()).hexdigest()",
      "assert rh=='c42ba94e917ea48f4c8761938c3e52989f5a01143bb0bc34dedd19425eb417dc'",
      "assert ch=='d28f8f888dedb6d9fb9f27858685d315a242c7276e9e73c40a0a47f0a15ac8b5'",
      "getcontext().prec=30",
      "def normalized(n):",
      "    c,q=by_n[n]",
      "    return Decimal(q).sqrt()*Decimal(c)/(Decimal(2)**n)",
      "print('admissible_records=500 last_n=1000')",
      "print('post16_comparisons=492 all_strict=true')",
      "print('decreases=3->4,8->11,15->16')",
      "print(f'count_n16={by_n[16][0]}')",
      "print(f'count_n200={by_n[200][0]}')",
      "print(f'normalized_n16={normalized(16):.15f}')",
      "print(f'normalized_n999={normalized(999):.15f}')",
      "print(f'normalized_n1000={normalized(1000):.15f}')",
      "print(f'records_sha256={rh}')",
      "print(f'comparisons_sha256={ch}')"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://cs.uwaterloo.ca/journals/JIS/VOL16/Sullivan/sullivan8.html",
    "locator": "Inline CPython standard-library computation executed on 2026-07-24"
  },
  "models": [],
  "relations": [
    {
      "slug": "R745",
      "title": "All 492 comparisons through n=1000 are strict increases",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "R743",
      "title": "The all-n monotonicity claim remains unresolved in this audit",
      "object_type": "claim",
      "relation": "tests",
      "direction": "outgoing"
    },
    {
      "slug": "signed-subset-sum-local-clt-monotone",
      "title": "signed subset sum local clt monotone",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}