fix(verifier): split a witness's origin step from its detection step

A deferred obligation spans two steps: the one that armed it and the one whose
reduction failed. They were conflated under one index, so the extractor snapshot
(which is the detecting step's state) was reported against the origin step.

Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J

internal/verifier/worker.go

@@ -476,21 +476,27 @@ func (v *Verifier) EvaluateProperties() map[string]ltl.Verdict {
 }
 
 // Witness is the verifier-level record of a property violation: the LTL reason
-// (a predicate's thrown-error text, "predicate false", or a liveness failure),
+// (a predicate's thrown-error text, "predicate false", or a liveness failure)
-// the step it fired at, and a snapshot of every extractor's current value at
+// and the two step indices a deferred obligation spans.
-// that step. The snapshot lets a reader see the state that produced the
+//
-// violation without replaying the run.
+// Step is the origin: the step whose observation armed the obligation that
+// failed. DetectedStep is the observation whose reduction produced the
+// violation, which for a next or an eventually is later. Extractors is that
+// observation's state, so it belongs to DetectedStep and not to Step; the two
+// were previously conflated under one index.
 type Witness struct {
 	Property     string
 	Reason       string
 	Step         int
+	DetectedStep int
 	IsError      bool
 	Extractors   map[string]json.RawMessage
 }
 
 // captureWitness records the witness for a property that just transitioned to
 // violated, snapshotting the current extractor values so the cause is visible
-// after the run.
+// after the run. The snapshot is the state of the observation being reduced,
+// which the witness records as its detection step.
 func (v *Verifier) captureWitness(name string) {
 	evaluator, ok := v.evaluators[name]
 	if !ok {
@@ -504,6 +510,7 @@ func (v *Verifier) captureWitness(name string) {
 		Property:     name,
 		Reason:       violation.Reason,
 		Step:         violation.Step,
+		DetectedStep: v.stepIndex,
 		IsError:      violation.IsError,
 		Extractors:   v.extractorSnapshot(),
 	}