Overlapping siphons, resident-dependent invasion, and uniform permanence in a two-strain coinfection reaction network

A siphon of a reaction network is a set of species whose simultaneous absence is preserved by the dynamics. When two siphons overlap, the invasion of a shared species cannot be counted as two independent modes, and the linearization at a disease-free state does not determine whether an absent strain can invade a population in which the other strain is already resident. We address both issues for finite mass-action networks and for a specific four-compartment, fourteen-reaction two-strain coinfection model with constant recruitment. The first result is structural: at any common boundary point of a family of siphons, first-order production can only decrease siphon membership, so the normal Jacobian is block triangular over membership signatures. For two siphons this yields the cross-multiplied characteristic identity $\chi_N\chi_{N_{S_1\cap S_2}}=\chi_{N_{S_1}}\chi_{N_{S_2}}$ on the fully covered normal space, valid as a polynomial identity and hence also at invasion thresholds. The second result is dynamical: for the coinfection model, if all fourteen rates are positive, both single-strain resident equilibria exist, and each missing two-dimensional block strictly invades the other resident, then every positive initial state has a unique global positive solution, and there is a lower bound $\varepsilon>0$, depending on the parameters but not on the initial state, that every compartment eventually exceeds. The converse holds away from the threshold: if one missing block is Hurwitz, that resident equilibrium attracts nearby positive states and permanence fails. The proof derives the resident limits from an exactly corrected relative entropy, lifts the flow to a compact space of normalized infection masses, obtains one common growth window on the extinction boundary by compactness, and recovers each compartment from a product floor. An explicit example shows that the entire disease-free Jacobian can remain unchanged while resident invasion changes sign. The structural theorem and the permanence theorem, including existence and uniqueness, have warning-free Lean 4 proofs in a frozen Mathlib environment.