| paper | d4-journals-mss-2021-0030 |
| authors | — |
| venue | ? |
| filed under | unclassified |
| judged by | gpt-6-luna / xhigh (triple__luna__xhigh__c6r1) |
| judge confidence | high |
| authors would recognise it | yes |
Theorem 4.8 identifies the SEC allocation as the unique maximizer of a weighted welfare problem, but provides no algorithm, complexity bound, or computational use of that formulation. The proposed mass model is recognizable, and the CARA schedule is computable, but that computation comes from the mirror construction rather than a computational result asserted by the paper.
fails bit a — no named computational result to mirror
Theorem 4.8 gives an optimization characterization, not a computational result; the paper does not use the formulation as a method for computing allocations.
fatal: True
The proposed schedule reflects Theorem 4.8’s weighted-utilitarian characterization; it leaves Theorem 4.2’s uniqueness result, Theorem 6.5’s rationalizability criterion, and the other axiomatic results untouched.
This paper has no named theorem classifying a problem as polynomial-time, NP-hard, FPT, or otherwise. The closest useful anchor is Theorem 4.8, proved in the paper (Appendix A.3). It says that for every regular ex-ante estate-division problem with homogeneous beliefs, and every estate value \(E\), there is a unique allocation maximizing
\[
\sum_{i\in N}\frac{u_i(x_i)}{u_i'(c_i)}
\quad\text{subject to}\quad
\sum_{i\in N}x_i=E,\qquad x_i\ge 0,
\]
and that this allocation is the one given by the paper’s strongly efficient and compliant rule, the SEC rule. This is an optimization characterization of the underlying allocation problem, not a complexity result; I would not attribute a polynomial-time theorem to the authors.
A natural high-multiplicity setting is a large pool of creditors holding standardized claims. Many creditors share a contract and claim size, and perhaps a common preference class. Let \(T\) be the \(\tau\) claimant types, with mass \(\mu_t>0\), \(\sum_t\mu_t=1\). Type \(t\) has per-person claim \(c_t>0\) and utility \(u_t(x)=-e^{-r_tx}\), where \(r_t>0\). Suppose the estate is uncertain ex ante, with a common uniform belief over \([0,C]\), where \(C=\sum_t\mu_tc_t\) is the average total claim per claimant. If the pool has \(n\) creditors, its type-\(t\) count is about \(n\mu_t\), while \(\tau\) can stay small as \(n\) grows.
The continuous question I would hand to a prover is CARA Type-Support SEC Schedule:
Given binary-rational \((\mu_t,c_t,r_t)_{t\in T}\), output the per-person award schedule \(x_t:[0,C]\to\mathbb R_{\ge0}\) for every type. The schedules must satisfy \(\sum_t\mu_tx_t(E)=E\) for every \(E\in[0,C]\), and \(x_t(C)=c_t\). They must maximize
\[ > \int_0^C\sum_{t\in T}\mu_t\frac{u_t(x_t(E))}{u_t'(c_t)}\,\frac{dE}{C} > \]
over feasible schedules.
The solution is the unique SEC schedule characterized by Theorem 4.8. In particular, set \(\theta_t=r_tc_t\); for each \(E\), find the unique \(q(E)\in[0,\max_t\theta_t]\) satisfying
\[
\sum_t\mu_t\max\!\left(0,c_t-\frac{q(E)}{r_t}\right)=E.
\]
Then \(x_t(E)=\max(0,c_t-q(E)/r_t)\). This gives a concrete output representation: sort the rational thresholds \(\theta_t\), and report the resulting piecewise-affine schedules. There are at most \(\tau\) type drop-out thresholds. On each segment the active set \(A\) is fixed and
\[
q(E)=\frac{\sum_{t\in A}\mu_tc_t-E}{\sum_{t\in A}\mu_t/r_t}.
\]
Thus this restricted mirror is exactly solvable in polynomial time in \(\tau\) and the input bit length by rational arithmetic. That tractability claim is for the stated CARA family; Theorem 4.8 itself does not give a bit-complexity bound for arbitrary utility functions.
This seems recognizable as the authors’ problem: the decision is still an ex-ante estate-division rule, the claim and preference information remains part of claimant type, and the objective and compliance condition are unchanged. The continuization is the claimant population: \(\mu_t\) is a share of creditors, and \(x_t(E)\) is the award per claimant of that type. A discrete pool with \(n_t\) creditors of each type maps to \(\mu_t=n_t/n\), with total estate \(nE\); the continuous schedule gives the same per-person rule. Fractional awards are inherent in dividing a homogeneous divisible estate, while the new modeling move is representing the population by masses.
The mirror covers Theorem 4.8’s allocation characterization only. Its weakest point is that this is not a paper-backed complexity breakthrough: the finite problem is already a separable allocation problem, and grouping repeated types compresses it. The continuous formulation is a sensible high-multiplicity version, but it does not show discrete hardness dissolving. A natural next question is whether exact or approximation complexity remains tractable for general regular utilities under a precise rational input representation.
Theorem 4.8 is the proponent’s strongest anchor, but it does not establish a computational result. It characterizes the allocation for a finite set of claimants as the maximizer of a separable, strictly concave objective subject to one resource constraint. The KKT conditions give the allocation directly through normalized marginal utilities. The paper asks whether its efficiency and compliance principles determine a rule, and how that rule can be rationalized; it does not ask how hard it is to compute one. Turning that characterization into a complexity problem would add a new agenda rather than mirror a computational result in the paper.
There is a credible high-multiplicity scenario: many creditors may share the same claim and preference parameters. That makes type masses a sensible representation, and I would not object to the mirror on the ground that creditors are inherently individual. But with \(\tau\) such types, the SEC allocation at each estate value \(E\) still has the form
\[
x_t(E)=(u_t')^{-1}\!\left(\lambda(E)u_t'(c_t)\right),
\qquad
\sum_{t=1}^{\tau}\mu_t x_t(E)=E,
\]
with the usual zero-award condition when the marginal utility threshold is reached. The type masses cancel from each type’s marginal condition; they appear only in the single balance equation determining \(\lambda(E)\). So the continuous population creates no new interaction or combinatorial structure. It repackages repeated claimants into a separable resource-allocation problem with one scalar to find.
The proponent’s CARA example makes this limitation especially clear. Its schedule has at most \(\tau\) breakpoints and is computed by sorting thresholds and evaluating rational affine formulas. For broader utility classes, a computational question needs a finite representation of each utility function. The paper assumes arbitrary regular functions, not a particular encoding. If the functions are supplied through a suitable explicit representation or evaluation oracle, the central task is a monotone scalar search using inverse marginal utilities. If a chosen encoding makes that task hard, the source of difficulty may be the encoding or function evaluation; the paper gives no reason to treat it as a population-complexity phenomenon. Either way, the mirror does not expose the kind of algorithmic landscape the programme is built to chart.
A stronger rescue might target Theorem 4.2’s uniqueness result or Theorem 6.5’s rationalizability criterion instead. Those are also mathematical characterizations, not computational claims. In particular, Theorem 6.5 asks for a differential condition over a parametric function. Making that a finite-input decision problem would require choosing a representation and restricting the function class; changing the population from named agents to type masses does not supply either choice.
Thus, the high-multiplicity regime is plausible, and the proponent has described a valid population-aggregated version of the SEC rule. The negative case is about whether it is a worthwhile *ChoCo mirror*: the most faithful computational formulation is a standard separable allocation calculation, while richer complexity questions require extra representational assumptions not motivated by the paper. I cannot rule out an application-specific reason to build a solver, but that would be a new optimization project, not a computational result this paper invites the programme to classify.
The adversarial triple: the proponent anchors on up to three named results; the opponent sees that case and must defeat every anchor; the judge decides which case convinced it. These are the pipeline’s own outputs, generated by tools/triple_run.py — no human edited them. The paper’s own text is not reproduced here beyond the quoted statement above.