Lesson 4 of 10

When everything is P1

If every team can call its request urgent, what makes the label mean anything?

The problem

Two urgent requests, one week of help

Two product teams want the same scarce thing in the same week. The Warranty Claims team wants help with a document reader that keeps missing exclusions buried in scanned contract annexes. The Field Repair Dispatch team wants help with a reader that pulls part numbers out of service manuals so crews leave with the right parts. The scarce thing might be a block of GPU time, a slice of the vendor budget, or — most often — one week of the one specialist who knows how to fix this kind of problem.

Both requests arrive marked P1. Of course they do. Each team knows its own work better than anyone, and each genuinely believes it matters. But only one of them can go first, and the person who decides cannot see inside either team's head.

This is not a story about bad people. It is a story about a label that costs nothing to use. When saying "urgent" is free and saying it improves your chances, everyone says it, and the label stops carrying information. The people who allocate the scarce resource then have to decide blind, or by who shouts loudest, or by who asked first.

We want to know three things. Why does a free label collapse? What would make a team's claim mean something again? And when does the effort of checking claims cost more than the better decision it buys?

The intuition

Why the label collapses, and what could rescue it

Start with the arrangement where nothing is shared. Each team buys its own GPU time, hires its own contractor, waits its turn in a first-come queue. Nobody has to judge anyone's urgency. The cost is the one the earlier lessons counted: the same lesson gets paid for twice, and a single scarce expert cannot be split into two half-experts who each know half as much.

Now share. One person — call them the sponsor, because they hold the budget — awards the scarce slot to one team at a time. Sharing has an obvious advantage: the slot can go where it does the most good. But that only works if the sponsor knows where it does the most good, and that knowledge sits with the teams. The team knows whether its idea is strong (likely to work and worth it) or weak. The sponsor does not.

So the shared route has a new friction that the local route never had: each team's report affects its own chances. That is exactly the situation game theory was built for. A game, here, is any situation where what is best for you depends on what the others do. A team deciding whether to call its request urgent has to think about what the other team will call its request. The outcome we look for is an equilibrium: a pair of plans where neither team could do better by changing only its own plan. It is the point where everyone has already taken everyone else's reasoning into account.

We will look at three versions of the same contest, each one adding one thing.

A free label. Each team says "high" or "low". The slot goes to the team that says high; if both say the same thing, a fair coin decides.
A costly pitch with a test. To be considered, a team must put effort into a pitch. A reviewer then runs a quick test of the idea. Strong ideas pass more often than weak ones. The slot goes to a team that passes; if both pass, a coin decides.
A checked claim with an honest alternative. A team can claim the slot, or instead file a complete record of what it has learned (and earn a small credit for it), or say nothing. Claims are checked. A claim the evidence does not support can be caught and penalized. A supported claim can be wrongly flagged too.

Each version has a pro and a con. The free label is cheap and useless. The costly pitch sorts strong ideas from weak ones, but only when the effort sits in the right window, and the tests cost the company real money. The checked claim can make telling the truth the best move for every team, but only if the checks can tell the difference, the penalties are real, and the checks are cheap enough. Any of these can go either way. That is why we need the arithmetic.

The model

Three contests, one slot

1. The free label

Let the slot be worth $B$ to the team that wins it — a private benefit, measured in the team's own illustrative units. With a free label, a team that says high when the other says low wins for sure; when both say the same thing, each wins half the time.

Definition · free label, fair coin on ties

\begin{aligned}\text{say high, rival says low:}\ & B &\quad \text{say low, rival says low:}\ & \tfrac12 B\\ \text{say high, rival says high:}\ & \tfrac12 B &\quad \text{say low, rival says high:}\ & 0\end{aligned}

In words: whatever the rival says, saying high gives the team more: $B$ beats half of $B$ , and half of $B$ beats nothing. So both teams say high, and the label carries no information.

Look at each column. If the rival says low, saying high gives $B$ instead of half of $B$ . If the rival says high, saying high gives half of $B$ instead of nothing. Saying high is better whatever the rival does. Game theorists call such a choice strictly dominant. Both teams pick it, the coin decides everything, and the sponsor has learned nothing. That is the P1 trap, in two lines.

2. The costly pitch

Now a pitch costs the team effort $\kappa$ , paid whether it wins or not. A share $\rho$ of ideas are strong. The reviewer's test passes a strong idea with chance $p_{\text{strong}}$ and a weak idea with chance $p_{\text{weak}}$ . Suppose the rival pitches only when its idea is strong. Then a team whose idea passes with chance $p$ wins outright if the rival does not pass, and half the time if both pass:

