This post is about a formalization of an simple argument Jasper Bernes explained to me yesterday which proves that primitive accumulation produces a surplus population.

Marx in Capital explains surplus population as resulting from the introduction of labor saving technology, which reduces the need for workers (i.e., “automation”.) But, there is an additional source of surplus population, which is primitive accumulation: people formerly living off the land by a non-capitalist mode of production, who are dispossessed.

Here we imagine that after dispossession, these people are put to work using the same techniques of production they used previously¹.

Say one “unit” of land is what is required with the given technique to provide 1 “subsistence basket” for one person, and further assume that said unit of land is being used maximally.

We claim that seizing $L$ units of land (and concurrently dispossessing $L$ people who used that land) and working the land according to the existing technique in a profitable way, results in a positive number of people who will not be employed.

The argument is simple. Say $E$ people are employed after the enclosure. They must be producing $> E$ subsistence baskets since there is a profit, and their labor power costs $E$ subsistence baskets. Producing 1 subsistence basket requires 1 unit of land, so they are using $> E$ units of land, i.e., $L > E$. In words, the number of people employed is less than the number of units of land being worked. $L$ is also equal to the number of people dispossessed, so there are more people who were dispossessed than are being employed. I.e., there is a surplus population.

To put it another way: the people employed after dispossession have to work longer than they did before if they are going to do a surplus. If they do that, they will have to use more than 1 unit of land each. Which means we need more units of land than people, and therefore there will be a surplus population. The people employed after the enclosure in the extended part of their working day are doing the work the surplus population was doing previously.

I formalized this argument in Lean using Codex. Of course most of the “truth content” is in the modelling, and cannot be formalized, but I share it in case it is of interest. The proof is just unfolding definitions and chaining (in)equalities:

/-- The core argument: `employed < output ≤ land = displaced`. -/
theorem positive_profit_produces_surplus_population {s : State}
    (feasible : Feasible s) (profit : Profitable s) :
    0 < s.surplusPopulation := by
  have land := feasible.landCapacity
  unfold Profitable at profit
  unfold State.surplusPopulation State.displaced
  omega

structure Feasible (s : State) : Prop where
  landCapacity : s.output ≤ s.land
  laborCapacity : s.output ≤ s.employed * s.workday
  subsistence : s.employed ≤ s.output

def Profitable (s : State) : Prop := s.employed < s.output

def State.surplusPopulation (s : State) : Nat := s.displaced - s.employed

def State.displaced (s : State) : Nat := s.land

structure State where
  land : Nat
  employed : Nat
  workday : Nat
  output : Nat