PaperlayerView exact revision on arXiv

Source-linked AI summary

Formalizing Cooperation and Competition: An AI-Assisted Mathematical Addendum to a 2018 Planning Thesis

Haitham Masaud Amar

arXiv:2610.29637v1cs.GTcs.AI

TL;DR

The paper addresses how claims linking strategic choice and cooperative stability depend on specified coalition opportunities and enforcement. It formalizes selected relationships and a finite negotiation procedure, then tests implementations on reproducible instances. Its central contribution is a traceable reconstruction connecting source statements, assumptions, proofs, and executable code, with limitations made explicit.

  • Problem

    The thesis’s Nash-to-core connection is under-specified without explicit outsider opportunities, and the paper asks what conditions make links between strategic choice, cooperative stability, and efficiency precise.

    Source: §1 · p. 2

  • Method

    The paper reconstructs selected planning claims as explicit models, proves a finite negotiation procedure’s guarantees, and compares its implementation with a documented heuristic reconstruction on shared finite instances.

    Source: §1 · p. 2

  • Results

    The investigation supplies a source-to-model-to-proof correspondence and finite-instance evidence for the reconstructed coordination logic under stated assumptions.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The case study shows how engineering intuitions can be reconstructed as mathematical claims whose assumptions, proofs, and computational consequences can be inspected.

    Source: Relationship to the 2018 engineering… · p. 21

    The two-person proof does not extend to more players merely because a procedure uses pairs, and does not establish globally stable agreements from arbitrary pairwise bargaining.

    Source: §3 · p. 4

Abstract

from arXiv · show

We present an AI-assisted mathematical addendum to Strategic Trip Planning: Striking a Balance Between Competition and Cooperation (Amar, 2018). We reconstruct selected relationships between strategic choice, cooperative stability, participant approval and enforcement. The thesis's Nash-to-core proposition is under-specified until outsider opportunities are stated. We verify two-person implications under fixed outsiders and explicit efficiency conditions. Under isolation, the original example has an empty TU core; its funded counterpart uses an explicit external subsidy. For a monotone resource model we characterize the exact financing gap. A finite negotiation procedure implemented in Lean is proved to terminate with participant approval, joint-cost non-worsening and local optimality against permitted approved moves. Supporting formalizations address bargaining geometry and regret-based efficiency. A resource-game counterinstance shows why monotonicity alone provides no uniform price-of-anarchy bound. Reproducible computations compare a documented heuristic reconstruction with the verified procedure on 44 source-based instances and 96 starting cases from four additional synthetic network families. Acceptance-matched heuristic and randomized pairwise-search controls contextualize the optimization results. The mathematical ingredients are established results; the contribution is a traceable reconstruction linking source statements, explicit assumptions, checked proofs, executable code and retained counterinstances. The study illustrates how AI-assisted investigation can turn engineering intuitions from legacy research into precise mathematical claims whose conditions and computational consequences can be inspected and reproduced.

1. Introduction

The paper reconstructs selected cooperation and competition claims from a 2018 planning thesis as explicit mathematical models, proofs, and executable procedures. It combines formal guarantees with reproducible finite-instance tests while distinguishing theorem-backed claims from observed behavior.

1. Introduction

  • The motivating planning problem involves individually motivated travellers whose routes interact through shared resources and may become costly when choices overlap.The thesis framework combined personalized route generation, team formation, and bargaining.Source: §1 · p. 1
  • The work is a case study in AI-assisted reconstruction that connects source statements to explicit assumptions, checkable theorems, and executable procedures.It does not present the thesis’s original engineering work as a mathematical-theory contribution.Source: §1 · p. 2
  • The paper asks what must be specified for links between competitive choice, cooperative stability, and collective efficiency to hold.Its questions concern game actions and costs, departing-coalition opportunities, referee enforcement, and repeated-game learning costs.Source: §1 · p. 2
  • The treatment specifies coalition opportunities and financing, proves a finite negotiation procedure’s guarantees, and compares a documented thesis-heuristic reconstruction with the executable procedure on shared instances.The original two-traveller model provides an end-to-end example; enforcement and regret results address additional implementation and repeated-outcome questions.Source: §1 · p. 2
  • New reproducible simulations test the coordination logic on newly generated inputs, while Lean proofs establish guarantees only under the stated reconstruction and model assumptions.The evidence includes reproducible generators, shared-instance comparisons, and exhaustive finite benchmarks.Source: §1 · pp. 1–2