Derived by hand · gain from pitching

\text{gain from pitching} \;=\; p\left(1-\tfrac12\,\rho\, p_{\text{strong}}\right)B \;-\; \kappa

In words: the chance of passing, times the chance of not having to share the slot, times what the slot is worth to the team, minus the effort of pitching.

The pitch sorts the teams when a strong team gains from pitching and a weak team would lose. Put $p = p_{\text{strong}}$ and $p = p_{\text{weak}}$ into the line above and ask for one positive and one negative answer:

Checked in Lean · the sorting window

p_{\text{weak}}\left(1-\tfrac12\rho\,p_{\text{strong}}\right)B \;<\; \kappa \;<\; p_{\text{strong}}\left(1-\tfrac12\rho\,p_{\text{strong}}\right)B

In words: the effort must be large enough to put off weak ideas and small enough to keep strong ones. With half the ideas strong, tests that pass strong ideas 3 times in 4 and weak ones 1 time in 4, and a slot worth 4 to the winner, the window runs from 13/16 to 39/16.

In our worked case, half the ideas are strong, the test passes a strong idea 3 times in 4 and a weak one 1 time in 4, and the slot is worth 4 to the team that wins it. The window runs from 13/16 (about 0.8) to 39/16 (about 2.4). At an effort of 3/2, a strong team expects to gain 15/16 and a weak team would expect to lose 11/16. Each team stays in its lane.

Sorting is one thing; paying for it is another. Each test costs the reviewer $\gamma$ , and a strong project, once funded, is worth $V_{\text{strong}}$ to the company. With two teams, each pitching only when strong, the company's gain over using the slot for ordinary work is:

Checked in Lean · what the company gets

\left(2\rho\,p_{\text{strong}}-(\rho\,p_{\text{strong}})^2\right)V_{\text{strong}} \;-\; 2\rho\,\gamma

In words: the chance that at least one strong idea passes, times what a strong project is worth, minus the expected number of tests times their cost.

With a strong project worth 8 and a test costing 1, that is 31/8, almost 4 units. With a strong project worth only 1, it is −25/64. The pitch sorts the teams just as well in both cases. In the second one, the sorting is simply not worth its tests.

Lesson 4 · Figure 1

A pitch sorts strong ideas from weak ones only inside a window of effort.

Shown at Effort a pitch costs the team: 1.50 illustrative units; What a strong project is worth to the company: 8 illustrative units. Turn on JavaScript to move the values.

Between 0.81 and 2.44, only strong ideas pitch. At effort 1.5 a strong team gains about 0.94, a weak team would lose about 0.69, and the company gains about 3.88 after paying for the tests.

Strong team, gain from pitching: 15/16
Weak team, gain from pitching: −11/16
Company, gain after tests: 31/8

Two teams, half the ideas strong; the test passes strong ideas 3 times in 4 and weak ones 1 time in 4; the slot is worth 4 to the winner and each test costs the reviewer 1. Lean checks both thresholds and the values at effort 3/2. The company's gain appears only where the teams sort.

Model result · checked in Lean

3. The checked claim

The pitch window is fragile: get the effort wrong and either everyone pitches or nobody does. The third contest gives a team a third option. It can claim the slot, file a record of what it has learned without claiming, or stay silent. A filed record earns the team a small net credit $R_{\text{file}}$ — recognition, say, after the effort of writing it. Claims are checked. A strong team's claim survives the check with chance $s_{\text{strong}}$ ; a weak team's with chance $s_{\text{weak}}$ . A claim that is flagged carries an expected penalty $\varphi_{\text{strong}}$ or $\varphi_{\text{weak}}$ , which is lower for strong teams because they are flagged less often.

Here is the trick. We do not need to know what the rival will do. We look for conditions under which telling the truth — strong teams claim, weak teams file a record — is best for each team whatever the rival does. The worst case for a strong claim is a rival who also claims and survives; the best case for a weak claim is a rival who stays out. So it is enough that:

Checked in Lean · truth is best whatever the rival does

\begin{aligned}\tfrac12\,B\,s_{\text{strong}}-\varphi_{\text{strong}}-\kappa \;&>\; R_{\text{file}} \;>\; 0\\ B\,s_{\text{weak}}-\varphi_{\text{weak}}-\kappa \;&<\; R_{\text{file}}\end{aligned}

