2510.20013

ivanisvili_xie.lean

import Mathlib.Data.Rat.Defs
import Init.Data.List.Basic
import Std.Tactic

/--
Verify the counterexample of Ivanisvili-Xie in https://arxiv.org/abs/2510.20013
Most of the codes are written by GPT-5 Pro & Codex.
-/

namespace NICD

/-- Cartesian power: all length-`n` lists over `vals`. -/
def cartesianPow (vals : List ℚ) : Nat → List (List ℚ)
| 0     => [[]]
| n+1   =>
  let tails := cartesianPow vals n
  List.foldr (fun tail acc => (List.map (fun v => v :: tail) vals) ++ acc) [] tails

-- Domains
def pm1     : List ℚ := [-1, 1]
def ternary : List ℚ := [-1, 0, 1]
def hypercube : List (List ℚ) := cartesianPow pm1 5
def erasures  : List (List ℚ) := cartesianPow ternary 5

/-- Sign on ℚ with sgn(0) = -1 (never occurs on {±1}^5 here). -/
def sgn (q : ℚ) : ℚ := if 0 < q then 1 else -1

-- The two Boolean functions on {±1}^5
def fLTF (x : List ℚ) : ℚ :=
  sgn (x[0]! - 3 * x[1]! + x[2]! - x[3]! + 3 * x[4]!)

def maj5 (x : List ℚ) : ℚ :=
  sgn (x[0]! + x[1]! + x[2]! + x[3]! + x[4]!)

-- Erasure model
def p : ℚ := 2/5
def probVal (q : ℚ) : ℚ :=
  if q = -1 then p/2 else
  if q = 0  then 1 - p else
  if q = 1  then p/2 else 0

def probVec (z : List ℚ) : ℚ :=
  List.foldl (fun s a => s * probVal a) (1 : ℚ) z

/-- Tiny rational absolute value to avoid extra notations. -/
def qabs (q : ℚ) : ℚ := if 0 ≤ q then q else -q

/-
  Multilinear extension via the Walsh identity:
    f̃(z) = (1/2^5) * Σ_{x ∈ {±1}^5} f(x) * Π_{i=0}^4 (1 + z_i x_i).
  No Fourier precomputation needed; avoid dot-syntax folds and indexing.
-/
def evalExt (g : List ℚ → ℚ) (z : List ℚ) : ℚ :=
  let denom : ℚ := (2 : ℚ) ^ (5 : Nat)
  (List.foldl
     (fun S x =>
        let term :=
          List.foldl
            (fun acc (zx : ℚ × ℚ) => acc * (1 + zx.fst * zx.snd))
            (1 : ℚ)
            (List.zip z x)
        S + g x * term)
     (0 : ℚ) hypercube) / denom

/-- Φ_p(g) = E_z | f̃(z) | under the erasure law. -/
def phi (g : List ℚ → ℚ) : ℚ :=
  List.foldl (fun s z => s + qabs (evalExt g z) * probVec z) (0 : ℚ) erasures

def phi_f   : ℚ := phi fLTF
def phi_maj : ℚ := phi maj5

#eval phi_f
#eval phi_maj
#eval phi_f - phi_maj

-- Close goals with the VM evaluator (robust for list folds)
example : phi_f   = (2689 : ℚ) / 6250  := by native_decide
example : phi_maj = (5363 : ℚ) / 12500 := by native_decide
example : phi_f > phi_maj              := by native_decide

end NICD