# Record 004 proof artifact

This is a deliberately small, synthetic allocation problem. It contains no
employer data and no data or findings from an unpublished paper.

Six organisations need one assisted migration window each. Three windows can
accept two migrations apiece. An earlier provisional plan put three migrations
in Window 1, but the current capacity is two, so at least one commitment must
move. The product team has also assigned each organisation a synthetic
operational-fit score for each window.

| Request | Window 1 | Window 2 | Window 3 | Prior plan |
| :------ | -------: | -------: | -------: | :--------- |
| R1      |       35 |       30 |       95 | Window 1   |
| R2      |       25 |       80 |       40 | Window 1   |
| R3      |       40 |       35 |       95 | Window 1   |
| R4      |       65 |       40 |       85 | Window 2   |
| R5      |       20 |       50 |       40 | Window 3   |
| R6      |       20 |       20 |       50 | Window 3   |

The inputs and feasible schedules stay fixed. Only the objective policy changes:

1. **Efficiency:** maximise total fit.
2. **Minimum-fit protection:** maximise the minimum request fit, then total fit.
3. **Continuity:** minimise changed commitments, then maximise total fit.

The second phase in Policies 2 and 3 is lexicographic. It fixes the proven
primary optimum before optimising the secondary term, so a larger secondary
gain can never trade away the primary result.

## Reproduce

Requirements:

- Python 3.10 or newer, using only the standard library
- MiniZinc 2.9 or newer with the open-source COIN-BC solver

Run:

```sh
python3 run.py
python3 run.py --json
```

`run.py` solves every optimisation phase with MiniZinc/COIN-BC and then checks
the result using an independent exhaustive enumeration of all 90 feasible
schedules. It fails unless every phase reports `OPTIMAL_SOLUTION`, all three
final optima are unique, and both implementations agree exactly.

## What this artifact establishes

It establishes a bounded counterexample: identical inputs, constraints, and
solver can produce materially different stakeholder outcomes under defensible
objective policies. It does not establish that these scores capture real-world
preference, that max-min is universally fair, or that one policy should be used
in production. Those are product decisions, which is the point of the example.