EconCSLib.SocialChoice.FairDivision.Divisible.CutAndChoose

The cut-and-choose protocol for 2-agent divisible fair division.

Protocol

1. The cutter (agent 0) cuts the cake at a position t ∈ [0,1], producing two pieces:
   • Left piece: [0, t]
   • Right piece: (t, 1]
2. The chooser (agent 1) picks whichever piece they value more (ties go to the left).
3. The cutter receives the remaining piece.

Main definitions

• cutAndChooseAlloc μ t — allocation produced by the protocol at cut point t ∈ [0,1]
• IsFairCutPoint μ t — the cut is "fair for the cutter": μ 0 (Iic t) = μ 0 (Ioi t)

Main results

• cutAndChooseAlloc_isAllocation — the output is always a valid complete partition
• chooser_isEnvyFree — the chooser (agent 1) never envies the cutter, regardless of the cut point (they always receive their preferred half)
• cutter_isEnvyFree_of_fair — the cutter (agent 0) does not envy the chooser at a fair cut (the two halves are equal for the cutter, so they are indifferent)
• cutAndChoose_isEnvyFree — both agents are EF at any fair cut point
• fairCutPoint_exists — for finite non-atomic μ 0, a fair cut always exists (via the shared unit-interval IVT lemma DubinsSpanier.cut_exists)
• cutAndChoose_ef_exists — EF allocation always exists for 2 agents (corollary: combine fairCutPoint_exists with cutAndChoose_isEnvyFree)

Relationship to ef_exists_two_agents

ef_exists_two_agents in EnvyFree.lean proves EF existence directly as an existential. This file adds structure: the protocol is an explicit function parametrized by the cut point, and the two fairness guarantees (chooser and cutter) are proved separately. The key separation is that chooser_isEnvyFree holds for any cut — the chooser's guarantee does not depend on the cut being fair.

References

• Steinhaus, "The Problem of Fair Division" (1948) — original fair division paper
• Robertson–Webb, Cake-Cutting Algorithms (1998), Ch. 1
• Nisan et al., Algorithmic Game Theory, Ch. 13

Protocol definition

noncomputable def SocialChoice.FairDivision.Divisible.cutAndChooseAlloc (μ : Fin 2 → MeasureTheory.Measure ↑unitInterval) (t : ↑unitInterval) : Allocation (Fin 2) ↑unitInterval

The cut-and-choose allocation at cut point t ∈ [0,1].

The chooser (agent 1) receives the half they value more:

• If μ 1 (Iic t) ≥ μ 1 (Ioi t), agent 1 takes [0, t]; agent 0 gets (t, 1].
• Otherwise, agent 1 takes (t, 1]; agent 0 gets [0, t].

The allocation is noncomputable because measures are noncomputable.

Equations

• SocialChoice.FairDivision.Divisible.cutAndChooseAlloc μ t i = if (μ 1) (Set.Iic t) ≥ (μ 1) (Set.Ioi t) then if i = 0 then Set.Ioi t else Set.Iic t else if i = 0 then Set.Iic t else Set.Ioi t

def SocialChoice.FairDivision.Divisible.IsFairCutPoint (μ : Fin 2 → MeasureTheory.Measure ↑unitInterval) (t : ↑unitInterval) : Prop

A cut point t is fair (for the cutter, agent 0) if agent 0's measure is split equally: μ 0 [0, t] = μ 0 (t, 1].

At a fair cut the cutter is indifferent between the two halves, so they cannot envy whichever piece the chooser selects.

Equations

• SocialChoice.FairDivision.Divisible.IsFairCutPoint μ t = ((μ 0) (Set.Iic t) = (μ 0) (Set.Ioi t))

Simp lemmas for agent-specific pieces

@[simp]

theorem SocialChoice.FairDivision.Divisible.cutAndChooseAlloc_zero (μ : Fin 2 → MeasureTheory.Measure ↑unitInterval) (t : ↑unitInterval) : cutAndChooseAlloc μ t 0 = if (μ 1) (Set.Iic t) ≥ (μ 1) (Set.Ioi t) then Set.Ioi t else Set.Iic t

Cutter (agent 0) receives the right piece when the chooser prefers left, and the left piece otherwise.

@[simp]

theorem SocialChoice.FairDivision.Divisible.cutAndChooseAlloc_one (μ : Fin 2 → MeasureTheory.Measure ↑unitInterval) (t : ↑unitInterval) : cutAndChooseAlloc μ t 1 = if (μ 1) (Set.Iic t) ≥ (μ 1) (Set.Ioi t) then Set.Iic t else Set.Ioi t

Chooser (agent 1) receives the left piece if they prefer it, the right piece otherwise.

The output is always a valid partition

theorem SocialChoice.FairDivision.Divisible.cutAndChooseAlloc_isAllocation (μ : Fin 2 → MeasureTheory.Measure ↑unitInterval) (t : ↑unitInterval) : IsAllocation (cutAndChooseAlloc μ t)