2. Strategic actions and cooperative opportunities

The paper defines finite strategic games with profile-dependent costs and distinguishes physical costs from referee charges and learning scores. It then separates transferable and nontransferable stability and makes coalition departure opportunities explicit.

2. Strategic actions and cooperative opportunities

  • Finite action sets form a profile space, and profile-dependent costs capture resource externalities that route scores on individual action sets alone do not specify.The model does not assume independently chosen baseline favourites form a Nash equilibrium.Source: §2 · pp. 2–3

2.1 Transferable and nontransferable stability

  • Transferable-utility core claims require a common cost/payment scale and real transfers, whereas NTU blocking requires a coalition deviation that strictly lowers every member’s cost.A lower coalition total alone need not be an NTU block if one member loses.Source: §2.1 · p. 3

2.2 Two explicit outsider conventions

  • Fixed-outsider opportunities hold nonmembers to their reference plans, while isolation removes outsiders and recomputes coalition costs under an explicit resource model.Leaving a referee’s jurisdiction may create yet another opportunity, so exit rights belong in the mechanism specification.Source: §2.2 · p. 4

3. A precise equilibrium-to-core bridge

The paper makes the Nash-to-core connection conditional on explicit coalition opportunities and efficiency assumptions. In the two-traveller example, fixed outsiders support the result, while isolation exposes a financing problem; the bargaining geometry separately characterizes attainable expected gains.

3. A precise equilibrium-to-core bridge

  • For two players, Nash equilibrium plus Pareto efficiency implies the fixed-outsider NTU core, while Nash equilibrium plus social optimality implies the fixed-outsider TU cost core.Under the same outsider rule, the NTU core corresponds to strong Nash; the result is a sufficient two-person completion, not a general multi-player result.Source: §3 · p. 4

3.1 The original two-traveller instance

  • At (p1, p2), unilateral alternatives cost 7 and 8 instead of 4 and 5, and the profile is Nash, Pareto efficient, and minimum-total-cost among the four profiles.Under isolation, singleton costs of 4 and a joint cost of at least 9 make the TU core empty; correlated lotteries do not remove the obstruction.Source: §3.1 · p. 5

3.2 Bargaining geometry of the two-traveller example

  • The gain frontier runs between (4, 3) and (3, 4), with total expected cost 9; a half-and-half joint lottery attains equal gains of 7/2 and the Nash-product bound 49/4.The geometry uses the interacting status quo (8, 8); the joint lottery is not an independent mixed strategy or a deterministic assignment.Source: §3.2 · p. 5, Figure 1 · p. 6

3.3 Adopted counterpart rule for the revised proposition

  • The revised counterpart adopts fixed-outsider opportunities and proves the two-person results under explicit efficiency conditions; its scope is not a machine-verified balanced-collection characterization.The multi-traveller financed result is treated separately.Source: §3.3 · p. 6

4. Congestion, coalition budgets and the cost of stability

The monotone resource model identifies the financing gap between isolated singleton promises and joint service, and characterizes the minimum subsidy or relaxation needed for stability. An explicit subsidy can also yield a funded core while preserving a physical Nash agreement, subject to the stated implementation conditions.

4. Congestion, coalition budgets and the cost of stability

  • The resource model is a source-supported subclass, not a representation of every reward, production, discount, or private-fare mechanism.Those omitted mechanisms require another model and may reverse the budget conclusion.Source: §4 · p. 7
  • Monotone congestion makes each coalition’s cost at least the sum of members’ optimized isolated costs, yielding singleton domination.The model allows player-specific private costs and asymmetric feasible routes.Source: §4 · p. 7
  • When isolated singleton values sum to the grand-coalition value, assigning each singleton value is efficient and satisfies every coalition bound.Source: §4 · p. 7
  • A positive gap cannot be covered by payment rearrangement while guaranteeing every isolated singleton opportunity; it may exist even at a social optimum.The gap is not a Nash inefficiency measure, and comparison with an interacting noncooperative baseline differs from removing other travellers.Source: §4 · p. 7

