Common Utilities for LCS Games

This module provides technical lemmas and definitions for signs, indicator functions, and basic properties of the outcome space $\mathbb{F}_2$.

Key Definitions

• observableSign: Returns $1$ if $a=0$ or $-1$ if $a=1$.

Key Lemmas

• sign_mul: The product of signs corresponds to the sum in $\mathbb{F}_2$.
• sign_indicator: Relates the sign-based expression $(1/2)(1 + (-1)^{b+s})$ to the Kronecker delta.

theorem fin2_eq_zero_or_one (a : Fin 2) : a = 0 ∨ a = 1

theorem sign_mul (a b : Fin 2) : (-1) ^ ↑a * (-1) ^ ↑b = (-1) ^ ↑(a + b)

theorem sign_indicator (b s : Fin 2) : 1 / 2 + 1 / 2 * (-1) ^ ↑b * (-1) ^ ↑s = if s = b then 1 else 0

Arithmetic helper: the sign factor $(1/2)(1 + (-1)^b * (-1)^s)$ equals the indicator s = b.

def observableSign (a : Fin 2) : ℂ

Equations

• observableSign a = if a = 0 then 1 else -1

theorem sign_fin2_sq (x : Fin 2) : (-1) ^ ↑x * (-1) ^ ↑x = 1

theorem prod_sign_eq_sum_sign_aux {G : LCSLayout} {i : Fin G.r} (x : Assignment G i) (s : Finset ↥(G.V i)) : ∏ j ∈ s, (-1) ^ ↑(x j) = (-1) ^ ↑(∑ j ∈ s, x j)

theorem prod_sign_eq_sum_sign {G : LCSLayout} (i : Fin G.r) (x : Assignment G i) : ∏ j ∈ (G.V i).attach, (-1) ^ ↑(x j) = (-1) ^ ↑(∑ j : ↥(G.V i), x j)

theorem finset_filter_eq_inter_univ_filter {α : Type u_1} [Fintype α] [DecidableEq α] (S : Finset α) (p : α → Prop) [DecidablePred p] : Finset.filter p S = S ∩ Finset.filter p Finset.univ