{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R470",
  "content_hash": null,
  "slug": "life6-claim-suffix-upper-bound",
  "type": "claim",
  "title": "An independent-state suffix relaxation gives a rigorous search bound",
  "summary": "A 4,096-state recurrence bounds every common output suffix and makes the exhaustive prefix search small.",
  "relevance": "This records a result, observation, or conjecture used to assess the target problem.",
  "relevance_source": "derived",
  "body": "Let \\(N_s(z)\\) be the number of predecessor-row suffixes that begin in state \\(s=(a,b)\\), produce the specified output-row suffix \\(z\\), and end at the forced zero boundary. Define \\(U_1(a,b)=1\\). For \\(r\\geq2\\), set\n\\[\nU_r(a,b)=\\max_y\\sum_{c:F(a,b,c)=y}U_{r-1}(b,c).\n\\]\nInduction gives\n\\[\nN_s(z)\\leq U_r(s)\n\\]\nfor every length-\\(r\\) suffix \\(z\\). The recurrence may combine a different best tail for each choice of \\(c\\), so it can overestimate. This direction is safe for pruning.\n\nAfter an output prefix, let \\(v_s\\) be the exact number of compatible predecessor prefixes ending in state \\(s\\). Every common remaining suffix then has at most\n\\[\n\\sum_s v_s U_r(s)\n\\]\nfull predecessors. The root value of this bound is 53,245,419. Recomputing the exact vectors after each chosen output row tightens it enough to close the search after 988 internal prefix nodes. This establishes the upper-bound logic independently of any heuristic ordering.",
  "status": "established",
  "evidence_grade": "mathematical_identity",
  "scope": {
    "kind": "bounded",
    "statement": "all row-transfer states and all output suffix lengths from one through six for the fixed-dead 6 by 6 Life map",
    "bounds": {
      "row_states": {
        "min": 4096,
        "max": 4096
      },
      "suffix_length": {
        "min": 1,
        "max": 6
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.1063/1.5006143",
      "locator": "Inductive bound implemented and checked in life6-artifact-row-transfer-branch-and-bound"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1063/1.5006143",
    "locator": "Inductive bound implemented and checked in life6-artifact-row-transfer-branch-and-bound"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R469",
      "title": "The exact maximum preimage multiplicity is 1,093,273",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "life-six-preimage-multiplicity",
      "title": "life six preimage multiplicity",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}