Antimatroid characterization of RAF interior operators

Addressing the RAF-realizability question in Section 4 of Mike Steel's Interior Operators and Their Relationship to Autocatalytic Networks (arXiv:2305.16714v4, 2023), we characterize which interior operators on the subsets of a finite set E are maxRAF operators of catalytic reaction systems whose reaction set is exactly E. An interior operator is represented by its family of fixed sets, a union-closed family containing the empty set. A same-ground realization is a system with one reaction per element of E, finitely many molecule types, a food set and a catalysis relation; it realizes the empty set together with its RAFs, the nonempty reaction sets whose reactants arise from food by iterated closure under the selected reactions and whose reactions are each catalysed by a molecule of that closure. Such a family has a same-ground realization if and only if it is the intersection of an accessible union-closed family A and a predecessor-support family. Here A contains the empty set, is closed under unions, and every nonempty member of A has an element whose removal leaves a member of A; the members of A need not cover E. A set S is supported by a predecessor map P on E when every element e of S has some element of S in P(e), loops allowed. The family consisting of the empty set and all subsets of size at least three has a same-ground realization if and only if E has at most four elements. This gives the sharp threshold for the family considered in Proposition 5 and its subsequent remarks in Steel (2023). Both results are formalized in Lean 4 with Mathlib.