I have spotted an error in the statement (and proof) of Theorem 5, and then Corollary 6. The issue is that for any uncaused y we must have f(y) = y, so if there are several uncaused entities then they can't all have f(y) = g. The revised statements should go like this:

Theorem 5: Let x and y both have causes. Then f(x) = f(y) if and only if x and y are causally connected.

Proof: It is clear that if f(x) = f(y) then x is causally-connected to y (just build a path backwards from x to f(x) and then forward again to y). Conversely, suppose that x C y, then f(x) is uncaused and satisfies f(x) <= y so we have f(x) P f(y); since x is caused, there are f(x)=x1,...,xn=x such that each xi C xi+1 for i=1..n-1, then by A3 we have f(y) C x2 and hence f(y) <= x, which implies f(y) P f(x) and so by B1 f(x) = f(y). Next, suppose that for some uncaused z we have z C x and z C y; then z P f(x) which implies by A3 that f(x) C y and hence f(x) P f(y); similarly, f(y) P f(x) so by B1 f(x) = f(y). By an induction on the length of any other path connecting x to y, we have that f(x) = f(y).

Corollary 6: There is a single g in E such that: f(x) = g for every x in E with a cause, and every uncaused y P g.

Proof: Suppose there is at least one entity x with a cause, then set g = f(x). For any other caused entity y, f(y) = g by Theorem 5 and B5, and for an uncaused y, B5 implies y <= x, so that y P g. Lastly, if there are no caused entities, then B5 implies that E = {y} for some uncaused y, so we can just pick g = y.

I have also spotted a way of weakening or removing some of the premises (in particular A3, and B1 to B4). I will update with that later today.