In words: even when it must share the slot, a strong team prefers claiming to filing a record, and a record beats silence; even when it would win the slot alone, a weak team prefers filing a record to claiming.

In the worked case every claim is checked, a strong claim is wrongly flagged 1 time in 4, a weak claim is caught 3 times in 4, a flagged claim costs the team 4, the record earns a net 1/8, and the slot is still worth 4. A strong team that claims expects 23/16; filing a record would earn it only 1/8. A weak team that claims expects −35/16; filing a record earns 1/8. Nobody needs to be noble.

Then the company's ledger. The slot goes to a strong project with chance 39/64. A strong project is worth 8 and ordinary work in that slot is worth 2, so the better award is worth 117/32. Take away the expected cost of the checks and of handling the records, and the company keeps 93/32, about 2.9 units — if a check costs 1/2. Raise the cost of a check, and the gain shrinks one for one.

Lesson 4 · Figure 2

Checking claims pays only while a check costs less than about 3.4.

Shown at Cost of one check to the company: 0.50 illustrative units. Turn on JavaScript to move the values.

At 0.5 per check, checking pays: strong ideas claim, weak ones file their record instead, and the company gains about 2.91 over using the slot for ordinary work. Below 3.41 per check, this stays true.

Company gain over ordinary work: 93/32
Expected checks per round: 1
Break-even cost per check: 3.41

Teams tell the truth at every cost on this chart: the cost of a check falls on the company, not on the teams. Lean checks the gain at 1/2 (93/32) and at 4 (−19/32); the line between is computed by the tested model code.

Model result · checked in Lean

What each letter stands for

$B$: what the slot is worth to the team that wins itteam's illustrative units
$\kappa$: the effort a pitch or claim costs the team, paid win or loseteam's illustrative units
$\rho$: the share of ideas that are strongprobability
$p_{\text{strong}},\ p_{\text{weak}}$: the chance the reviewer's test passes a strong idea, a weak ideaprobability
$V_{\text{strong}}$: what a funded strong project is worth to the companyillustrative units
$\gamma$: what one test or check costs the companyillustrative units
$R_{\text{file}}$: the net credit a team earns for filing a record instead of claimingteam's illustrative units
$s_{\text{strong}},\ s_{\text{weak}}$: the chance a strong team's claim, a weak team's claim, survives the checkprobability
$\varphi_{\text{strong}},\ \varphi_{\text{weak}}$: the expected penalty a strong team, a weak team, faces for claimingteam's illustrative units

What Lean checks

Lean is a program that checks every step of a proof. "Checked in Lean" means the conclusion follows from the stated assumptions with no gap; it does not mean the assumptions describe your company. Here is what it checks for this lesson, each result exactly as strong as its statement.

Checked in Lean

With a free label, one award and a fair coin on ties, saying high gives a team strictly more than saying low, whatever the other team says, as long as the slot is worth something to it.

high_priority_strictly_dominates in ExpertiseScarcity.lean

Show the Lean statement

theorem high_priority_strictly_dominates (b : Rat) (hb : 0<b) (other : Bool) :
    priorityUtility b false other < priorityUtility b true other

A companion theorem, unique_pure_priority_equilibrium, adds that "both say high" is the only equilibrium among plans that do not flip coins. The dominance result is the stronger and simpler statement.

Checked in Lean

If the rival pitches only when strong, a strong team strictly prefers to pitch and a weak team strictly prefers to stay home exactly when the effort lies strictly inside the window.

strict_separating_equilibrium_threshold in ExpertiseScarcity.lean

Show the Lean statement

theorem strict_separating_equilibrium_threshold (pi pHigh pLow benefit burden : Rat) :
    strictSeparatingBestReplies pi pHigh pLow benefit burden ↔
    pLow*(1-pi*pHigh/2)*benefit < burden ∧
    burden < pHigh*(1-pi*pHigh/2)*benefit

What this does not prove: Lean checks the two inequalities and the formula for the chance of winning. Calling the result stable — neither team wants to change its rule — also needs the teams' ideas and the tests to be independent, a test that cannot be gamed, and a sponsor who keeps testing after guessing who is strong. Other stable outcomes are not ruled out. The worked numbers (15/16, −11/16, 31/8 and −25/64) are checked separately by high_type_enters_example, low_type_stays_example, separating_gate_profitable_example and separating_gate_loses_example.

Checked in Lean

