The Shapley allocation of a graph energy game can leave its core

Gerardo Arizmendi and Octavio Arizmendi, The graph energy game, arXiv:2012.14114v2, Conjecture 3.10, page 8:

For the energy game, the Shapley value is in the core.

The source defines the energy of a finite simple undirected graph as the sum of absolute adjacency eigenvalues, with multiplicity. Its game has $w_G(S)=\mathcal E(G[S])$. For each vertex $i$ its allocation is

$$ \phi_i(w_G)=\sum_{S\subseteq V\setminus{i}} \frac{|S|!(|V|-|S|-1)!}{|V|!} \bigl(w_G(S\cup{i})-w_G(S)\bigr). $$

The core consists of all $x$ satisfying $\sum_{i\in S}x_i\ge w_G(S)$ for every coalition $S$ and $\sum_{i\in V}x_i=w_G(V)$. The conjecture quantifies over every finite simple graph, without connectedness, degree or bipartiteness assumptions. Preregistration #21951 binds this universal proposition and its expected refutation. The Library note records the versioned source and the literal defining formulas.

Statement echo

All local names below belong to D5.S3.Combinatorics.SpectralGraph.ArizmendiEnergyGameShapleyRefutation.

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | Finite simple undirected graph, every size | claim, n : Nat, G : SimpleGraph (Fin n) | Includes size zero; no extra graph hypothesis | | Energy of the induced coalition | worth | Reuses CyclicExtensionRefutation.graphEnergy with MatrixKind.adjacency, whose center is zero | | Every subset of the other players | shapley, powerset of univ.erase i | Includes empty and full predecessor sets | | Factorial coefficient and marginal contribution | shapley | Natural factorials and subtraction, followed by real coercions and real division | | Coalition payoff total | Finite sum in core | Inlined sum, with no duplicate payoff-total definition | | Every coalition inequality and efficiency | The two conjuncts of core | Singleton, empty and grand coalitions included | | Universal core membership | claim | Literal source conclusion | | Refutation | result | Negates the entire universal claim |

The explicit vertex labels $0,1$ in Fin 52 choose a counterexample; they add no hypothesis to the source claim. The private parameter $m\ge50$ restricts a sufficient counterexample family, not the quantified claim.

A scarce-side vertex of $K_{2,m}$ has a large average marginal contribution over predecessor coalitions. For $m\ge50$ this average exceeds its marginal contribution to the grand coalition. Efficiency then conflicts with the lower payoff bound of the coalition excluding that vertex.

The settlement is Refuted: result proves the negation of claim. All auxiliary theorems are private and used by the refutation. Their bind-only classification supplies no independent escape witness; the module's admission basis is open-problem-resolution (#21951; Refuted). No atom or cover is involved.

For a coalition with $r$ vertices on the two-vertex side and $k$ vertices on the other side, its energy is $2\sqrt{rk}$. The proof obtains this from the adjacency matrix identities $A^3=rkA$ and $\operatorname{tr}(A^2)=2rk$. The existing frozen declaration D5.S3.Arith.Lattices.Klartag.trace_mul_self_eq_sum_sq supplies the Hermitian trace-square identity used by energy_of_cubic.

Writing $q=\sqrt2$, $H=(m+1)(m+2)$, $S_1=\sum_{k=0}^m\sqrt k$ and $S_3=\sum_{k=0}^m k\sqrt k$, scarce_payoff gives

$$ \phi_a=\frac{2((m+q)S_1+(q-2)S_3)}{H}. $$

The private sum bounds give $S_1\ge\frac23m\sqrt m$ and $S_3\le\frac25m^2\sqrt m+m\sqrt m$. The sign $q-2<0$ requires the upper bound on $S_3$. scarce_formula_gap establishes $\phi_a>2(\sqrt2-1)\sqrt m$ for every $m\ge50$. family_not_core combines this inequality with the efficiency conjunct and the coalition inequality at $V\setminus{a}$ to derive a contradiction. result specializes to $m=50$.

The source claim would require both efficiency and every coalition inequality on $K_{2,50}$. The contradiction in family_not_core rules out that conjunction. No separately formalized universal efficiency theorem is asserted. An exact prior literature settlement would remove the novelty basis; the literature screen below is explicitly incomplete.

