Below is a sketch of an argument that might imply that the answer to Q5 is (clasically) ‘yes’. (I thought about a question that’s probably the same a little while back, and am reciting from cache, without checking in detail that my axioms lined up with your A1-4).
Pick a lottery Z with the property that forall A,B with A⪯Z and B⪯Z, forall p∈[0,1], we have (1−p)A+pB⪯Z. We will say that Z is “extreme(ly high)”.
Pick a lottery X with X⪯Z.
Now, for any Y with X⪯Y⪯Z, define u(Y) to be the p guaranteed by continuity (A3).
Lemma: forall α,β∈[0,1] with α≤β, (1−α)X+αZ⪯(1−β)X+βZ.
Proof:
(1−α)X+αZ⪯Z, by X⪯Z and Z⪯Z and the extremeness of Z.
(1−α)X+αZ⪯1−α1−β((1−α)X+αZ)+(1−1−α1−β)Z, by A4.
(1−α)X+αZ⪯(1−β)X+βZ, by some reduction.
We can use this lemma to get that u(A)≤u(B) implies A⪯B, because A∼(1−u(A))X+u(A)Z, and B∼(1−u(B))X+u(B)Z, so invoke the above lemma with α=u(A) and β=u(B).
Next we want to show that A⪯B implies u(A)≤u(B). I think this probably works, but it appears to require either the axiom of choice (!) or a strengthening of one of A3 or A4. (Either strengthen A3 to guarantee that if B1∼B2 then it gives the same p in both cases, or strengthen A4 to add that if B≺A then B≺pA+(1−p)B, or define u(A) not from A3 directly, but by using choice to pick out a p for each ∼-equivalence-class of lotteries.) Once you’ve picked one of those branches, the proof basically proceeds by contradiction. (And so it’s not terribly constructive, unless you can do ¬¬(A≺B)→(A≺B) constructively.)
The rough idea is: if A≺B but u(A)≥u(B) then you can use the above lemma to get a contradiction, and so you basically only need to consider the case where A∼B in which case you want u(A)=u(B), which you can get by definition (if you use the axiom of choice), or directly by the strengthening of A3. And… my cache says that you can also get it by the strengthening of A4, albeit less directly, but I haven’t reloaded that part of my cache, so \shrug I dunno.
Next we argue that this function u is unique up to postcomposition by… any strictly isotone endofunction on the reals? I think? (Perhaps unique only among quasiconvex functions?) I haven’t checked the details.
Now we have a class of utility-function-ish-things, defined only on Y with X⪯Y⪯Z, and we want to extend it to all lotteries.
I’m not sure if this step works, but the handwavy idea is that for any lottery Y that you want to extend u to include, you should be able to find a lower X and an extreme higher Z that bracket it, at which point you can find the corresponding u (using the above machinery), at which point you can (probably?) pick some canonical strictly-isotone real endofunction to compose with it that makes it agree with the parts of the function you’ve defined so far, and through this process you can extend your definition of u to include any lottery. handwave handwave.
Note that the exact function you get depends on how you find the lower X and higher Z, and which isotone function you use to get all the pieces to line up, but when you’re done you can probably argue that the whole result is unique up to postcomposition by a strictly isotone real endofunction, of which your construction is a fine representative.
This gets you C1. My cache says it should be easy to get C2 from there, and the first paragraph of “Edit 3” to the OP suggests the same, so I haven’t checked this again.
Below is a sketch of an argument that might imply that the answer to Q5 is (clasically) ‘yes’. (I thought about a question that’s probably the same a little while back, and am reciting from cache, without checking in detail that my axioms lined up with your A1-4).
Pick a lottery Z with the property that forall A,B with A⪯Z and B⪯Z, forall p∈[0,1], we have (1−p)A+pB⪯Z. We will say that Z is “extreme(ly high)”.
Pick a lottery X with X⪯Z.
Now, for any Y with X⪯Y⪯Z, define u(Y) to be the p guaranteed by continuity (A3).
Lemma: forall α,β∈[0,1] with α≤β, (1−α)X+αZ⪯(1−β)X+βZ.
Proof:
(1−α)X+αZ⪯Z, by X⪯Z and Z⪯Z and the extremeness of Z.
(1−α)X+αZ⪯1−α1−β((1−α)X+αZ)+(1−1−α1−β)Z, by A4.
(1−α)X+αZ⪯(1−β)X+βZ, by some reduction.
We can use this lemma to get that u(A)≤u(B) implies A⪯B, because A∼(1−u(A))X+u(A)Z, and B∼(1−u(B))X+u(B)Z, so invoke the above lemma with α=u(A) and β=u(B).
Next we want to show that A⪯B implies u(A)≤u(B). I think this probably works, but it appears to require either the axiom of choice (!) or a strengthening of one of A3 or A4. (Either strengthen A3 to guarantee that if B1∼B2 then it gives the same p in both cases, or strengthen A4 to add that if B≺A then B≺pA+(1−p)B, or define u(A) not from A3 directly, but by using choice to pick out a p for each ∼-equivalence-class of lotteries.) Once you’ve picked one of those branches, the proof basically proceeds by contradiction. (And so it’s not terribly constructive, unless you can do ¬¬(A≺B)→(A≺B) constructively.)
The rough idea is: if A≺B but u(A)≥u(B) then you can use the above lemma to get a contradiction, and so you basically only need to consider the case where A∼B in which case you want u(A)=u(B), which you can get by definition (if you use the axiom of choice), or directly by the strengthening of A3. And… my cache says that you can also get it by the strengthening of A4, albeit less directly, but I haven’t reloaded that part of my cache, so \shrug I dunno.
Next we argue that this function u is unique up to postcomposition by… any strictly isotone endofunction on the reals? I think? (Perhaps unique only among quasiconvex functions?) I haven’t checked the details.
Now we have a class of utility-function-ish-things, defined only on Y with X⪯Y⪯Z, and we want to extend it to all lotteries.
I’m not sure if this step works, but the handwavy idea is that for any lottery Y that you want to extend u to include, you should be able to find a lower X and an extreme higher Z that bracket it, at which point you can find the corresponding u (using the above machinery), at which point you can (probably?) pick some canonical strictly-isotone real endofunction to compose with it that makes it agree with the parts of the function you’ve defined so far, and through this process you can extend your definition of u to include any lottery. handwave handwave.
Note that the exact function you get depends on how you find the lower X and higher Z, and which isotone function you use to get all the pieces to line up, but when you’re done you can probably argue that the whole result is unique up to postcomposition by a strictly isotone real endofunction, of which your construction is a fine representative.
This gets you C1. My cache says it should be easy to get C2 from there, and the first paragraph of “Edit 3” to the OP suggests the same, so I haven’t checked this again.