Abundant reactions in autocatalytic networks with locally ranked supplier cores

A reflexively autocatalytic and food-generated set (RAF) of a catalytic reaction system is a set of reactions that can be built up from a food set and in which every reaction is catalysed from within. With the empty set adjoined, the RAFs of a finite system form a union-closed family, and Steel asked whether some reaction always lies in at least half of them. We prove this for every system containing a locally ranked complete-supplier core: a nonempty set $U$ of reactions in which each reaction has one internal supplier producing all of its non-food reactants and, unless food already catalyses it, a catalyst, and in which the internal substrate-production digraph is acyclic. Nothing is assumed outside $U$: the surrounding system may contain arbitrary substrate cycles, alternative producers and catalytic feedback into the core, and the core itself need not be elementary. The proof identifies each exterior fibre of the RAF family exactly, through food closure of the combined selected set, with a supported family under an upward constraint, and applies the dependency counting injection of Lozin and Zamaraev. The resulting occupancy inequality holds in every exterior context and with the empty set counted, and it yields exterior-weighted and bounded-distortion sampling statements with the sharp constant $1/(1+\kappa)$, deterministic and expected bounds for the number of RAFs destroyed by deleting one core reaction, transport of the certificate across exterior edits, and distinct abundant reactions from disjoint cores. Every elementary core is a locally ranked supplier core, so the theorem strictly extends the elementary-core abundance theorem; a three-reaction system separates it from any hypothesis on the global substrate digraph. A uniform three-chain family with no elementary RAF shows that the core average is sharp while individual core reactions can be arbitrarily rare, and that the RAF family need not be the support family of any digraph. The main theorem and the source-level consequences are verified in Lean 4 against Mathlib.