The Lean source and its full-statement Blueprint are D5 and Blueprint. The axiom closure of every public declaration is contained in ${\texttt{propext},\texttt{Classical.choice},\texttt{Quot.sound}}$. The public result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9). There are no other source-authored public theorems or published owners. Compiler-generated congruence companions are machine companion names under CLAUDE.md §3.9.

Experiment: exact checker at immutable commit 482b7177598d82c15ee82daca692752e471ee567. The committed check.py was extracted without modification and run as python3 /Users/auric/.sshx/327280fbd116be4105813297/attempt-1/experiment-check.py (exit 0, ALL_CHECKS_OK). Its SHA-256 is 5e2feaa724951623c0a3e8730b1a9727c71f70ab2d6f434869d5a9fdccc20125. The script uses exact integer, rational and symbolic arithmetic. It checks all eight coalition constraints of $P_3$; 30 characteristic polynomials for $0\le r\le4$, $0\le k\le5$; full subset Shapley formulas for $1\le m\le4$; factorial identities and normalization for $0\le m\le70$; positive deficit enclosures at $m=50,64,100$; and the actual adjacency matrix of $K_{2,50}$. Its symbolic leading-coefficient calculation is separate from a uniform Lean asymptotic theorem.

1. Proved in Lean: every $K_{2,m}$ with $m\ge50$ fails Shapley core membership. The scarce-side payoff exceeds $2(\sqrt2-1)\sqrt m$. Evidence: private scarce_formula_gap and family_not_core, consumed by public result.
2. Proved in Lean: for that same actual family graph, assumed core membership supplies its own efficiency equality and the inequality for $V\setminus{a}$; the scarce-side overshoot contradicts them. Evidence: the concluding contradiction in family_not_core.
3. Computed: $K_{2,50}$ is connected, has minimum degree 2, and has blocking deficit in the exact interval $[1380588425475056173/6630000000000000000, 1380588425475064157/6630000000000000000]$, whose lower endpoint is positive. Evidence: the pinned checker, command, exit code and SHA-256 in Evidence; these graph properties and this exact interval are not separately stated as Lean theorems.
4. Computed: $P_3$ retains Example 3.9's allocation, center first, $((2+2\sqrt2)/3,(2\sqrt2-1)/3,(2\sqrt2-1)/3)$, and passes all eight core constraints. Evidence: the same pinned checker and exact eight-coalition calculation in Evidence.
5. Open: no Lean theorem of unbounded absolute blocking deficit or its asymptotic limit is delivered. The checker computes the symbolic candidate coefficient $(26-18\sqrt2)/15$ and its positive sign; that calculation does not certify convergence in Lean.
6. Open: the optimal threshold in $m$ and classifications for all trees, regular graphs or balanced complete bipartite graphs remain unsettled by these results.
7. Proved in the published paper, not in this Lean module: the different vertex-energy allocation belongs to the core. Evidence: independently read arXiv v2, Theorem 3.5 (the induced-subgraph energy inequality) and Theorem 3.6 (core membership). The source labels 3.6 a theorem. This allocation is not the refuted Shapley allocation.

What the settlement shows

The proved mechanism is an imbalance between a scarce-side vertex's average marginal contribution and its grand-coalition marginal contribution. scarce_formula_gap and family_not_core show that connectedness and minimum degree 2 do not rescue the universal conjecture; the two graph properties of the concrete witness are computed as item 3. The sufficient bound $m\ge50$ is proved, without an optimality claim.

The nearest verified surviving example here is $P_3$, computed in item 4. The source's vertex-energy allocation theorem concerns a different allocation and survives this refutation. Proposition 3.11's marginal lower bound and Proposition 4.13's assertion that the 2-energy Shapley value equals degree are separate published statements; neither uses Conjecture 3.10 in its proof. They are literature readings, not new Lean results. No additional source conclusion is invalidated by this delivery.

Literature completeness is ASSUMED-UNVERIFIED. The preregistration's bounded screen found no exact settlement in the retrieved texts. It includes the versioned source, cited and same-author papers, broad bibliographic and arXiv searches, and MathOverflow/MathDB readings. The journal full text (HTTP 403), Rather–Ganie–Imran, Iñarra–Usategui, Vertex energy of some integral graphs, API limits and the partial broad full-text search leave explicit unchecked scope. The spectral reduction, Shapley formula and sum-comparison method are literature-attested ingredients. The family calculation and blocking conclusion are suspected-novel within that searched scope only.