Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
Do you consider Metamath to meet the "present-day mathematics" criterion? I'm not sure whether you intend that to mean that you want a database of relationships between recent results, and if so what your cut-off for "recent" is.
Since I haven't had time to work on my partial answer, I'll throw open one idea in case it unblocks something for someone else: with the sum-product notation I used above ($+$ for the alternation of {W/B} etc. and $\cdot$ or simple concatenation to combine costs which must both be paid), we almost have a commutative idempotent semiring. We're just lacking an additive identity, which would have to be an unpayable cost and would be the greatest element in the partial order and a multiplicative annihilator. Might a tropical geometer have something useful to say?
An arguably simpler example than @Julian's, in the sense that it drops out of an attempted proof, is $BW(B+W) \ge (BB+WW)(B+W)$ but $BW \not\ge BB+WW$. Note the advantages of sum-product notation for seeing why.
I must be misunderstanding something, because the easiest example seems to be a counterexample. Consider $A_1=\{2/W\}$ and $B=\{W\}$. Then $A_1 < B$ with inequality. But the given algorithm would translate $A_1$ to $A_2 = \{1\}\{W\}$, and $B < A_2$, again with inequality.
In "Then, the question is, given two mana costs, how can we determine whether one is equal to another or not?", should it be "...less than or equal to..."? That seems to make more sense of the following paragraph. (PS You also conveniently omitted half-integral mana costs).
It can contain an odd cycle. Consider a poset which is fully characterised by two chains: $a < b < c$ and $a < d < e < c$. Then $(P, E_P)$ is a single cycle of length 5.
