[ocfnash]

I presume you've been looking at my presentation here http://olivernash.org/2019/07/06/coq-imo/index.html which I confess is quite concise; apologies if it is too terse.

Reusing the notation of my post, here's how the formula arises.

The argument based on counting cells that are either row/column good/bad requires the following of the parameter k:

  1. k-1 < r/m
  2. k-1 < c/n
  3. k−1 < cr/(c(m-1) + r(n-1))

These are equivalent to:

  1. k <= ceil r m
  2. k <= ceil c n
  3. k <= ceil cr (c(m-1) + r(n-1))

And so it is sufficient to have:

  k <= min (ceil r m) (ceil c n) (ceil cr (c(m-1) + r(n-1)))

We can then rearrange this to the headline formula by noting:

  * ceil r m = ceil (cr) (cm)
  * ceil c n = ceil (cr) (mr)

And then simplifying by repeatedly using the fact that for any x, y, z:

  * min (ceil x y) (ceil x z) = ceil x (max y z)

All this is of course in the Coq code. E.g., the last fact mentioned above is here: https://github.com/ocfnash/imo-coq/blob/f6d2e8337fadf00583fd...

[krapht]

Related: https://imo-grand-challenge.github.io/

[ocfnash]

Cool!

[meuk]

Thanks. I just don't understand how you arrived at

  k <= ceil cr (c(m-1) + r(n-1))

The rest is clear.

[ocfnash]

Oh I see. Here's how I got there (still using the terminology / notation of my original post).

Without knowing anything about k except that k-1 < r/m, I counted how many cells are column-bad for this value of k. By the pigeon-hole-principle argument in the post this is at most c(m-1)(k-1) cells. Similarly, and still knowing nothing about k except that k-1 < c/n, I count how many cells are row-bad for this value of k and see that it is at most r(n-1)(k-1). Combining these two I know that as long as we have k-1 < r/m and k-1 < c/n the number of cells that are either column-bad or row-bad (or both) is at most:

  * c(m-1)(k-1) + r(n-1)(k-1)

Since I want to be able to conclude that there is a cell that is neither column-bad nor row-bad, and since there are rc cells in total, I then further require that k is such that:

  * c(m-1)(k-1) + r(n-1)(k-1) < rc

(The point is that this is a strict inequality and so there must be a cell that is neither column-bad nor row-bad.)

And then solve this to get the formula for k. Of course when expositing it in the post, I _start_ with the formula which perhaps makes things seem mysterious at first, but I thought was efficient.

[meuk]

Ah, it makes total sense now! Thanks for taking the time to explain your thought process to a random stranger on the internet ;)

I'd say that the exposition in your post is very fitting for the purpose of proving it. The most elegant proofs are usually not the most enlightening.

[ocfnash]

You're welcome.