# A shortest path through an intermediate node

KL-FCS-028 · Graph algorithms · version 1.0.0

## Problem

Find the minimum weighted directed path from vertex 0 to vertex 3.

## Context

A path is a feasible witness; the minimum-distance claim must also exclude shorter paths.

## Definitions

- **Directed edge**: An ordered pair of vertices with a nonnegative weight.
- **Simple path**: A path visiting no vertex twice.
- **Distance**: The sum of the weights along a path.

## Checked result

Minimum distance: 5.

The supplied sequence is a valid path. Every alternative simple path is scored, so equal-cost optima are accepted and longer alternatives are ruled out.

## Checker reasoning

1. Enumerate every simple source-to-target path in the small graph.
2. Compute the total weight of each path.
3. Find the minimum and accept any witness attaining it.
4. Check the witness edge sequence and objective.

## Dataset construction

{
  "family": "graphs",
  "task": "Find the minimum weighted directed path from vertex 0 to vertex 3.",
  "input_encoding": "Structured JSON; field meanings are stated in the specification.",
  "coverage": "Complete simple-path enumeration",
  "acceptance": [
    "Enumerate every simple source-to-target path in the small graph.",
    "Compute the total weight of each path.",
    "Find the minimum and accept any witness attaining it.",
    "Check the witness edge sequence and objective."
  ],
  "generation": "Deterministic finite fixture; full enumeration or witness replay as stated.",
  "split_policy": "Reference corpus for exposition and reproduction; no train/test evaluation split is claimed."
}

## Formal payload

```json
{
  "specification": {
    "vertices": 4,
    "edges": [
      [
        0,
        1,
        2
      ],
      [
        0,
        2,
        5
      ],
      [
        1,
        2,
        1
      ],
      [
        1,
        3,
        6
      ],
      [
        2,
        3,
        2
      ]
    ],
    "start": 0,
    "target": 3
  },
  "claim": {
    "minimum_distance": 5
  },
  "witness": {
    "path": [
      0,
      1,
      2,
      3
    ]
  }
}
```

## Complexity

Simple-path enumeration can be exponential; nonnegative weights ensure a shortest path can be chosen simple.

## Limits

Weights are nonnegative. Negative cycles and unreachable targets require distinct result types.

## Common error and further work

A locally cheapest outgoing edge need not belong to a globally shortest path.

Replace enumeration with distance-label certificates and add max-flow/min-cut records.

## Verification

Complete simple-path enumeration. 3 checker units.
Replay with `python3 tools/verify.py`. Mechanical status: checked; human review
has not yet been recorded. Custom Python verification, not a proof-assistant
claim. Checker 1.0.0 and exact source hashes are in `verification.json`.

## Provenance and references

Original Kenton Labs reference instance, authored with Codex assistance on 2026-10-11.
No external dataset or model-generation experiment. Reuse-license selection
remains pending.

- [Conceptual reference](https://networkx.org/documentation/stable/reference/algorithms/generated/networkx.algorithms.flow.minimum_cut.html)