It seems like the lift in the open-source models is being used as a proxy metric, and the core goal is a human understandable yoga [1] for approaching these kinds of equational proofs in universal algebra.

[1] https://mathoverflow.net/questions/64071/what-does-the-term-...