If a record is worth something to a team, a strong team prefers claiming even when it must share, and a weak team prefers a record even when it would win alone, then 'strong teams claim, weak teams file a record' is the only equilibrium among plans that do not flip coins — including lopsided pairs where the two teams follow different rules.

unique_truthful_equilibrium in StrategicPitch.lean

Show the Lean statement

theorem unique_truthful_equilibrium (g : Game) (hv : Valid g)
    (hg : 0 < g.disclosureUtility)
    (hq : g.disclosureUtility <
      g.benefit*g.qQualified/2-g.fineQualified-g.claimBurden)
    (hu : g.benefit*g.qUnsupported-g.fineUnsupported-g.claimBurden <
      g.disclosureUtility)
    (first second : Strategy) :
    Equilibrium g first second ↔ first = truth ∧ second = truth

It rests on truthful_actions_strictly_dominant: each truthful choice is strictly best against every possible rival plan. Because of that, plans that mix choices at random cannot do better either; that last step is standard reasoning, not checked here. The worked numbers — 23/16, −35/16 and 1/8 for the teams, 93/32 for the company at a check cost of 1/2 and −19/32 at 4 — are baseline_private_utilities, baseline_net and overhead_loss.

Lean also checks the losing cases below, each as an exact value in the worked example: no_audit_unique and no_audit_net (no checks: everyone claims, gain 0), half_audit_equilibria (checks half the time: exactly two stable outcomes, both lopsided), false_accusations_lose, nondiscriminating_audit_loses, weak_enforcement_still_filters and economic_misalignment_loses.

What it means

A free priority label cannot work, and that is not a character flaw. Saying high is the best move for every team no matter what the others do. Asking people to be more honest about priorities is asking them to act against their own team. If labels are to mean something, they must cost something, or be checked, or both.

A cost can sort, but only in a window. Too little effort and weak ideas pitch anyway; too much and strong ones give up. The window depends on how good the test is and how much the slot is worth, so a pitch process tuned for one kind of request can be wrong for another. And sorting is not profit: in Figure 1, drag the project value down to 1 while leaving the effort alone. The teams still sort perfectly. The company now loses on every round of tests.

A good check can make the truth the best move for everyone. That is a strong result: it does not depend on guessing what the other team will do. But it asks for a lot, and each request is a way to lose.

The checks cost too much. Past about 3.4 per check, the company would do better with no review at all (Figure 2).
The check cannot tell strong from weak. If strong and weak claims are flagged equally often, no rule of this kind can strictly sort them (nondiscriminating_no_strict_separation). In the worked case everyone then claims and the company loses 1.
The check accuses the wrong people. If strong claims are wrongly flagged 3 times in 4, strong teams stop claiming. Everyone files a record, no project gets the slot, and the company loses 1/2.
Nobody checks. Everyone claims and the slot is a lottery: gain 0. Checking only half the time is stranger: there are exactly two stable outcomes, each with one team always claiming and the other telling the truth. The model does not say which one happens.
The record is not worth filing. If filing costs the team more than it earns, weak teams go silent and the lesson is lost. If it exactly breaks even, four stable outcomes survive, and some of them have no records.
The criterion is wrong. Keep everyone honest but reward the wrong thing — here, suppose the "strong" projects are actually worth 0 and the "weak" ones 8. The careful review then loses 63/32 while the unchecked lottery would have gained 2. A tidy process is not the same as a good decision.

One surprise is worth keeping. When penalties are announced but never enforced, everyone claims — the deterrent fails — yet the checks still filter which claims are eligible, and the company still gains 5/4 when checks are cheap. A rule that fails to deter can still help decide.

None of this needs an ACM by name. A capable local or federated arrangement allowed the same evidence, the same checks and the same rules would get exactly the same numbers. That is a design rule of every model in this series, stated on the research index, not a finding. What a shared owner can bring is the ability to run the check at all: comparable evidence across teams, people who can read it, and the standing to enforce the result.

What the model leaves out. Two teams, one slot, one round. Strengths and test results are independent. The check is honest and cannot be gamed. Nobody colludes, nobody appeals, nobody builds a reputation. Real priority systems have all of these. The model tells you which levers matter — the cost of a pitch, the quality of the check, the penalty, the value of the record — not where to set them.

Next: what the reviewer remembers

In this lesson, the reviewer's test was as good as it was ever going to be: it passed strong ideas 3 times in 4, full stop. But a reviewer who has seen the scanned-annex failure once should recognize it the second time. What is a record of failures worth to the next decision — and when does keeping it cost more than it saves? That is lesson 5.