4.1 Exact budget repair and approximate stability

  • The minimum stabilizing subsidy is G: at σ = G, singleton-value payments are stable, and every stable subsidized allocation requires σ ≥ G.The subsidy is an explicit financing extension; the original coalition departure opportunities remain available.Source: §4.1 · p. 7
  • With the full budget retained, the minimum uniform per-member relaxation is G/n.For the thesis table, G = 1: subsidy 1 stabilizes payments (4, 4), while tolerance 1/2 admits allocation (4.5, 4.5); these are TU conclusions, not claims about attainable NTU cost vectors.Source: §4.1 · pp. 7–8

4.2 An admissible financed isolation counterpart

  • Fixed participation rebates totaling G make the realized net allocation at a physical Nash and social optimum belong to the funded game’s ordinary TU cost core.At the example profile, costs (4, 5) become net costs (4, 4) under rebates (0, 1); full-team finance and isolated exit opportunities must be implemented as specified.Source: §4.2 · pp. 8–9

5. Contract enforcement and its limits

The proposed charge makes every announced contract strongly Nash and prevents coalitions from lowering their aggregate implemented cost. This guarantee depends on pricing authority and does not establish physical efficiency, truthfulness, or consent from an unspecified exit option.

5. Contract enforcement and its limits

  • The nonnegative charge, zero at the agreement, makes every contract strongly Nash and prevents coalitions from lowering aggregate implemented cost.In finite games, realized costs belong to a fixed-outsider TU cost core whose opportunities remain subject to the charge rule.Source: §5 · p. 9
  • The rule can strongly implement an inefficient contract: the all-preferred profile costs 16 rather than 9, so choosing an efficient agreement remains separate.The result is not dominant-strategy truthfulness, app credibility, or stability after a coalition escapes the mechanism’s jurisdiction.Source: §5 · p. 9
  • Participation requires a separate individual-rationality condition comparing the contract with each traveller’s outside-app exit opportunity.The theorem supplies no consent guarantee without a specified exit-payoff model.Source: §5 · p. 9

6. Repeated play, empirical equilibrium and observed costs

The paper formalizes finite-time regret and smoothness guarantees, then distinguishes observed learning costs from physical costs when prices or personalization vary. Its finite resource-game results include an unbounded price-of-anarchy family, showing that monotone overlap costs and private preferences alone do not provide a uniform finite bound.

6. Repeated play, empirical equilibrium and observed costs

  • The empirical action distribution satisfies CCE deviation inequalities when every player’s cumulative fixed-action improvement is bounded by the stated regret bound.Nonnegative bounds per round give approximate-CCE tolerances; nonpositive fixed-action deviation sums give an exact CCE.Source: §6 · pp. 9–10

6.1 Smoothness and physical efficiency

  • Smoothness and regret yield a finite-time efficiency bound against a common feasible joint comparator, with a positive denominator T(1 − µ).The comparator need not be optimal; applying the result to an optimum requires its existence and feasibility.Source: §6.1 · p. 10

6.2 Changing referee prices and personalization

  • Observed regret transfers to physical regret with a distortion remainder, but persistent action-dependent distortion can leave a nonvanishing efficiency remainder.At the all-preferred profile, physical unilateral improvement is 3 per traveller while the enforced implemented improvement is zero; an action-independent fee cancels.Source: §6.2 · pp. 10–11
  • The price-distortion result retains a fixed player set, action sets, and physical base game; turnover or a changing physical environment needs another comparator model.Source: §6.2 · p. 11

6.3 Social cost and pure price of anarchy

  • Under smoothness, every pure Nash equilibrium has cost at most λC∗/(1 − µ); the bound requires smoothness of the actual cost model.The unshifted counterinstance cannot satisfy the stated smoothness condition for any real λ and µ < 1.Source: §6.3 · pp. 11–12
  • Among 92 enumerated games, all have pure equilibria; the largest ratio among 88 positive-optimum games is 5, while a zero-optimum game has a positive-cost Nash equilibrium.The four-traveller layered instance reaches ratio 5; in the ring-with-shortcuts counterinstance, profile 9 costs (3, 0, 0, 0) while profile 10 costs (0, 0, 0, 0).Source: §6.3 · p. 11
  • Monotone overlap costs and private preferences alone provide no uniform finite pure-price-of-anarchy bound in the declared resource class.The verified positive-base-cost family has positive optimum and a Nash equilibrium costing more than any chosen multiple of that optimum.Source: §6.3 · pp. 11–12

7. A bounded engineering guarantee and certification interface

