Elementary cores, abundant reactions, and the union-closed boundary of autocatalytic reaction systems

A reflexively autocatalytic and food-generated set (RAF) of a catalytic reaction system is a collection of reactions that can be built up from a food set and in which every reaction is catalysed from within. The RAFs of a finite system, with the empty set adjoined, form a union-closed family, and Steel asked whether some reaction always lies in at least half of its members: a RAF form of Frankl’s union-closed sets conjecture. We prove this for every system that contains a viable elementary core, a nonempty RAF all of whose reactants are food, with no restriction on the remaining reactions or on catalytic feedback into the core. The proof conditions on the reactions selected outside the core, recomputes the core’s support relation in that context, and applies the Horn-function counting injection of Lozin and Zamaraev to the resulting support relation under an upward constraint. The occupancy inequality holds separately in every exterior context, survives arbitrary nonnegative weights on contexts, and implies that every catalytic cycle of food-ready reactions meets a globally abundant reaction, that vertex-disjoint cycles yield distinct abundant reactions, and that systems with at most two non-food-ready reactions satisfy the half-frequency bound. Sharpness and a changing-witness example are given, together with exact projection diagnostics for an embedded module. We then locate the boundary of the method. RAF interior operators on a fixed reaction set are characterised as accessible union-closed food feasibility intersected with predecessor support; food-generation families are exactly antimatroids. A producer–gate construction with two reactions per coordinate realises every finite union-closed family containing the empty set, preserving frequencies and all availability queries with one food molecule, one catalyst per reaction, and molecular closure stabilising after two rounds. Its elementary RAFs correspond exactly to the singleton members of the encoded family. Hence a half-frequency theorem for systems without an elementary core is equivalent to the unrestricted union-closed conjecture, which remains open. The main theorems are verified in Lean 4 against Mathlib; the correspondence between the article and the formal development is recorded in an appendix.