{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R588",
  "content_hash": null,
  "slug": "pnc-claim-strict-probability-monotonicity",
  "type": "claim",
  "title": "The avoidance probability is strictly increasing for every n at least 4",
  "summary": "Riordan's four-term recurrence yields a positive recurrence for the first differences of a(n)/n!.",
  "relevance": "For Monotonicity of consecutive-adjacency avoidance in random permutations, record pnc-claim-strict-probability-monotonicity (“The avoidance probability is strictly increasing for every n at least 4”) records a bound, answer, status fact, or structural consequence. The record states: Riordan's four-term recurrence yields a positive recurrence for the first differences of a(n)/n!.",
  "relevance_source": "recorded",
  "body": "Let \\(a_n\\) count the admissible permutations and put \\(p_n=a_n/n!\\). The exact recurrence in the companion claim is\n\\[\na_n=(n+1)a_{n-1}-(n-2)a_{n-2}-(n-5)a_{n-3}+(n-3)a_{n-4}\\qquad(n\\geq4),\n\\]\nwith \\(a_0=a_1=1\\) and \\(a_2=a_3=0\\).\n\nSet \\(\\Delta_n=p_n-p_{n-1}\\). Dividing the recurrence by \\(n!\\), subtracting \\(p_{n-1}\\), and collecting terms gives\n\\[\nn\\Delta_n=\\Delta_{n-1}+\n\\frac{(n-2)p_{n-2}-(n-5)p_{n-3}+p_{n-4}}\n{(n-1)(n-2)}. \\tag{1}\n\\]\nThe numerator in the fraction has the useful form\n\\[\n3p_{n-3}+p_{n-4}+(n-2)(p_{n-2}-p_{n-3}). \\tag{2}\n\\]\n\nNow \\(p_2=p_3=0\\) and \\(p_4=2/4!=1/12\\), so \\(\\Delta_4>0\\). For \\(n=5\\), the comparison needed in (2) is \\(p_3\\geq p_2\\). At every later step it follows from the preceding induction cases. All probabilities are nonnegative, so (2) is nonnegative. Equation (1) then gives \\(\\Delta_n>0\\) from \\(\\Delta_{n-1}>0\\). Induction proves \\(p_n>p_{n-1}\\) for every \\(n\\geq4\\). Replacing \\(n\\) by \\(n+1\\) answers the stated question:\n\\[\n\\boxed{p_{n+1}>p_n\\quad\\text{for every }n\\geq4.}\n\\]",
  "status": "established",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "universal",
    "statement": "every comparison p_(n+1) > p_n for n at least 4"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.1214/aoms/1177700181",
      "locator": "Riordan's recurrence plus the self-contained first-difference induction in this record"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1214/aoms/1177700181",
    "locator": "Riordan's recurrence plus the self-contained first-difference induction in this record"
  },
  "relations": [
    {
      "slug": "R587",
      "title": "Inclusion-exclusion gives the classical Hertzsprung numbers",
      "object_type": "claim",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R585",
      "title": "Exact recurrence, inclusion-exclusion, and brute-force verifier",
      "object_type": "artifact",
      "relation": "tests",
      "direction": "incoming"
    },
    {
      "slug": "R586",
      "title": "The counts and recurrence are classical Hertzsprung material",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "R1696",
      "title": "Direct answer and proof for Monotonicity of consecutive-adjacency avoidance in random permutations",
      "object_type": "claim",
      "relation": "supersedes",
      "direction": "incoming"
    },
    {
      "slug": "permutation-no-consecutive-adjacency-monotone",
      "title": "permutation no consecutive adjacency monotone",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}