{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R638",
  "content_hash": null,
  "slug": "r2s6-claim-monotone-in-clause-count",
  "type": "claim",
  "title": "Satisfiability probability decreases with the number of clauses",
  "summary": "Deleting a uniformly chosen clause from a uniform (m+1)-set gives a uniform m-set, and deletion preserves satisfiability.",
  "relevance": "For Median satisfiability threshold for a six-variable clause set, record r2s6-claim-monotone-in-clause-count (“Satisfiability probability decreases with the number of clauses”) records a bound, answer, status fact, or structural consequence. The record states: Deleting a uniformly chosen clause from a uniform (m+1)-set gives a uniform m-set, and deletion preserves satisfiability.",
  "relevance_source": "recorded",
  "body": "Write \\(P_m\\) for the satisfiability probability of a uniformly chosen \\(m\\)-element clause set. Sample a uniform \\((m+1)\\)-element set \\(F\\), then delete one of its clauses uniformly. The resulting \\(m\\)-set is uniform because every \\(m\\)-set has the same number of one-clause extensions and every extension has the same deletion probability.\n\nIf \\(F\\) is satisfiable, every subset of \\(F\\) is satisfiable. Under this coupling, the satisfiability indicator after deletion is at least its value before deletion. Taking expectations gives\n\\[\nP_m\\geq P_{m+1}.\n\\]\nThus exact inequalities at 12 and 13 clauses determine whether 13 is the first crossing below one half.",
  "status": "established",
  "evidence_grade": "mathematical_identity",
  "scope": {
    "kind": "bounded",
    "statement": "uniform m-element subsets of any fixed finite clause universe, compared with uniform (m+1)-element subsets from the same universe",
    "bounds": {
      "available_clauses": {
        "min": 1
      },
      "clauses": {
        "min": 0
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.5070/C63261985",
      "locator": "Elementary deletion coupling recorded by TheoremDB entry research on 2026-07-25"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.5070/C63261985",
    "locator": "Elementary deletion coupling recorded by TheoremDB entry research on 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R636",
      "title": "The exact thirteen-clause coefficient remains to be extracted",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "outgoing"
    },
    {
      "slug": "random-two-sat-six-median",
      "title": "random two sat six median",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}