> **ARCHIVED 2026-07-20** — Diagnostic daté 2026-05-18, valeur = historique uniquement. Superseded by EPIC #4365 absorption (StableMarriage absorbed into `game_theory_lean/StableMarriage/` post-c.304-305). Les 6 sorrys documentés (GaleShapley.lean L116/L117/L146, Lattice.lean L324/L387/L727, Basic.lean L308) restent dans le KB prover actif via `intractable_targets.json` (référence déplacée). Le contenu verbatim est préservé ci-dessous pour audit rétrospectif. Source triage : PR #7426 (c.674). Archiveur : po-2026 worker (c.696). Anti-contamination L420 owner-dispatch : Lean core = po-2026.

# Stable Marriage Lean 4 — Intractable Sorry Diagnosis

**Date:** 2026-05-18
**Author:** myia-po-2026 (prover BG iterations + manual analysis)
**Status:** 6 sorrys remaining, all INTRACTABLE until substantial new formalization

---

## Summary

The stable marriage Lean 4 port has 6 remaining sorrys across 3 files. Prover BG iterations (10+ sessions, multi-agent + autonomous modes, Director GPT-5.5 consulted) have consistently failed to close any of them. Root cause: these sorrys require ~200-300 lines of **new formalization** (rural hospitals theorem, Knuth lattice duality) that does not exist in our codebase or Mathlib.

## Sorry Inventory

### Blocker 1: Man-Optimality (GaleShapley.lean L116)

```lean
theorem gale_shapley_man_optimal ... : ∃ μ, IsManOptimal prof μ :=
  ...
  refine ⟨μ, ?_⟩
  unfold IsManOptimal
  constructor
  · sorry  -- L116: IsStable prof μ
  · sorry  -- L117: ∀ μ', IsStable prof μ' → ∀ m, menPref m (μ.sp m) ≤ menPref m (μ'.sp m)
```

**Why intractable:**
- `IsStable prof μ` (L116) requires proving the GS matching has no blocking pairs — already proved as `gale_shapley_stable` in Lemmas.lean, but the witness type and the way it's threaded through `gsFinalMatching` makes direct reuse complex.
- The optimality property (L117) requires the **rural hospitals theorem**: the GS algorithm gives each man the best partner among all stable matchings. This is a non-trivial combinatorial argument needing its own induction on the GS algorithm's intermediate states.

**Effort estimate:** 80-120 lines new formalization (rural hospitals lemma + optimality induction).

### Blocker 2: Woman-Pessimality (GaleShapley.lean L146)

```lean
-- INTRACTABLE_UNTIL_GS_IMPL: Knuth 1976 lattice duality theorem.
sorry  -- L146
```

**Why intractable:**
- Woman-pessimality is derived from man-optimality via Knuth's lattice duality: the woman-pessimal matching is the man-optimal matching of the reversed preference profile.
- Requires both Blocker 1 (man-optimality) AND the lattice duality theorem.

**Effort estimate:** 40-60 lines (after Blocker 1 is resolved), or 120-180 lines standalone.

### Blocker 3: meetSpouse "Different Women" Cases (Lattice.lean L324, L387)

```lean
-- L324: meet case where ν.sp m₁ ≠ μ.sp m₁ and ν.sp m₁ ≠ w (different women)
sorry

-- L387: symmetric "different women" case (ν.sp₁ ≠ μ.sp₂)
sorry
```

**Why intractable:**
- These arise in `meet_isStable` proof. When two matchings μ and ν give man m₁ different women, and neither is the "meet spouse", we need to show stability is preserved.
- Requires the **rural hospitals theorem** or the **Knuth lattice structure** to argue about how the meet of two stable matchings distributes preferences.
- For n ≤ 2: trivially impossible (can't have 3 distinct women in Fin 2). For n ≥ 3: needs the lattice argument.

**Effort estimate:** 60-80 lines per case (shared infrastructure from rural hospitals).

### Blocker 4: Doctor-Optimal (Lattice.lean L727)

```lean
theorem doctor_optimal ... (hstable : IsStable prof μ') : ManLE prof μ_gs μ' :=
  fun m => by sorry
```

**Why intractable:**
- This is essentially man-optimality of the GS matching, rephrased as `ManLE` ordering.
- Same underlying requirement as Blocker 1 (rural hospitals).

**Effort estimate:** 20-30 lines (after Blocker 1 infrastructure exists).

### Blocker 5: hCore Nonemptiness (Basic.lean L308)

```lean
-- bondareva_shapley_backward, step: hP_nonempty → hCore
sorry  -- L308
```

**Why intractable:**
- This is the Bondareva-Shapley theorem core nonemptiness proof. Requires Farkas' lemma or separating hyperplane in the context of balanced games.
- Completely different mathematical machinery from stable marriage (convex geometry vs combinatorial matching).

**Effort estimate:** 100-150 lines (hyperplane separation + core characterization).

---

## Blocker Clustering

| Cluster | Sorrys | Underlying Theory | Priority |
|---------|--------|-------------------|----------|
| **Rural Hospitals / GS Optimality** | L116, L117, L146, L324, L387, L727 | GS algorithm induction + lattice duality | HIGH (6/6 sorrys) |
| **Bondareva-Shapley Core** | L308 | Convex geometry, separating hyperplane | LOW (1/6 sorrys, independent project) |

All stable marriage sorrys (5/6) trace to a single missing formalization: **rural hospitals theorem + GS optimality**.

## Options

### Option A: Formalize Rural Hospitals (RECOMMENDED)
- Implement `theorem rural_hospitals` in a new file `StableMarriage/RuralHospitals.lean`
- Then derive man-optimality, woman-pessimality, and lattice meet stability
- **Effort:** ~200-300 lines new Lean code
- **Unlocks:** all 5 stable marriage sorrys

### Option B: Prove via Lattice Theory
- Build the Knuth lattice of stable matchings (`Lattice.lean` already partially exists)
- Derive everything from the lattice structure
- **Effort:** ~250-350 lines new Lean code
- **Unlocks:** all 5 stable marriage sorrys + lattice completeness

### Option C: Wait for Mathlib
- Some of this machinery may appear in Mathlib's `Combinatorics.GameTheory` or similar
- **Timeline:** unknown (months to years)
- **Risk:** Mathlib doesn't have matching theory yet

## Prover Iteration History

| Date | Mode | Target | Iterations | Result |
|------|------|--------|------------|--------|
| 2026-05-15 | multi | L97 man_optimal | 8 | INTRACTABLE |
| 2026-05-15 | autonomous | L308 hCore | 10 | INTRACTABLE (5.9h) |
| 2026-05-16 | multi | Lemmas (gsNoBlockingPairs) | 6 | **PROVED** |
| 2026-05-17 | multi | L97 man_optimal (F8 wired) | 15 | INTRACTABLE (Director 2x consulted) |
| 2026-05-18 | multi | L97 man_optimal (F8+Director) | 15 | RUNNING |

The prover successfully proved Lemmas (gsNoBlockingPairs, gsFinalMatching, gsAllWomenMatched) but consistently fails on the 6 sorrys above. Director (GPT-5.5 via OpenRouter) confirms: the missing piece is mathematical formalization, not search depth.

## Conclusion

**Verdict:** All 6 sorrys are INTRACTABLE until Option A or B is implemented. The prover architecture (multi-agent + Director + F8 escalation) is functioning correctly but cannot invent new theorems. The next actionable step is human-directed formalization of the rural hospitals theorem.