The paper specifies participation bounds and a finite negotiation procedure, then tests a documented heuristic reconstruction against the procedure on source-based and synthetic instances. Its guarantees are bounded: approval and joint-cost non-worsening are proved, while terminal optimality is local to permitted moves.

7.1 Participation-safe finite selection

  • Theorem 11 selects a minimum-cost plan within declared participant ceilings, guaranteeing joint cost no greater than a feasible approved baseline.It does not guarantee strict improvement, unconstrained social optimality, truthfulness, or coalition stability.Source: §7.1 · p. 12

7.2 Reusing the original negotiation results

  • The original ten-traveller example’s final cost vector is no greater coordinatewise than its baseline, with total cost falling from 320 to 282.Some provisional rounds exceed individual baseline costs, so the example distinguishes interim negotiation from final participant approval.Source: §7.2 · p. 13

7.3 An executable finite negotiation procedure

  • Theorem 12 proves that the finite procedure terminates with an approved feasible plan whose joint cost does not exceed the baseline, with no approved permitted improving move remaining.The scan commits only approved moves with strict joint-cost descent and restarts after each commitment.Source: §7.3 · p. 13
  • The procedure guarantees only local optimality against approved permitted moves, not global optimality or physical Nash stability; a complete scan can be exponential in traveller count.Synthetic counterexamples show a cheaper approved plan may require a three-person change, or an individual improvement may violate another traveller’s ceiling.Source: §7.3 · p. 14

7.4 Reconstructing the ten-traveller heuristic on common instances

  • On the coalesced vertex instance, H1 and V both reach the computed minimum of 254 from baseline cost 320; on the coalesced edge instance, both reach 148 from 178.These are reconstructed results, not recovered optima from the original experiment.Source: §7.4 · p. 15
  • Across 21 coalesced cases per resource model, V is approved, physically Nash, and pairwise-terminal in all cases, while heuristic rates vary by scheduling and resource model.H2 coincides with H1 throughout this collection; V’s observed global optimality is not a guarantee of Theorem 12.Source: §7.4 · p. 15

7.5 Independent network families

  • The four synthetic network families vary topology, traveller count, and starting plan while retaining a two-route additive overlap-cost model; they are controlled tests, not representative transport samples.The largest reported relative search gap is 50%, and an approved individual deviation can violate another traveller’s baseline ceiling.Source: §7.5 · pp. 17–18
  • V preserves approval and reaches an approved pairwise terminal point in all 96 cases, attaining the exact approved minimum in 92 and the unrestricted minimum in 57.V is physically Nash in 67 cases; H1’s raw outcomes are approved in 56, and fallback-adjusted outcomes attain the approved minimum in 46.Source: §7.5 · p. 17, Figure 4 · p. 18

Retrospective matched controls

Matched controls contextualize the reconstructed procedures’ optimization results, while Section 7.6 lays out a certification workflow that separates game assumptions, coalition opportunities, enforcement, and repeated-outcome evidence.

Retrospective matched controls

  • The 96-case controls are retrospective, and their proposal neighborhoods differ from V’s full one-/two-person neighborhood.H1-A adds V’s baseline-ceiling filter to H1 negotiation and withdrawal; H1-A-strict additionally requires strict total-cost descent.Source: Retrospective matched controls · p. 18
  • V reaches the approved optimum in 92/96 cases with mean gap 0.1771; H1-A and H1-A-strict reach it in 54/96 cases, with mean gaps 3.3958 and 3.4583, respectively.The table also reports raw approved counts of 96/96 for V, H1-A, and H1-A-strict, versus 56/96 for H1.Source: Retrospective matched controls · p. 19
  • V’s higher approved-optimum count does not establish pointwise dominance: H1-A beats V on one grid case, returning cost 14 against V’s 16.Adding approval can reduce physical Nash incidence, so the procedures’ objectives must be distinguished.Source: Retrospective matched controls · p. 19
  • Randomized pairwise search reaches the approved optimum in 93.148% of same-baseline trials on average, versus V’s 95.833%; its mean gap is 0.3733 versus V’s 0.1771.Both randomized arms reach the approved minimum on every trial in 85/96 cases; random approved initialization is a separate landscape diagnostic, not a same-start operational control.Source: Retrospective matched controls · p. 19

