{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R728",
  "content_hash": null,
  "slug": "skolem-artifact-one-sided-modular-replay",
  "type": "artifact",
  "title": "Exact Fibonacci and order-two modular replay",
  "summary": "Exact replay classifies all 2,401 tuples in the coefficient-and-initial box [-3,3]^4: 841 gain a zero witness through index 1000, 1,508 gain a complete modular nonzero certificate, and 52 remain inconclusive.",
  "relevance": "For Decidability of zeros in integer linear recurrence sequences, record skolem-artifact-one-sided-modular-replay (“Exact Fibonacci and order-two modular replay”) supplies evidence or a replay used to check the packet. The record states: Exact replay classifies all 2,401 tuples in the coefficient-and-initial box [-3,3]^4: 841 gain a zero witness through index 1000, 1,508 gain a complete modular nonzero certificate, and 52 remain inconclusive.",
  "relevance_source": "recorded",
  "body": "The repository replay has two exact parts. For \\(u_n=F_{n+1}\\), it enumerates the complete pair-state cycle modulo every integer \\(m\\) between 2 and 512. All 511 moduli have a nonnegative modular zero. The ordered row digest is `6eb196a28c2cac0d194ce1af150c99bdc5e64591ef0c163d3c4d79f43a76d082`.\n\nThe second part exhausts every tuple \\((a,b,u_0,u_1)\\in[-3,3]^4\\) for \\(u_{n+2}=au_{n+1}+bu_n\\). It checks exact integer terms through index 1000. For a row without a witnessed zero, it searches moduli 2 through 64. Each modular check follows the deterministic pair state until a repeat, so a zero-free completed orbit is a proof that no integer zero exists at any nonnegative index.\n\nThe partition has 841 witnessed rows, 1,508 rows with a modular nonzero certificate, and 52 inconclusive rows. Every certificate found already uses a modulus at most 11. Forty inconclusive rows have \\(b=\\pm1\\) and a checked negative zero within eight backward steps. The boundary lemma proves that such a negative zero blocks this certificate form for every modulus. The census makes no claim about an unwitnessed integer zero in an inconclusive row.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the Fibonacci shift modulo 2 through 512 and every order-two recurrence tuple in [-3,3]^4 under the stated witness and modular bounds",
    "bounds": {
      "order": {
        "min": 2,
        "max": 2
      },
      "coefficient_or_initial_value": {
        "min": -3,
        "max": 3
      },
      "integer_witness_index": {
        "min": 0,
        "max": 1000
      },
      "census_modulus": {
        "min": 2,
        "max": 64
      },
      "fibonacci_modulus": {
        "min": 2,
        "max": 512
      },
      "negative_index_depth": {
        "min": 1,
        "max": 8
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "complete",
    "kind": "repository_python_exact_modular_census",
    "command": "ulimit -t 30; api/.venv/bin/python tools/skolem_one_sided_modular_replay.py > skolem_one_sided_modular_replay.json",
    "entrypoint": "tools/skolem_one_sided_modular_replay.py",
    "runtime": "CPython 3.12.13 standard library, macOS 26.2 arm64",
    "source": "tools/skolem_one_sided_modular_replay.py",
    "citation": {
      "locator": "Repository artifact tools/skolem_one_sided_modular_replay.py at SHA-256 8fc41d2e82f44134de9af20adfba5a602593237fea1110da156adcb951f5760f; exact replay executed 2026-07-28"
    },
    "dependencies": [
      {
        "name": "CPython standard library",
        "version": "3.12.13",
        "license": "Python-2.0"
      }
    ],
    "outputs": {
      "format": "one canonical compact JSON object followed by LF",
      "source_bytes": 9953,
      "source_line_count": 290,
      "source_sha256": "8fc41d2e82f44134de9af20adfba5a602593237fea1110da156adcb951f5760f",
      "stdout_bytes": 3908,
      "stdout_sha256": "500af5d3f25cce870dd7747a24d2c0bf0dae614d4b98b61c64e4b7d9749ef96e",
      "expected": {
        "order_two_rows": 2401,
        "integer_zero_witness_rows": 841,
        "modular_nonzero_certificate_rows": 1508,
        "inconclusive_rows": 52,
        "boundary_rows": 40,
        "census_rows_sha256": "c8f561051d0eddcda8302ffc5fa47ba26e591b2181d320614e7fceed091966cf",
        "inconclusive_rows_sha256": "5b5e86706dfea20071c9f85d26478063162b9ccc98d2a61e4b3b95808c4cf83a",
        "boundary_rows_sha256": "d42519fead89173023ae438d88ba916734be3004356c76f2df524a4adb5a6c1d",
        "fibonacci_modulus_rows": 511,
        "fibonacci_rows_sha256": "6eb196a28c2cac0d194ce1af150c99bdc5e64591ef0c163d3c4d79f43a76d082"
      }
    },
    "runtime_seconds": 0.18
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Repository artifact tools/skolem_one_sided_modular_replay.py at SHA-256 8fc41d2e82f44134de9af20adfba5a602593237fea1110da156adcb951f5760f; exact replay executed 2026-07-28"
  },
  "models": [],
  "relations": [
    {
      "slug": "R733",
      "title": "A negative zero defeats one-sided modular exclusion for reversible recurrences",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R729",
      "title": "A fixed-modulus exclusion sieve fails as a complete one-sided method",
      "object_type": "attempt",
      "relation": "uses",
      "direction": "incoming"
    },
    {
      "slug": "R730",
      "title": "Formalize the reversible one-sided boundary lemma",
      "object_type": "attempt",
      "relation": "uses",
      "direction": "incoming"
    },
    {
      "slug": "skolem-problem-decidability",
      "title": "skolem problem decidability",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}