# Proof: Automation Nash Equilibrium vs Cooperative Optimum

- **Generated:** 2026-04-15
- **Verdict:** PROVED
- **Audit trail:** [proof_audit.md](proof_audit.md) | [proof.py](proof.py)

## Evidence Summary

| ID | Fact | Verified |
|----|------|----------|
| A1 | Nash equilibrium rate alpha^NE = (s - ell/N)/k via FOC | Computed: True (symbolic residual = 0) |
| A2 | Cooperative optimum alpha^CO = (s - ell)/k via joint FOC | Computed: True (symbolic residual = 0) |
| A3 | Gap alpha^NE - alpha^CO = ell*(1 - 1/N)/k > 0 | Computed: True (formula confirmed, strictly positive) |

## Proof Logic

The claim specifies a symmetric N-firm game where each firm chooses an automation rate to maximize individual profit, which includes revenue from a shared demand pool minus labor costs and quadratic integration friction. The key tension: each firm's automation reduces sectoral wage income and hence demand, but this demand externality is diluted across N firms, so each firm under-accounts for it.

**Nash Equilibrium (A1).** Differentiating firm i's profit with respect to its automation rate alpha_i yields a linear first-order condition. The demand externality contributes a term -ell/N (the demand loss per displaced worker, diluted by market share 1/N). Solving gives alpha_i* = (s - ell/N)/k. Crucially, this expression does not depend on rivals' choices -- each firm has a dominant strategy. At symmetric equilibrium all firms play this rate. SymPy symbolic differentiation confirms the formula exactly (residual = 0).

**Cooperative Optimum (A2).** A joint planner maximizing total industry profit internalizes the full demand externality. When all firms play a common rate alpha, the joint FOC includes the undiluted demand loss -ell (not -ell/N). Solving gives alpha^CO = (s - ell)/k. Again confirmed symbolically with zero residual.

**Over-Automation Gap (A3).** The difference alpha^NE - alpha^CO = ell*(1 - 1/N)/k. Each factor is strictly positive: ell > 0 by construction (lambda > 0, 1-eta > 0, w > 0); (1 - 1/N) >= 1/2 for N >= 2; k > 0 by assumption. The gap is strictly positive, confirming that firms over-automate relative to the cooperative optimum.

The economic intuition: each firm captures the full cost saving s from automation but bears only 1/N of the demand destruction ell. The cooperative planner sees the full ell. The gap ell*(1-1/N)/k measures exactly how much this externality dilution inflates automation.

## What could challenge this verdict?

Four adversarial checks were investigated:

1. **Second-order conditions.** Both the individual and joint profit functions are strictly concave in the choice variable (d^2 pi_i/d alpha_i^2 = -kL < 0, d^2 Pi/d alpha^2 = -NkL < 0), confirming that the FOC solutions are global maxima, not minima or saddle points.

2. **Uniqueness of Nash equilibrium.** Because each firm's optimal automation rate is independent of rivals' strategies (dominant strategy), the symmetric equilibrium is the unique Nash equilibrium. No asymmetric equilibria exist.

3. **Boundary feasibility.** The formulas are interior (unconstrained) FOC solutions. If parameters place them outside [0,1], the constrained solution would differ. The algebraic identities hold regardless; interiority is an implicit parameter assumption.

4. **Well-specified demand.** Even at full automation (all alpha_j = 1), demand D = A + lambda*w*L*N*eta >= A > 0. The model is well-specified.

## Conclusion

**Verdict: PROVED.** All three claimed results are confirmed by symbolic computation (SymPy) and independently verified by numerical spot-check:

- The Nash equilibrium automation rate is alpha^NE = (s - ell/N)/k (A1)
- The cooperative optimum is alpha^CO = (s - ell)/k (A2)
- The over-automation gap alpha^NE - alpha^CO = ell*(1 - 1/N)/k is strictly positive for N >= 2 (A3)

---

Generated by [proof-engine](https://github.com/yaniv-golan/proof-engine) v1.16.0 on 2026-04-15.