Emergence IS the Needle Killer

A needle is a persistent obstruction: a direction in which a declared budget is violated, typically because the available measurements cannot see or explain the response there. We give a linear-algebraic account of when a richer family of measurements removes such an obstruction. Measurements are linear maps on a finite-dimensional real or complex space carrying a positive semidefinite energy, and vanish on vectors of zero energy. The currency of a family is the positive operator whose quadratic form is its largest squared response at energy at most one. The first main theorem bounds the currency of a target family, after transport to a common space, by three separately proved estimates: one for the native measurements, one for the part of the target they cannot explain (the adequacy residual), and a transport estimate. The second main theorem works in a complete real Hilbert space of any dimension. Objects in a measure space carry an involution and a readout intertwining it with a linear isometric involution of the response space; suppose the sign-changing part of the readout is almost everywhere strongly measurable, square integrable, and vanishes exactly on the fixed locus. If its Gram operator is dominated by positive finite-trace budgets whose traces tend to zero, then almost every object lies on the fixed locus; such budgets exist exactly when the Gram operator is zero. We then construct parts of these hypotheses: a Schur formula for minimum energy with its exact legality conditions; exhaustion by increasing Hilbert windows with explicitly paid cross terms; forward transfer along supported isometric bridges (compatible with the probes, retaining their supports, with a null-legal and faithfully read native family), with errors tracked through chains; and, for a finite real dictionary of m measurements satisfying a lower frame bound on the initially hidden directions, a greedy selection that reduces the residual trace at a geometric rate and removes the residual exactly within min(m,d) steps, where d is the dimension of the hidden space. Every numbered theorem, lemma, proposition and corollary is formalized in Lean 4 with Mathlib, in the setting stated for it; the worked examples are not.