Profitable Deviations towards Antagonistic Tie-Breaking

Abstract

Both players can gain by changing friendly to antagonistic tie-breaking.

Bhagat, Kulkarni, Larsson and Murali, “Tie-breaking in self interest cumulative subtraction games”, arXiv:2510.24280v2 (20 January 2026), Section 6, Problem 6 asks: “Is it true that no player can have a positive discrepancy by going from AvF or FvA to AvA?” The answer is no. The authors’ own sentence immediately before the problem reads “Experimental results point towards that this cannot happen if deviating towards AvA”; their experiments pointed the other way.

For subtraction set {7,12,13,38,50}, at heap 122 the AvF and AvA outcomes are (64,57) and (64,58), so Bob, the second player, gains by switching his own convention from friendly to antagonistic. At heap 172 the FvA and AvA outcomes are (107,64) and (108,64), so Alice, the opening player, gains by the same change. Problem 6 is a disjunction over AvF and FvA, and both disjuncts are refuted.

Nothing about Conjecture 4, the FvF-to-AvA statement, is established. There is no classification of such subtraction sets and no claim that these are the only or the smallest witnesses. The paper supplies the question and Definition 2; the declarations are repository constructions. Nat denotes the natural numbers, List(Nat) a finite list, and .1 and .2 are pair projections.

Definition 1.1 (Mover-relative conventions).

$C o n v e n t i o n = B oo l \times B oo l$

Formalization. D5/S0/Certificates/SelfInterestConventionDeviationGain.Convention (✓ std3).

Source. Repository-derived.

Commentary.

A Boolean records whether a player is antagonistic. Component 1 belongs to the mover, and component 2 belongs to the opponent.

Definition 1.2 (Friendly versus friendly).

$F v F = (f a l se, f a l se)$

Formalization. D5/S0/Certificates/SelfInterestConventionDeviationGain.FvF (✓ std3).

Source. Repository-derived.

Commentary.

Both players use friendly tie-breaking.

Definition 1.3 (Antagonistic versus friendly).

$A v F = (t r u e, f a l se)$

Formalization. D5/S0/Certificates/SelfInterestConventionDeviationGain.AvF (✓ std3).

Source. Repository-derived.

Commentary.

The mover is antagonistic and the opponent is friendly.

Definition 1.4 (Friendly versus antagonistic).

$F v A = (f a l se, t r u e)$

Formalization. D5/S0/Certificates/SelfInterestConventionDeviationGain.FvA (✓ std3).

Source. Repository-derived.

Commentary.

The mover is friendly and the opponent is antagonistic.

Definition 1.5 (Antagonistic versus antagonistic).

$A v A = (t r u e, t r u e)$

Formalization. D5/S0/Certificates/SelfInterestConventionDeviationGain.AvA (✓ std3).

Source. Repository-derived.

Commentary.

Both players use antagonistic tie-breaking.

Definition 1.6 (Role reversal at every move).

$\forall co n v e n t i o n : C o n v e n t i o n, dual (co n v e n t i o n) = ((co n v e n t i o n) .2, (co n v e n t i o n) .1)$

Formalization. D5/S0/Certificates/SelfInterestConventionDeviationGain.dual (✓ std3).

Source. Repository-derived.

Commentary.

Swap the two components at every move, including moves in mixed conventions.

Theorem 1.7 (Two role reversals restore the convention).

$\forall co n v e n t i o n : C o n v e n t i o n, dual (dual (co n v e n t i o n)) = co n v e n t i o n$

Proof. Machine-checked in Lean as D5/S0/Certificates/SelfInterestConventionDeviationGain.dual_involutive (✓ std3). ∎

Source. Repository-derived.

Commentary.

This holds for every convention without further hypotheses.

Theorem 1.8 (Exactly the homogeneous conventions are fixed).

$\forall co n v e n t i o n : C o n v e n t i o n, dual (co n v e n t i o n) = co n v e n t i o n ⟺ (co n v e n t i o n = F v F \lor co n v e n t i o n = A v A)$

Proof. Machine-checked in Lean as D5/S0/Certificates/SelfInterestConventionDeviationGain.dual_fixed_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

The equivalence covers all four Boolean pairs.

Definition 1.9 (Own total with a convention-dependent tie-break).

