{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R585",
  "content_hash": null,
  "slug": "pnc-artifact-three-way-exact-verifier",
  "type": "artifact",
  "title": "Exact recurrence, inclusion-exclusion, and brute-force verifier",
  "summary": "Standard-library Python checks all 501 recurrence terms, inclusion-exclusion through 80, direct enumeration through 9, and every probability comparison through 500.",
  "relevance": "For Monotonicity of consecutive-adjacency avoidance in random permutations, record pnc-artifact-three-way-exact-verifier (“Exact recurrence, inclusion-exclusion, and brute-force verifier”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python checks all 501 recurrence terms, inclusion-exclusion through 80, direct enumeration through 9, and every probability comparison through 500.",
  "relevance_source": "recorded",
  "body": "The program builds \\(a_0,\\ldots,a_{500}\\) from Riordan's recurrence. It independently evaluates the run-based inclusion-exclusion formula through size 80 and enumerates every permutation through size 9. It verifies the first-difference identity used in the proof and all strict comparisons \\(p_n>p_{n-1}\\) for \\(4\\leq n\\leq500\\) using exact rational arithmetic.\n\nThe compact JSON array of all 501 counts is 257,598 bytes and has SHA-256 digest `057d0a8c39cfc574ba2d08470fdbe863460b6d7ccb669aea42afe3519099b3ca`. The complete five-line output is 660 bytes including its final newline, with SHA-256 digest `809a8620b1a1cd257d8a275e8e15172a15ed0913ca0ef5c9b3da07de1d5f2394`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "exact counts and normalized probabilities through size 500, with independent checks at smaller sizes",
    "bounds": {
      "n": {
        "min": 0,
        "max": 500
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "runnable",
    "kind": "inline_python_computation",
    "command": "python3 check.py",
    "entrypoint": "Join source_lines with newline and run with python3",
    "runtime": "CPython 3, standard library only",
    "citation": {
      "url": "https://oeis.org/A002464",
      "locator": "Inline CPython source below, executed on 2026-07-24"
    },
    "inline_source": [
      "from decimal import Decimal, getcontext",
      "from fractions import Fraction",
      "from hashlib import sha256",
      "from itertools import permutations",
      "from json import dumps",
      "from math import comb, factorial",
      "",
      "N=500",
      "a=[0]*(N+1)",
      "a[:4]=[1,1,0,0]",
      "for n in range(4,N+1):",
      "    a[n]=(n+1)*a[n-1]-(n-2)*a[n-2]-(n-5)*a[n-3]+(n-3)*a[n-4]",
      "",
      "def inclusion(n):",
      "    total=factorial(n)",
      "    for k in range(1,n):",
      "        runs=sum((1<<r)*comb(k-1,r-1)*comb(n-k,r) for r in range(1,k+1))",
      "        total+=(-1 if k&1 else 1)*factorial(n-k)*runs",
      "    return total",
      "",
      "def brute(n):",
      "    return sum(all(abs(x-y)!=1 for x,y in zip(p,p[1:]))",
      "               for p in permutations(range(1,n+1)))",
      "",
      "assert [brute(n) for n in range(10)]==a[:10]",
      "assert all(inclusion(n)==a[n] for n in range(81))",
      "p=[Fraction(a[n],factorial(n)) for n in range(N+1)]",
      "assert p[4]>p[3]",
      "for n in range(5,N+1):",
      "    numerator=(n-2)*p[n-2]-(n-5)*p[n-3]+p[n-4]",
      "    assert n*(p[n]-p[n-1])==p[n-1]-p[n-2]+numerator/Fraction((n-1)*(n-2))",
      "    assert numerator==3*p[n-3]+p[n-4]+(n-2)*(p[n-2]-p[n-3])",
      "    assert p[n]>p[n-1]",
      "",
      "raw=dumps(a,separators=(',',':')).encode()",
      "getcontext().prec=30",
      "print('counts_4_to_20',' '.join(f'{n}:{a[n]}' for n in range(4,21)))",
      "print('checked recurrence 4..500 inclusion_exclusion 0..80 brute_force 0..9 monotone_probabilities 4..500')",
      "print('count_table_0_to_500_bytes',len(raw),'sha256',sha256(raw).hexdigest())",
      "print('selected_probabilities',' '.join(f'{n}:{Decimal(a[n])/Decimal(factorial(n)):.18f}' for n in [4,5,10,20,50,100,500]))",
      "print('minimum_integer_cross_difference',min((a[n+1]-(n+1)*a[n],n) for n in range(4,N)))"
    ],
    "missing": [
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://oeis.org/A002464",
    "locator": "Inline CPython source below, executed on 2026-07-24"
  },
  "models": [],
  "relations": [
    {
      "slug": "R587",
      "title": "Inclusion-exclusion gives the classical Hertzsprung numbers",
      "object_type": "claim",
      "relation": "tests",
      "direction": "outgoing"
    },
    {
      "slug": "R588",
      "title": "The avoidance probability is strictly increasing for every n at least 4",
      "object_type": "claim",
      "relation": "tests",
      "direction": "outgoing"
    },
    {
      "slug": "permutation-no-consecutive-adjacency-monotone",
      "title": "permutation no consecutive adjacency monotone",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}