Warrant Containment in Dependency Graphs

Abstract

A conclusion rests on grounds; when a ground is withdrawn, some conclusions stop standing. This note reports a small instrument that computes which — a two-valued calculus over marked inputs, 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 does nothing whatever against a chosen loss, and works against a random one only at levels no real system has: anchored on a real dependency graph rather than a generated one, a random loss costs 93% of the collective and there is no containment at all. 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. 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.