$\forall co n v e n t i o n : C o n v e n t i o n, \forall c h ose n, a lt er na t i v e : N a t \times N a t, Preferred (co n v e n t i o n, c h ose n, a lt er na t i v e) ⟺ (a lt er na t i v e) .1 \leq (c h ose n) .1 \land ((a lt er na t i v e) .1 = (c h ose n) .1 \Rightarrow i f (co n v e n t i o n) .1 t h e n (c h ose n) .2 \leq (a lt er na t i v e) .2 e l se (a lt er na t i v e) .2 \leq (c h ose n) .2)$

Formalization. D5/S0/Certificates/SelfInterestConventionDeviationGain.Preferred (✓ std3).

Source. Repository-derived.

Commentary.

Own total is primary. On equality, an antagonistic mover minimizes the opponent’s total and a friendly mover maximizes it. The Boolean conditional tests component 1 of the mover-relative convention.

Definition 1.10 (Tabulated mover and opponent totals).

$\forall s u b t r a c t i o n s : List (N a t), \forall co n v e n t i o n : C o n v e n t i o n, \forall h e a p : N a t, outcome (s u b t r a c t i o n s, co n v e n t i o n, h e a p) = readTable (tabulate (s u b t r a c t i o n s, h e a p + 1), h e a p, co n v e n t i o n)$

Formalization. D5/S0/Certificates/SelfInterestConventionDeviationGain.outcome (✓ std3).

Source. Repository-derived.

Commentary.

The result has type Nat times Nat: mover total followed by opponent total. readTable and tabulate are the module’s private implementation functions. Structural tabulation stores all four conventions at each heap; a terminal position returns (0,0). The recurrence theorem proves the Definition 2 semantics, rather than assuming faithfulness of the table.

Theorem 1.11 (Definition 2 holds for the tabulated outcome).

$\forall s u b t r a c t i o n s : List (N a t), \forall co n v e n t i o n : C o n v e n t i o n, \forall h e a p : N a t, ((\neg (\exists s t e p \in s u b t r a c t i o n s, 0 < s t e p \land s t e p \leq h e a p)) \Rightarrow outcome (s u b t r a c t i o n s, co n v e n t i o n, h e a p) = (0, 0)) \land ((\exists s t e p \in s u b t r a c t i o n s, 0 < s t e p \land s t e p \leq h e a p) \Rightarrow \exists s t e p \in s u b t r a c t i o n s, 0 < s t e p \land s t e p \leq h e a p \land outcome (s u b t r a c t i o n s, co n v e n t i o n, h e a p) = ((outcome (s u b t r a c t i o n s, dual (co n v e n t i o n), h e a p - s t e p)) .2 + s t e p, (outcome (s u b t r a c t i o n s, dual (co n v e n t i o n), h e a p - s t e p)) .1) \land \forall a lt er na t i v e \in s u b t r a c t i o n s, 0 < a lt er na t i v e \Rightarrow a lt er na t i v e \leq h e a p \Rightarrow Preferred (co n v e n t i o n, outcome (s u b t r a c t i o n s, co n v e n t i o n, h e a p), ((outcome (s u b t r a c t i o n s, dual (co n v e n t i o n), h e a p - a lt er na t i v e)) .2 + a lt er na t i v e, (outcome (s u b t r a c t i o n s, dual (co n v e n t i o n), h e a p - a lt er na t i v e)) .1)))$

Proof. Machine-checked in Lean as D5/S0/Certificates/SelfInterestConventionDeviationGain.outcome_recurrence (✓ std3). ∎

Source. Repository-derived.

Commentary.

Both implications hold for every finite subtraction list, convention and natural heap. With no positive legal step the payoff is zero. Otherwise a positive legal step realizes the payoff, after role reversal, and that payoff is Preferred over every positive legal alternative. Heap subtraction is natural-number subtraction. The existential membership, both step bounds, the realization equality and the universally quantified optimality clause are all part of the proved statement.

Definition 1.12 (The subtraction list).

$w i t n ess S u b t r a c t i o n s : List (N a t) = [7, 12, 13, 38, 50]$

Formalization. D5/S0/Certificates/SelfInterestConventionDeviationGain.witnessSubtractions (✓ std3).

Source. Repository-derived.

Commentary.

Both witnesses use this list, representing the subtraction set {7,12,13,38,50}. Only positive entries not exceeding the heap are legal. The general recurrence imposes no sorting or distinctness hypothesis.

Theorem 1.13 (Four exact outcome pairs).

$outcome (w i t n ess S u b t r a c t i o n s, A v F, 122) = (64, 57) \land outcome (w i t n ess S u b t r a c t i o n s, A v A, 122) = (64, 58) \land outcome (w i t n ess S u b t r a c t i o n s, F v A, 172) = (107, 64) \land outcome (w i t n ess S u b t r a c t i o n s, A v A, 172) = (108, 64)$

