Warrant Containment in Dependency Graphs

A conclusion rests on grounds; when a ground is withdrawn, some conclusions stop standing. This note reports a small instrument that computes which — a three-valued calculus machine-checked in Lean 4 on an empty axiom list, with a ledger over it — and spends most of its length on measurements of when its answer is worth having. The useful results are negative. Redundancy contains a randomly located loss and does nothing against a chosen one. Declared redundancy resting on a shared origin reports a safety it does not provide. An incomplete dependency map errs in a direction set by the kind of missing edge, flattering in one case and frightening in the other. Anchored on a real dependency graph rather than a generated one, there is no containment at all. Twelve predictions made in the course of the work were refuted by its own runs — one of those refutations was itself refuted — and all are reported. Every figure is printed by a program in a public repository.