7.6 Certification obligations

  • The results support a testable certification layer around personalized planning and negotiation, not a claim that every bargaining process converges.Source: §7.6 · p. 19
  • The certification workflow first specifies feasible actions, costs, constraints, and coalition opportunities, then separates negotiated selection from the referee’s declared enforcement rule.Quality claims are checked against physical costs and appropriate outside options, not inferred from implementation alone.Source: §7.6 · p. 19
  • Repeated-outcome certification uses realized history, regret, and price-distortion bounds; smoothness must be proved for the physical cost class or checked exhaustively.A referee’s presence alone does not supply a smoothness certificate.Source: §7.6 · pp. 19–20
  • The specified finite completion terminates, but sublinear regret and guarantees for asynchronous or threat-based variants require further analysis.A regret certificate may be large, and a bargaining run may fail its stopping criterion.Source: §7.6 · p. 20

8. Verification, prior art and research significance

The paper links source statements to explicit models, checked proofs, executable procedures, and retained computational evidence. Its conclusions are bounded by the declared assumptions and by the finite instances studied.

8. Verification, prior art and research significance

  • The larger-instance results use exact finite computation with independent checks, not additional kernel-proved certificates; the project kernel-checks general theorems and declared two-traveller results.No admissions, custom mathematical postulates, unsafe proof shortcuts, or native decision oracles are used.Source: §8 · p. 20
  • The semantic correspondence remains conditional: the monotone model, penalty formula, subsidy, and observed-cost distortion are declared extensions, and the original larger numerical experiments were not replicated.The controlled reconstruction is computational evidence, not a recovered original implementation.Source: §8 · p. 20
  • The mathematical ingredients are attributed to established frameworks; the claimed contribution is their formal integration, executable procedure, and reproducible source-based comparisons.No new general equilibrium or bargaining solution concept is asserted.Source: §8 · p. 20

Relationship to the 2018 engineering framework

  • The addendum strengthens the 2018 thesis with explicit conditions and machine-checked proofs, plus implementations tested on new synthetic data.The engineering idea is coordinating personalized objectives with shared-resource use.Source: Relationship to the 2018 engineering… · p. 20
  • The study includes 44 source-based reconstructions and 48 additional graph/route/cost instances evaluated from 96 starting profiles across four network families.Matched controls indicate the high optimum-hit count is largely consistent with generic pairwise local search, rather than identifying a distinctive optimization benefit.Source: Relationship to the 2018 engineering… · p. 21
  • Coordination preserves baseline cost ceilings and reaches an approved local terminal outcome in all 96 broader-network cases; 66 strictly improve joint cost and 30 retain the baseline.The exact approved minimum is attained in 92 cases, while four residual search gaps and 29 underlying-cost non-Nash endpoints limit stronger claims.Source: Relationship to the 2018 engineering… · p. 21
  • The paper presents AI-assisted reconstruction as a case study in making engineering intuitions precise, with Lean proofs and reproducible experiments providing distinct checks.The stated conclusions are limited to what the evidence supports.Source: Relationship to the 2018 engineering… · p. 21

Artifact availability and reproduction

  • The companion reproducibility bundle contains the pinned Lake manifest, Lean sources, executable entry points, reconstruction inputs, plotting code, and finite certificates.The draft has no public archive identifier yet.Source: Artifact availability and reproduction · p. 22

Appendix A. Traceable source and proof correspondence

The appendix maps source claims to formal declarations and states which assumptions and extensions support each result. It distinguishes verified theorem statements from conditional applications and computational evidence.

Appendix A. Traceable source and proof correspondence

  • The source proposition’s outsider opportunities are under-specified, so the appendix records explicit fixed-outsider and isolated-opportunity replacements for the two-person claims.The correspondence table identifies the associated theorem declarations and source locations.Source: Appendix A · p. 23
  • The fixed-outsider results require explicit efficiency conditions: Pareto efficiency for NTU claims and minimum joint cost for TU claims.The appendix maps these conditions to the two-player Nash/core theorems and the source bargaining example.Source: Appendix A · p. 23
  • The listed extensions include monotone resource costs, isolation financing, approximate stability, referee contracts, and observed-cost distortion, each with its own declared assumptions.The correspondence distinguishes an explicit financing extension from an original subsidy theorem.Source: Appendix A · pp. 23–24
  • The appendix maps the finite negotiation guarantee to an executable protocol with explicit sequential scan, acceptance, strict-descent, and stopping rules.This is not a proof of an unspecified threat-based implementation.Source: Appendix A · p. 24

Related papers

This paper cites

Loading 2610.29637v1…