Proof. Machine-checked in Lean as D5/S0/Certificates/SelfInterestConventionDeviationGain.witness_values (✓ std3). ∎

Source. Repository-derived.

Commentary.

Lean verifies all four equalities together using decide +kernel. These are evaluations of the tabulation whose recurrence is proved, not assumed values or outputs trusted from an external search.

Definition 1.14 (Problem 6 as a proposition).

$n o P os i t i v eD i scre p an cy T o A v A ⟺ \forall s u b t r a c t i o n s : List (N a t), \forall h e a p : N a t, (outcome (s u b t r a c t i o n s, A v A, h e a p)) .2 \leq (outcome (s u b t r a c t i o n s, A v F, h e a p)) .2 \land (outcome (s u b t r a c t i o n s, A v A, h e a p)) .1 \leq (outcome (s u b t r a c t i o n s, F v A, h e a p)) .1$

Formalization. D5/S0/Certificates/SelfInterestConventionDeviationGain.noPositiveDiscrepancyToAvA (✓ std3).

Source. Repository-derived.

Commentary.

For every subtraction list and heap, Bob’s second component after AvF-to-AvA and Alice’s first component after FvA-to-AvA do not exceed their values before the respective changes. Both inequalities are required.

Theorem 1.15 (Typed refutation of Problem 6).

$\neg n o P os i t i v eD i scre p an cy T o A v A$

Proof. Machine-checked in Lean as D5/S0/Certificates/SelfInterestConventionDeviationGain.both_deviations_refute_no_positive_discrepancy (✓ std3). ∎

Source. Repository-derived.

Commentary.

This closed theorem negates the proposition without hypotheses. It uses both audited strict gains, for Bob at heap 122 and Alice at heap 172, to contradict the sum of the claimed upper bounds.

Theorem 1.16 (Both changes towards AvA are profitable).

$(outcome (w i t n ess S u b t r a c t i o n s, A v F, 122)) .2 < (outcome (w i t n ess S u b t r a c t i o n s, A v A, 122)) .2 \land (outcome (w i t n ess S u b t r a c t i o n s, F v A, 172)) .1 < (outcome (w i t n ess S u b t r a c t i o n s, A v A, 172)) .1$

Proof. Machine-checked in Lean as D5/S0/Certificates/SelfInterestConventionDeviationGain.both_deviations_profitable (✓ std3). ∎

Source. Repository-derived.

Commentary.

There are no hypotheses. Both strict inequalities are conclusions: Bob gains from 57 to 58 at heap 122, and Alice gains from 107 to 108 at heap 172. Each changes only their own friendly convention to antagonistic while the other player remains antagonistic.

References

Truth anchor: D5/S0/Certificates/SelfInterestConventionDeviationGain.AvA
Truth anchor: D5/S0/Certificates/SelfInterestConventionDeviationGain.AvF
Truth anchor: D5/S0/Certificates/SelfInterestConventionDeviationGain.Convention
Truth anchor: D5/S0/Certificates/SelfInterestConventionDeviationGain.FvA
Truth anchor: D5/S0/Certificates/SelfInterestConventionDeviationGain.FvF
Truth anchor: D5/S0/Certificates/SelfInterestConventionDeviationGain.Preferred
Truth anchor: D5/S0/Certificates/SelfInterestConventionDeviationGain.both_deviations_profitable
Truth anchor: D5/S0/Certificates/SelfInterestConventionDeviationGain.both_deviations_refute_no_positive_discrepancy
Truth anchor: D5/S0/Certificates/SelfInterestConventionDeviationGain.dual
Truth anchor: D5/S0/Certificates/SelfInterestConventionDeviationGain.dual_fixed_iff
Truth anchor: D5/S0/Certificates/SelfInterestConventionDeviationGain.dual_involutive
Truth anchor: D5/S0/Certificates/SelfInterestConventionDeviationGain.noPositiveDiscrepancyToAvA
Truth anchor: D5/S0/Certificates/SelfInterestConventionDeviationGain.outcome
Truth anchor: D5/S0/Certificates/SelfInterestConventionDeviationGain.outcome_recurrence
Truth anchor: D5/S0/Certificates/SelfInterestConventionDeviationGain.witnessSubtractions
Truth anchor: D5/S0/Certificates/SelfInterestConventionDeviationGain.witness_values

Keyboard shortcuts

trureturing — Discovering truth

Profitable Deviations towards Antagonistic Tie-Breaking

Abstract

References