For any cut point t, the cut-and-choose allocation is a complete measurable partition of [0,1] into two pieces. This holds regardless of whether the cut is fair.

Chooser guarantee

theorem SocialChoice.FairDivision.Divisible.chooser_isEnvyFree (μ : Fin 2 → MeasureTheory.Measure ↑unitInterval) (t : ↑unitInterval) : (MeasureValuation μ).val 1 (cutAndChooseAlloc μ t 0) ≤ (MeasureValuation μ).val 1 (cutAndChooseAlloc μ t 1)

The chooser (agent 1) never envies the cutter, regardless of the cut point.

Since agent 1 selects whichever piece they value more, their own piece is always at least as valuable as the cutter's piece. No fairness condition on the cut is needed.

This is the key asymmetry of cut-and-choose: the chooser's guarantee is unconditional; only the cutter's guarantee depends on the cut being fair.

Cutter guarantee at fair cut

theorem SocialChoice.FairDivision.Divisible.cutter_isEnvyFree_of_fair (μ : Fin 2 → MeasureTheory.Measure ↑unitInterval) (t : ↑unitInterval) (hfair : IsFairCutPoint μ t) : (MeasureValuation μ).val 0 (cutAndChooseAlloc μ t 1) ≤ (MeasureValuation μ).val 0 (cutAndChooseAlloc μ t 0)

The cutter (agent 0) does not envy the chooser at a fair cut.

If the cut point t satisfies IsFairCutPoint μ t, then agent 0 values both halves equally. Regardless of which half the chooser takes, the cutter is indifferent.

Combined EF

theorem SocialChoice.FairDivision.Divisible.cutAndChoose_isEnvyFree (μ : Fin 2 → MeasureTheory.Measure ↑unitInterval) (t : ↑unitInterval) (hfair : IsFairCutPoint μ t) : IsEnvyFree (MeasureValuation μ) (cutAndChooseAlloc μ t)

Both agents are envy-free at any fair cut point.

This combines chooser_isEnvyFree (unconditional) and cutter_isEnvyFree_of_fair (requires fair cut) to give the full IsEnvyFree predicate for both agents.

Fair cut existence

theorem SocialChoice.FairDivision.Divisible.fairCutPoint_exists (μ : Fin 2 → MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsFiniteMeasure (μ 0)] [MeasureTheory.NoAtoms (μ 0)] : ∃ (t : ↑unitInterval), IsFairCutPoint μ t

A fair cut always exists for finite non-atomic μ 0 on [0,1].

This is the c = μ([0,1])/2 case of DubinsSpanier.cut_exists.

EF existence corollary

theorem SocialChoice.FairDivision.Divisible.cutAndChoose_ef_exists (μ : Fin 2 → MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsFiniteMeasure (μ 0)] [MeasureTheory.NoAtoms (μ 0)] : ∃ (A : Allocation (Fin 2) ↑unitInterval), IsAllocation A ∧ IsEnvyFree (MeasureValuation μ) A

EF allocations always exist for 2 agents with non-atomic finite measures (via cut-and-choose).

This recovers ef_exists_two_agents from EnvyFree.lean as a corollary: fairCutPoint_exists gives a cut point tstar where agent 0's measure is halved, and cutAndChoose_isEnvyFree gives EF at any fair cut.

theorem SocialChoice.FairDivision.Divisible.cutAndChoose_exists_envyFree_allocation (M : MeasureInstance (Fin 2) ↑unitInterval) [MeasureTheory.IsFiniteMeasure (M.measure 0)] [MeasureTheory.NoAtoms (M.measure 0)] : ∃ (A : Allocation (Fin 2) ↑unitInterval), IsAllocation A ∧ M.IsEnvyFree A

Bundled-instance form of cut-and-choose envy-free existence.

noncomputable def SocialChoice.FairDivision.Divisible.cutAndChooseRule (M : MeasureInstance (Fin 2) ↑unitInterval) [MeasureTheory.IsFiniteMeasure (M.measure 0)] [MeasureTheory.NoAtoms (M.measure 0)] : { A : Allocation (Fin 2) ↑unitInterval // M.feasible A }

Cut-and-choose as a rule on bundled two-agent measure instances.

Equations

• SocialChoice.FairDivision.Divisible.cutAndChooseRule M = ⟨SocialChoice.FairDivision.Divisible.cutAndChooseAlloc M.measure (Classical.choose ⋯), ⋯⟩

theorem SocialChoice.FairDivision.Divisible.cutAndChooseRule_isEnvyFree (M : MeasureInstance (Fin 2) ↑unitInterval) [MeasureTheory.IsFiniteMeasure (M.measure 0)] [MeasureTheory.NoAtoms (M.measure 0)] : M.IsEnvyFree ↑(cutAndChooseRule M)

The bundled cut-and-choose rule is envy-free.