HH vs HT (https://twitter.com/littmath/status/1769044719034647001)

00_HH_vs_HT.md

Problem: https://twitter.com/littmath/status/1769044719034647001

Flip a fair coin 100 times—it gives a sequence of heads (H) and tails (T). For each HH in the sequence of flips, Alice gets a point; for each HT, Bob does, so e.g. for the sequence THHHT Alice gets 2 points and Bob gets 1 point. Who is most likely to win?

Proofs:

1. https://twitter.com/llllvvuu/status/1769629337953923403
2. https://x.com/alexselby1770/status/1769795987344638033
3. https://twitter.com/RadishHarmers/status/1770217473716932647
4. https://x.com/RadishHarmers/status/1771368007174168604?s=20

Generating Functions

Extension of: https://x.com/alexselby1770/status/1770269732588888466

Number of games Bob wins

$$f(x) = \dfrac{x\left(1 + x + 2x^2 + (x - 1)\sqrt{1 + \frac{4x^3}{x - 1}}\right)}{2 (x - 1)^2\left(1 + \frac{4x^3}{x - 1}\right)}$$

• TODO: Rewrite as quadratic equation
• TODO: Substitute $f(x) = \sum a_n x^n$ into quadratic equation and derive linear recurrence relation for $a_n$ by aligning coefficients of $x^n$

Number of games Alice wins

$$f(x) = \dfrac{(x + 1) \sqrt{1 + \frac{4x^3}{x - 1}} - 2 x^2 - x - 1}{2 (x - 1)\left(1 + \frac{4x^3}{x - 1}\right)}$$

• TODO: Rewrite as quadratic equation
• TODO: Substitute $f(x) = \sum a_n x^n$ into quadratic equation and derive linear recurrence relation for $a_n$ by aligning coefficients of $x^n$

Number of more games Bob wins

$$f(x) = \dfrac{\left(1+\frac{4x^3}{x-1}\right)^{-\frac{1}{2}} - 1}{2(1 - x)}$$

$$(4x^3 + x - 1)(1 - x)^2 f(x)^2 + (4x^3 + x - 1)(1 - x)f(x) + x^3 = 0$$

• TODO: Substitute $f(x) = \sum a_n x^n$ and derive linear recurrence relation for $a_n$ by aligning coefficients of $x^n$

Number of games tied

$$f(x) = \dfrac{(1 + 2 x)\left(1 + \frac{4 x^3}{x - 1}\right)^{-\frac{1}{2}} + 1}{2 (1 - x)}$$

$$(-1 + x)^2 (-1 + x + 4 x^3) f(x)^2 + (-1 + x) (-1 + 2 x) (1 + x + 2 x^2) f(x) + x = 0$$

• TODO: Substitute $f(x) = \sum a_n x^n$ and derive linear recurrence relation for $a_n$ by aligning coefficients of $x^n$

What's incomplete about the "autocorrelation" intuition?

This intuition basically says "Alice has larger average win margins, but total win margin is the same for Alice and Bob, so Alice wins fewer times".

"Alice has larger average win margins" is an unproven conjecture, extrapolated from a few data points (e.g. there are win margins between n/2 and n for Alice, but not for Bob).

It turns out this skew is not really noticeable outside of the tails:

How do we know the center is not skewed the other way? We need an actual proof here.

HH_vs_HT.c

#include <assert.h>
#include <stdint.h>
#include <stdio.h>
#include <string.h>

#define SWAP(x, y, T)                                                          \
  do {                                                                         \
    T SWAP = x;                                                                \
    x = y;                                                                     \
    y = SWAP;                                                                  \
  } while (0)

#define MAX_FLIPS 65

/**
 * @param flips - At most 65 due to overflow
 * @param[out] alice - Must be allocated at least `flips` `uint64_t`s
 * @param[out] bob - Must be allocated at least `flips` `uint64_t`s
 * @param[in, out] buf - Must be allocated at least `8 * (flips + 1)` `uint64_t`s.
 */
void count(uint8_t flips, uint64_t *alice, uint64_t *bob, uint64_t *buf) {
  assert(flips <= MAX_FLIPS);
  flips++; // HACK: bump memory offset
  uint64_t *T_prev = &buf[flips], *T = &buf[5 * flips];
  uint64_t *H_prev = &buf[3 * flips], *H = &buf[7 * flips];
  memset(buf, 0, 8 * flips * sizeof(uint64_t));
  *T = 1;
  for (uint8_t n = 1; n < flips; n++) {
    alice[n - 1] = bob[n - 1] = 0;
    SWAP(H_prev, H, uint64_t *);
    SWAP(T_prev, T, uint64_t *);
    for (int8_t d = -n; d < 0; d++) {
      assert(1 - d <= flips); // bounds check
      T[d] = T_prev[d] + H_prev[d - 1];
      H[d] = T_prev[d] + H_prev[d + 1];
      alice[n - 1] += T[d] + H[d];
    }
    assert(flips > 1); // bounds check
    T[0] = T_prev[0] + H_prev[-1];
    H[0] = T_prev[0] + H_prev[1];
    for (int8_t d = 1; d <= n / 2; d++) {
      assert(d + 1 < flips); // bounds check
      T[d] = T_prev[d] + H_prev[d - 1];
      H[d] = T_prev[d] + H_prev[d + 1];
      bob[n - 1] += T[d] + H[d];
    }
  }
}

int main() {
  static uint64_t alice[MAX_FLIPS], bob[MAX_FLIPS], buf[8 * (MAX_FLIPS + 1)];
  count(MAX_FLIPS, alice, bob, buf);
  for (uint8_t i = 0; i < MAX_FLIPS; i++) {
    printf("%2d flips: Bob %24llu - Alice %24llu\n", i + 1, bob[i], alice[i]);
  }
  return 0;
}

HH_vs_HT.lean

import Mathlib

def alice {n : ℕ} (x : Std.BitVec n.succ) : ℕ :=
  Finset.card <| (Finset.range n).filter (fun i ↦ x.getLsb i ∧ x.getLsb i.succ)

def bob {n : ℕ} (x : Std.BitVec n.succ) : ℕ :=
  Finset.card <| (Finset.range n).filter (fun i ↦ x.getLsb i ∧ ¬x.getLsb i.succ)

def alice_win {n : ℕ} (x : Std.BitVec n.succ) : Prop :=
  bob x < alice x

def alice_win' {n : ℕ} (x : Std.BitVec n.succ) : Prop :=
  bob x < alice x ∨ (bob x == alice x ∧ ¬x.getLsb n)

def bob_win {n : ℕ} (x : Std.BitVec n.succ) : Prop :=
  alice x < bob x

instance {n : ℕ} (x : Std.BitVec n.succ) : Decidable (alice_win x) := by
  unfold alice_win; infer_instance

instance {n : ℕ} (x : Std.BitVec n.succ) : Decidable (alice_win' x) := by
  unfold alice_win'; infer_instance

instance {n : ℕ} (x : Std.BitVec n.succ) : Decidable (bob_win x) := by
  unfold bob_win; infer_instance

def alice_wins (n : ℕ) : ℕ :=
  Finset.card
    <| (Finset.range (2 ^ n.succ)).filter
    <| (fun i ↦ alice_win (Std.BitVec.ofNat n.succ i))

def alice_wins' (n : ℕ) : ℕ :=
  Finset.card
    <| (Finset.range (2 ^ n.succ)).filter
    <| (fun i ↦ alice_win' (Std.BitVec.ofNat n.succ i))

def bob_wins (n : ℕ) : ℕ :=
  Finset.card
    <| (Finset.range (2 ^ n.succ)).filter
    <| (fun i ↦ bob_win (Std.BitVec.ofNat n.succ i))

#eval (List.range 10).map alice_wins
#eval (List.range 10).map alice_wins'
#eval (List.range 10).map bob_wins

proof_wanted key_lemma (n : ℕ) : alice_wins' n = (bob_wins n).succ
proof_wanted bob_advantage (n : ℕ) : alice_wins n.succ.succ < bob_wins n.succ.succ