A very strong proportionality criterion

During the first round of the STARPR committee I proposed a criterion for proportionality called the Independent Aggregated Hare Criterion. It states that:
"If for some set of candidates S with at least k members, there is a subset of ballots for which the sum of each ballot's lowest score given to a candidate in S\W (where W is the set of all elected candidates) exceeds the sum of each ballot's highest score given to a candidate in W\S by at least (k)(MAX)(Quota) points on some set of ballots, then at least k members of S must be elected."(Such a winner set can be proven to exist in the approval case by induction. In the singlewinner case it can be passed by always taking unanimously approved candidate if one exists. In cases with k>1 winners, the criterion can be passed by taking a Hare quota of ballots that all approve a single candidate and electing that candidate, then electing a winner set containing k1 winners that passes this criterion on all ballots outside the selected quota. I'd supply details but it would make this post run much longer. The proof can be extended to the score case by applying the KPtransformation.)
The idea behind the IAHC is basically that party PR should still be passed even in cases of partial disagreement, specifically, if some members of the party approve some losing candidates outside the party or if some members fail to approve some winning candidates from the party. It seems to have some things in common with Justified Representation; it implies JR and PJR but not EJR (1 ABC, 1 ABD; CD), nor does EJR imply it (1 ABCD, 1 ABD, 1 ACD, 1 BCD; ABCX).
A much stricter version of this criterion is: for disjoint ballot sets B_1, ..., B_m, candidate sets S_1, ..., S_m (not necessarily disjoint), if for each i, the Independent Aggregated Hare Criterion would require that at least k candidates would be elected from S_i by taking B_i as the subset of ballots, and ∩S_i ≥ mk, then at least mk candidates from ∩S_i must be elected.
(The idea is that if a party can be divided into factions and subfactions, then the consensus candidates must be elected before the factional candidates. It could be called the Consensus Independent Aggregated Hare Criterion. This is a greater demand than it may first appear.)
For example, with ballots
1: AB
0.5: ABC
0.5: ABD
1: C
1: D
(Where the number of ballots is given in Hare quotas, and there may be other ballots.)
A, B, C, and D are all required to be elected. C and D are required by standard party PR. Since C,D are guaranteed to be in W, we can take S_1 = {A,B} and B_1 = {1 AB}; S_2 = {A,B,C,D} and B_2 = {0.5 ABC, 0.5 ABD}. The IAHC requires 1 candidate from S_1 and S_2 be elected based on ballot sets B_1, B_2 respectively. ∩S_i={A,B}, k=1, and m=2, so 2 of {A,B} must be elected.The proof of possibility for the IAHC will not work for this criterion but I think there is a way to adapt it to make it work.
Edit: the first version I posted of this did not work because you can take an empty B_i and then the S_i that goes with it can be completely arbitrary. By forcing all of the (B_i, S_i) to meet the same required k, hopefully this should no longer be possible.

@marylander We will start the 2nd round soonish. We are just gathering people. Are you interested in participating again? I have also invited Piotr Skowron who invented/coinvented FJR, RuleX and MES. This would be a great topic to discuss

@keithedmonds Yes, I anticipate that I should be back for the committee. I was going to post something in the loomio thread but I think that a lot of the goals that I was thinking of had already been said (and I don't think I need to try to come up with a whole lot of others since the goals other people stated seem like plenty to do already.)