{
  "id": "oai:papers.qnfo.org:deductive-verification-of-discrete-time-quantum-walk-simulators-contracts-cost-b",
  "slug": "deductive-verification-of-discrete-time-quantum-walk-simulators-contracts-cost-b",
  "title": "Deductive Verification of Discrete‑Time Quantum‑Walk Simulators: Contracts, Cost Bounds, and Extensions to Graph‑Generalized and Open‑System Walks",
  "authors": [
    "Rowan Brad Quni-Gudzinas"
  ],
  "abstract": "Discrete‑time quantum walks are a universal model of quantum computation, a platform for topological phases, and a testbed for quantum algorithms, yet the simulators used to study them are rarely checked with the rigor applied to classical library code. This paper frames quantum‑walk simulator verification as a contract‑checking problem in the style of deductive verification of unmodified library functions. We define eight contracts—unitarity, probability (or trace) conservation, exact support bounds, integer‑valued topological invariants, periodicity, graph‑support closure, statistical‑limit, and trace‑conservation for open‑system evolutions—and derive their computational costs with explicit arithmetic. For a Hadamard walk evolved t=10³ steps, the state‑vector dimension is d₁000=4002; a dense unitarity check costs d_t³=64 096 048 008 multiply‑add operations, while a sparse check exploiting two non‑zeros per column costs 4d_t²=64 064 016, a speedup factor of d_t/4=1000.5. A graph‑generalized staggered walk on N=100 vertices with maximum degree Δ=3 yields a sparse‑over‑dense speedup of N/k≈33.33. The verification overhead for probability (or trace) conservation is a constant 50\\% of the simulation multiplication count per step, independent of t. We project a double‑precision drift bound of 8.88×10^-10 after 10⁶ steps and a block‑diagonalization cost of $432$ multiply‑adds for the 3‑cycle periodicity contract. All quantitative results are either computed with shown arithmetic or explicitly labeled projections. The framework supplies quantum‑algorithm developers, simulator library maintainers, and hardware‑control engineers with a decision procedure for selecting and costing verification checks, and it identifies concrete falsification conditions.",
  "abstract_markdown": "Discrete‑time quantum walks are a universal model of quantum computation, a platform for topological phases, and a testbed for quantum algorithms, yet the simulators used to study them are rarely checked with the rigor applied to classical library code. This paper frames quantum‑walk simulator verification as a contract‑checking problem in the style of deductive verification of unmodified library functions. We define eight contracts—unitarity, probability (or trace) conservation, exact support bounds, integer‑valued topological invariants, periodicity, graph‑support closure, statistical‑limit, and trace‑conservation for open‑system evolutions—and derive their computational costs with explicit arithmetic. For a Hadamard walk evolved $t=10^{3}$ steps, the state‑vector dimension is $d_{1000}=4002$; a dense unitarity check costs $d_t^{3}=64\\,096\\,048\\,008$ multiply‑add operations, while a sparse check exploiting two non‑zeros per column costs $4d_t^{2}=64\\,064\\,016$, a speedup factor of $d_t/4=1000.5$. A graph‑generalized staggered walk on $N=100$ vertices with maximum degree $\\Delta=3$ yields a sparse‑over‑dense speedup of $N/k\\approx33.33$. The verification overhead for probability (or trace) conservation is a constant $50\\%$ of the simulation multiplication count per step, independent of $t$. We project a double‑precision drift bound of $8.88\\times10^{-10}$ after $10^{6}$ steps and a block‑diagonalization cost of $432$ multiply‑adds for the 3‑cycle periodicity contract. All quantitative results are either computed with shown arithmetic or explicitly labeled projections. The framework supplies quantum‑algorithm developers, simulator library maintainers, and hardware‑control engineers with a decision procedure for selecting and costing verification checks, and it identifies concrete falsification conditions.",
  "date": "2026-10-11",
  "first_published": "2026-10-11",
  "last_revised": "2026-10-19T11:41:07Z",
  "modified": "2026-10-19T11:41:07Z",
  "version": "2.0.1",
  "version_count": 2,
  "language": "en",
  "keywords": [],
  "quality_tags": [
    "High-quality scholarly research",
    "open-access scholarly work",
    "versioned research publication"
  ],
  "quality_label": "High-quality scholarly research",
  "quality_basis": "QNFO publisher classification for open-access, versioned research with a public revision history and reader correction channel; this is not a claim of independent peer review.",
  "quality_evidence_url": "https://qnfo.org/about",
  "peer_review_status": "Not independently peer-reviewed",
  "resource_type": "ScholarlyArticle",
  "doi": null,
  "doi_url": null,
  "url": "https://papers.qnfo.org/papers/deductive-verification-of-discrete-time-quantum-walk-simulators-contracts-cost-b",
  "license_url": "https://legal.qnfo.org/",
  "license_spdx": null,
  "sha256": "5aaccc8033576b3455e42f90d3ca602d439a879c572e6a9da0ec5f32a75162ab",
  "version_url": "https://papers.qnfo.org/papers/deductive-verification-of-discrete-time-quantum-walk-simulators-contracts-cost-b/v/2.0.1",
  "datacite": {
    "schemaVersion": "http://datacite.org/schema/kernel-4",
    "identifiers": [
      {
        "identifier": "https://papers.qnfo.org/papers/deductive-verification-of-discrete-time-quantum-walk-simulators-contracts-cost-b",
        "identifierType": "URL"
      }
    ],
    "creators": [
      {
        "name": "Rowan Brad Quni-Gudzinas",
        "nameType": "Personal",
        "nameIdentifiers": [
          {
            "nameIdentifier": "https://orcid.org/0009-0002-4317-5604",
            "nameIdentifierScheme": "ORCID",
            "schemeUri": "https://orcid.org"
          }
        ]
      }
    ],
    "titles": [
      {
        "title": "Deductive Verification of Discrete‑Time Quantum‑Walk Simulators: Contracts, Cost Bounds, and Extensions to Graph‑Generalized and Open‑System Walks"
      }
    ],
    "publisher": "QNFO",
    "publicationYear": "2026",
    "resourceType": {
      "resourceTypeGeneral": "Text",
      "resourceType": "ScholarlyArticle"
    },
    "subjects": [
      {
        "subject": "High-quality scholarly research",
        "subjectScheme": "QNFO publisher classification",
        "schemeUri": "https://qnfo.org/about"
      },
      {
        "subject": "open-access scholarly work",
        "subjectScheme": "QNFO publisher classification",
        "schemeUri": "https://qnfo.org/about"
      },
      {
        "subject": "versioned research publication",
        "subjectScheme": "QNFO publisher classification",
        "schemeUri": "https://qnfo.org/about"
      }
    ],
    "dates": [
      {
        "date": "2026-10-11",
        "dateType": "Issued"
      },
      {
        "date": "2026-10-19",
        "dateType": "Updated"
      }
    ],
    "language": "en",
    "version": "2.0.1",
    "rightsList": [
      {
        "rightsUri": "https://legal.qnfo.org/"
      }
    ],
    "descriptions": [
      {
        "description": "Discrete‑time quantum walks are a universal model of quantum computation, a platform for topological phases, and a testbed for quantum algorithms, yet the simulators used to study them are rarely checked with the rigor applied to classical library code. This paper frames quantum‑walk simulator verification as a contract‑checking problem in the style of deductive verification of unmodified library functions. We define eight contracts—unitarity, probability (or trace) conservation, exact support bounds, integer‑valued topological invariants, periodicity, graph‑support closure, statistical‑limit, and trace‑conservation for open‑system evolutions—and derive their computational costs with explicit arithmetic. For a Hadamard walk evolved t=10³ steps, the state‑vector dimension is d₁000=4002; a dense unitarity check costs d_t³=64 096 048 008 multiply‑add operations, while a sparse check exploiting two non‑zeros per column costs 4d_t²=64 064 016, a speedup factor of d_t/4=1000.5. A graph‑generalized staggered walk on N=100 vertices with maximum degree Δ=3 yields a sparse‑over‑dense speedup of N/k≈33.33. The verification overhead for probability (or trace) conservation is a constant 50\\% of the simulation multiplication count per step, independent of t. We project a double‑precision drift bound of 8.88×10^-10 after 10⁶ steps and a block‑diagonalization cost of $432$ multiply‑adds for the 3‑cycle periodicity contract. All quantitative results are either computed with shown arithmetic or explicitly labeled projections. The framework supplies quantum‑algorithm developers, simulator library maintainers, and hardware‑control engineers with a decision procedure for selecting and costing verification checks, and it identifies concrete falsification conditions.",
        "descriptionType": "Abstract"
      },
      {
        "description": "Publisher quality classification: High-quality scholarly research. QNFO publisher classification for open-access, versioned research with a public revision history and reader correction channel; this is not a claim of independent peer review.",
        "descriptionType": "Other"
      },
      {
        "description": "Peer review status: Not independently peer-reviewed",
        "descriptionType": "Other"
      }
    ],
    "formats": [
      "text/html"
    ]
  }
}