/-
  Counterexample to Ziegler's cross-polytope conjecture for simplicial 0/1-polytopes — kernel-attested.
  Independent confirmation of Kaibel & Pokutta (2026), arXiv:2606.31640 (Theorem 3.1). P = conv(V) for the 14
  vertices `V` ⊂ {0,1}^7 is a simplicial 7-polytope with 2·7 vertices that is NOT centrally symmetric.

  The counterexample is decided in full by exact rational arithmetic (scripts/verify_ziegler_counterexample.py:
  dim 7; 136 supporting facets each an affinely-independent 6-simplex; every ridge in exactly 2 facets; not
  centrally symmetric). This file has the Lean 4.31 kernel INDEPENDENTLY re-decide (plain `decide`,
  report-only) the parts that fit its reduction budget:
    • ziegler_dim_notsym : rank[1|V]=8 (dim 7, via a nonzero 8×8 minor) AND V is balanced (each coordinate sums
      to 7, so the only possible centre is (½,…,½)) AND four vertices lack their cube antipode 1−v — hence P is
      not centrally symmetric.
    • ziegler_supporting : each of the 136 `facets` is cut out by a supporting hyperplane `normals`ₖ that
      vanishes on its 7 vertices and is strictly negative on the other 7 — so each facet has exactly 7 vertices.
    • ziegler_closed : the 136 facets form a CLOSED pseudomanifold — for every facet and every one of its 7
      ridges (drop one vertex) a `partner` facet shares that ridge; with each facet a genuine simplex facet this
      forces the list to be ALL facets (∂P is a connected pseudomanifold), so P is simplicial.
  Affine-independence of the 136 facets (that each is a genuine 6-simplex) is certified by the exact-rational
  leg — 136 nonzero determinants — which exceeds the kernel's `decide` budget.

  Plain `decide` — no `native_decide`, no `sorry`. Report-only: the kernel observes; nothing sets
  kernel_verified.
-/
set_option maxHeartbeats 0
set_option maxRecDepth 1000000

def dot : List Int → List Int → Int
  | a :: as, b :: bs => a * b + dot as bs
  | _, _ => 0

def detN : Nat → List (List Int) → Int
  | 0, _ => 1
  | (m+1), M => match M with
    | [] => 0
    | row :: rest => (List.range (m+1)).foldl (fun acc j =>
        acc + (if j % 2 == 0 then (1:Int) else -1) * (row.getD j 0) * detN m (rest.map (fun r => r.eraseIdx j))) 0

def V : List (List Int) := [[0, 0, 1, 0, 1, 1, 0], [1, 0, 1, 1, 1, 0, 1], [1, 0, 0, 0, 1, 0, 0], [1, 0, 0, 1, 0, 1, 0], [0, 1, 1, 1, 0, 0, 0], [1, 1, 0, 0, 0, 0, 1], [0, 0, 1, 0, 0, 0, 1], [0, 0, 0, 1, 1, 0, 0], [0, 1, 0, 0, 0, 1, 0], [1, 0, 0, 1, 1, 1, 1], [1, 1, 0, 1, 1, 1, 0], [0, 1, 1, 0, 1, 0, 1], [1, 1, 1, 0, 0, 1, 1], [0, 1, 1, 1, 0, 1, 1]]
def facets : List (List Nat) := [[0, 1, 2, 3, 4, 6, 7], [0, 1, 2, 3, 4, 6, 12], [0, 1, 2, 3, 4, 7, 10], [0, 1, 2, 3, 4, 10, 12], [0, 1, 2, 3, 6, 7, 9], [0, 1, 2, 3, 6, 9, 12], [0, 1, 2, 3, 7, 9, 10], [0, 1, 2, 3, 9, 10, 12], [0, 1, 2, 4, 6, 7, 11], [0, 1, 2, 4, 6, 11, 12], [0, 1, 2, 4, 7, 10, 11], [0, 1, 2, 4, 10, 11, 12], [0, 1, 2, 6, 7, 9, 11], [0, 1, 2, 6, 9, 11, 12], [0, 1, 2, 7, 9, 10, 11], [0, 1, 2, 9, 10, 11, 12], [0, 1, 3, 4, 6, 7, 13], [0, 1, 3, 4, 6, 12, 13], [0, 1, 3, 4, 7, 10, 13], [0, 1, 3, 4, 10, 12, 13], [0, 1, 3, 6, 7, 9, 13], [0, 1, 3, 6, 9, 12, 13], [0, 1, 3, 7, 9, 10, 13], [0, 1, 3, 9, 10, 12, 13], [0, 1, 4, 6, 7, 11, 13], [0, 1, 4, 6, 11, 12, 13], [0, 1, 4, 7, 10, 11, 13], [0, 1, 4, 10, 11, 12, 13], [0, 1, 6, 7, 9, 11, 13], [0, 1, 6, 9, 11, 12, 13], [0, 1, 7, 9, 10, 11, 13], [0, 1, 9, 10, 11, 12, 13], [0, 2, 3, 4, 6, 7, 8], [0, 2, 3, 4, 6, 8, 12], [0, 2, 3, 4, 7, 8, 10], [0, 2, 3, 4, 8, 10, 12], [0, 2, 3, 6, 7, 8, 9], [0, 2, 3, 6, 8, 9, 12], [0, 2, 3, 7, 8, 9, 10], [0, 2, 3, 8, 9, 10, 12], [0, 2, 4, 6, 7, 8, 11], [0, 2, 4, 6, 8, 11, 12], [0, 2, 4, 7, 8, 10, 11], [0, 2, 4, 8, 10, 11, 12], [0, 2, 5, 6, 8, 9, 11], [0, 2, 5, 6, 8, 9, 12], [0, 2, 5, 6, 8, 11, 12], [0, 2, 5, 6, 9, 11, 12], [0, 2, 5, 8, 9, 11, 12], [0, 2, 6, 7, 8, 9, 11], [0, 2, 7, 8, 9, 10, 11], [0, 2, 8, 9, 10, 11, 12], [0, 3, 4, 6, 7, 8, 13], [0, 3, 4, 6, 8, 12, 13], [0, 3, 4, 7, 8, 10, 13], [0, 3, 4, 8, 10, 12, 13], [0, 3, 6, 7, 8, 9, 13], [0, 3, 6, 8, 9, 12, 13], [0, 3, 7, 8, 9, 10, 13], [0, 3, 8, 9, 10, 12, 13], [0, 4, 6, 7, 8, 11, 13], [0, 4, 6, 8, 11, 12, 13], [0, 4, 7, 8, 10, 11, 13], [0, 4, 8, 10, 11, 12, 13], [0, 5, 6, 8, 9, 11, 12], [0, 6, 7, 8, 9, 11, 13], [0, 6, 8, 9, 11, 12, 13], [0, 7, 8, 9, 10, 11, 13], [0, 8, 9, 10, 11, 12, 13], [1, 2, 3, 4, 5, 6, 7], [1, 2, 3, 4, 5, 6, 12], [1, 2, 3, 4, 5, 7, 10], [1, 2, 3, 4, 5, 10, 12], [1, 2, 3, 5, 6, 7, 9], [1, 2, 3, 5, 6, 9, 12], [1, 2, 3, 5, 7, 9, 10], [1, 2, 3, 5, 9, 10, 12], [1, 2, 4, 5, 6, 7, 11], [1, 2, 4, 5, 6, 11, 12], [1, 2, 4, 5, 7, 10, 11], [1, 2, 4, 5, 10, 11, 12], [1, 2, 5, 6, 7, 9, 11], [1, 2, 5, 6, 9, 11, 12], [1, 2, 5, 7, 9, 10, 11], [1, 2, 5, 9, 10, 11, 12], [1, 3, 4, 5, 6, 7, 13], [1, 3, 4, 5, 6, 12, 13], [1, 3, 4, 5, 7, 9, 10], [1, 3, 4, 5, 7, 9, 13], [1, 3, 4, 5, 9, 10, 13], [1, 3, 4, 5, 10, 12, 13], [1, 3, 4, 7, 9, 10, 13], [1, 3, 5, 6, 7, 9, 13], [1, 3, 5, 6, 9, 12, 13], [1, 3, 5, 9, 10, 12, 13], [1, 4, 5, 6, 7, 11, 13], [1, 4, 5, 6, 11, 12, 13], [1, 4, 5, 7, 9, 10, 13], [1, 4, 5, 7, 10, 11, 13], [1, 4, 5, 10, 11, 12, 13], [1, 5, 6, 7, 9, 11, 13], [1, 5, 6, 9, 11, 12, 13], [1, 5, 7, 9, 10, 11, 13], [1, 5, 9, 10, 11, 12, 13], [2, 3, 4, 5, 6, 7, 8], [2, 3, 4, 5, 6, 8, 12], [2, 3, 4, 5, 7, 8, 10], [2, 3, 4, 5, 8, 10, 12], [2, 3, 5, 6, 7, 8, 9], [2, 3, 5, 6, 8, 9, 12], [2, 3, 5, 7, 8, 9, 10], [2, 3, 5, 8, 9, 10, 12], [2, 4, 5, 6, 7, 8, 11], [2, 4, 5, 6, 8, 11, 12], [2, 4, 5, 7, 8, 10, 11], [2, 4, 5, 8, 10, 11, 12], [2, 5, 6, 7, 8, 9, 11], [2, 5, 7, 8, 9, 10, 11], [2, 5, 8, 9, 10, 11, 12], [3, 4, 5, 6, 7, 8, 13], [3, 4, 5, 6, 8, 12, 13], [3, 4, 5, 7, 8, 10, 13], [3, 4, 5, 7, 9, 10, 13], [3, 4, 5, 8, 10, 12, 13], [3, 5, 6, 7, 8, 9, 13], [3, 5, 6, 8, 9, 12, 13], [3, 5, 7, 8, 9, 10, 13], [3, 5, 8, 9, 10, 12, 13], [4, 5, 6, 7, 8, 11, 13], [4, 5, 6, 8, 11, 12, 13], [4, 5, 7, 8, 10, 11, 13], [4, 5, 8, 10, 11, 12, 13], [5, 6, 7, 8, 9, 11, 13], [5, 6, 8, 9, 11, 12, 13], [5, 7, 8, 9, 10, 11, 13], [5, 8, 9, 10, 11, 12, 13]]
def normals : List (List Int) := [[1, 1, -6, 4, 1, -2, -3, -5], [-1, 3, -2, 4, -1, -2, -1, -3], [-5, 3, -2, 4, 3, 2, -1, -7], [-1, 1, 0, 1, 0, 0, 0, -1], [0, 0, -1, 0, 0, 0, 0, 0], [-3, 4, -6, 2, -3, -1, 2, 1], [-5, 2, -3, 1, 2, 3, 1, -3], [-8, 6, -2, 3, -1, 2, 3, -2], [-1, -1, -2, 4, -1, 2, -5, -3], [-1, 1, 0, 2, -1, 0, -1, -1], [-7, 1, 2, 4, 1, 6, -3, -5], [-5, 3, 2, 4, -1, 2, -1, -3], [-2, -2, -4, -1, -2, 4, -1, 3], [-5, 2, -3, 1, -5, 3, 1, 4], [-1, 0, 0, 0, 0, 1, 0, 0], [-10, 4, 1, 2, -3, 6, 2, 1], [-3, -3, -6, 4, 5, -2, 1, -1], [-3, 1, -2, 4, 1, -2, 1, -1], [-9, -1, -2, 4, 7, 2, 3, -3], [-3, 1, 0, 2, 1, 0, 1, -1], [-3, -3, -6, 2, 4, -1, 2, 1], [-6, 1, -5, 4, 1, -2, 4, 2], [-8, -1, -2, 3, 6, 2, 3, -2], [-11, 3, -1, 5, 3, 1, 5, -1], [-5, -5, -2, 4, 3, 2, -1, 1], [-1, 0, 0, 1, 0, 0, 0, 0], [-11, -3, 2, 4, 5, 6, 1, -1], [-7, 1, 2, 4, 1, 2, 1, -1], [-5, -5, -3, 1, 2, 3, 1, 4], [-8, -1, -2, 3, -1, 2, 3, 5], [-10, -3, 1, 2, 4, 6, 2, 1], [-13, 1, 2, 4, 1, 5, 4, 2], [3, -1, -2, 0, -1, -2, -1, -3], [3, 3, -2, 4, -5, -6, -1, -7], [0, 0, 0, 0, 0, 0, 0, -1], [-3, 5, 2, 4, -3, -2, 1, -9], [4, -3, -6, -5, -3, -1, 2, 1], [1, 1, -5, -3, -6, -2, 4, 2], [-1, -1, -2, -4, -1, 2, 3, -2], [-4, 3, -1, -2, -4, 1, 5, -1], [1, -1, 0, 0, -1, 0, -1, -1], [1, 1, 2, 4, -7, -2, -3, -5], [-1, -1, 2, 0, -1, 2, -1, -3], [-5, 3, 6, 4, -5, 2, -1, -7], [0, -1, -1, -2, -3, 1, 1, 2], [0, 0, -1, -1, -2, 0, 1, 1], [0, 0, 0, 0, -1, 0, 0, 0], [-1, 0, -1, -1, -3, 1, 1, 2], [-1, 0, 0, -1, -2, 1, 1, 1], [2, -5, -3, -6, -5, 3, 1, 4], [-3, -3, 1, -5, -3, 6, 2, 1], [-6, 1, 2, -3, -6, 5, 4, 2], [1, -3, -2, 0, 1, -2, 1, -1], [-1, -1, -2, 4, -1, -6, 3, -3], [-1, -1, 0, 0, 1, 0, 1, -1], [-7, 1, 2, 4, 1, -2, 5, -5], [1, -6, -5, -3, 1, -2, 4, 2], [-2, -2, -4, -1, -2, -3, 6, 3], [-4, -4, -1, -2, 3, 1, 5, -1], [-1, 0, 0, 0, 0, 0, 1, 0], [0, -1, 0, 0, 0, 0, 0, 0], [-3, -3, 2, 4, -3, -2, 1, -1], [-3, -3, 2, 0, 1, 2, 1, -1], [-9, -1, 6, 4, -1, 2, 3, -3], [-1, -1, -1, -2, -4, 1, 2, 3], [-1, -8, -2, -4, -1, 2, 3, 5], [-4, -4, -1, -2, -4, 1, 5, 6], [-6, -6, 2, -3, 1, 5, 4, 2], [-9, -2, 3, -1, -2, 4, 6, 3], [2, 2, -3, -1, 2, -4, -6, -1], [-1, 6, -2, 4, -1, -5, -4, -3], [-3, 4, 1, -2, 4, -1, -5, -2], [-6, 8, 2, 3, 1, -2, -3, -4], [1, 1, -4, -3, 1, -2, -3, 2], [-1, 2, -2, 0, -1, -1, 0, 1], [-1, 1, 0, -1, 1, 0, -1, 0], [-1, 1, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, -1, 0], [-3, 4, 1, 5, -3, -1, -5, -2], [-5, 2, 4, -1, 2, 3, -6, -1], [-8, 6, 5, 4, -1, 2, -4, -3], [-1, -1, -2, -3, -1, 2, -3, 4], [-2, 1, -1, 0, -2, 1, 0, 2], [-5, 1, 2, -3, 1, 4, -3, 2], [-4, 2, 1, 0, -1, 2, 0, 1], [-1, -1, -2, -3, 6, -5, -4, 4], [-4, 3, -1, 2, 3, -6, -2, 2], [-3, 1, 1, -2, 4, -1, -2, 1], [-1, 0, 0, -1, 2, -1, -1, 1], [-3, 1, 1, -1, 3, -1, -1, 1], [-9, 5, 3, 1, 5, -3, -1, 1], [-1, 0, 0, 0, 1, 0, 0, 0], [-1, -1, -2, -3, 5, -4, -3, 4], [-2, 1, -1, 0, 1, -2, 0, 2], [-4, 2, 1, 0, 2, -1, 0, 1], [-3, -3, 1, -2, 4, -1, -5, 5], [-6, 1, 2, 3, 1, -2, -3, 3], [-2, 0, 1, -1, 2, 0, -1, 1], [-8, -1, 5, -3, 6, 2, -4, 4], [-11, 3, 6, 2, 3, 1, -2, 2], [-1, -1, 0, -1, 1, 0, -1, 2], [-1, 0, 0, 0, 0, 0, 0, 1], [-7, -1, 4, -3, 5, 2, -3, 4], [-5, 1, 2, 0, 1, 1, 0, 2], [6, -1, -2, -3, -1, -5, -4, -3], [3, 3, -1, 2, -4, -6, -2, -5], [1, 1, 2, -4, 1, -2, -3, -4], [-2, 5, 3, 1, -2, -3, -1, -6], [2, -1, -2, -3, -1, -1, 0, 1], [1, 1, -4, -3, -5, -2, 3, 2], [0, 0, 0, -1, 0, 0, 0, 0], [-1, 1, 0, -1, -1, 0, 1, 0], [4, -3, 1, -2, -3, -1, -5, -2], [1, 1, 2, 3, -6, -2, -3, -4], [-1, -1, 5, -3, -1, 2, -4, -3], [-4, 3, 6, 2, -4, 1, -2, -5], [1, -2, -1, -3, -2, 1, 0, 2], [-1, -1, 1, -3, -1, 2, 0, 1], [-5, 1, 2, -3, -5, 4, 3, 2], [3, -4, -1, -5, 3, -6, -2, 2], [0, 0, 0, 0, 0, -1, 0, 0], [-2, -2, 3, -6, 5, -3, -1, 1], [-2, 0, 1, -2, 3, -1, -1, 1], [-5, 2, 4, -1, 2, -4, 1, -1], [1, -2, -1, -3, 1, -2, 0, 2], [-1, -1, -2, -3, -1, -4, 3, 4], [-1, -1, 1, -3, 2, -1, 0, 1], [-5, 1, 2, -3, 1, -2, 3, 2], [1, -6, 2, -4, 1, -2, -3, 3], [-2, -2, 3, 1, -2, -3, -1, 1], [-4, -4, 6, -5, 3, 1, -2, 2], [-1, 0, 1, 0, 0, 0, 0, 0], [0, -1, 0, -1, 0, 0, 0, 1], [-1, -1, 0, -1, -1, 0, 1, 2], [-2, -2, 2, -3, 1, 1, 0, 2], [-7, -1, 4, -3, -1, 2, 3, 4]]
def partner : List (List Nat) := [[69, 32, 16, 8, 4, 2, 1], [70, 33, 17, 9, 5, 3, 0], [71, 34, 18, 10, 6, 3, 0], [72, 35, 19, 11, 7, 1, 2], [73, 36, 20, 12, 6, 5, 0], [74, 37, 21, 13, 7, 1, 4], [75, 38, 22, 14, 7, 2, 4], [76, 39, 23, 15, 3, 5, 6], [77, 40, 24, 12, 10, 9, 0], [78, 41, 25, 13, 11, 1, 8], [79, 42, 26, 14, 11, 8, 2], [80, 43, 27, 15, 9, 3, 10], [81, 49, 28, 14, 13, 8, 4], [82, 47, 29, 15, 9, 5, 12], [83, 50, 30, 15, 10, 12, 6], [84, 51, 31, 11, 13, 7, 14], [85, 52, 24, 20, 18, 17, 0], [86, 53, 25, 21, 19, 16, 1], [91, 54, 26, 22, 19, 16, 2], [90, 55, 27, 23, 17, 18, 3], [92, 56, 28, 22, 21, 16, 4], [93, 57, 29, 23, 17, 20, 5], [91, 58, 30, 23, 18, 20, 6], [94, 59, 31, 19, 21, 22, 7], [95, 60, 28, 26, 25, 16, 8], [96, 61, 29, 27, 17, 24, 9], [98, 62, 30, 27, 24, 18, 10], [99, 63, 31, 25, 19, 26, 11], [100, 65, 30, 29, 24, 20, 12], [101, 66, 31, 25, 21, 28, 13], [102, 67, 31, 26, 28, 22, 14], [103, 68, 27, 29, 23, 30, 15], [104, 52, 40, 36, 34, 33, 0], [105, 53, 41, 37, 35, 1, 32], [106, 54, 42, 38, 35, 2, 32], [107, 55, 43, 39, 3, 33, 34], [108, 56, 49, 38, 37, 4, 32], [109, 57, 45, 39, 5, 33, 36], [110, 58, 50, 39, 6, 34, 36], [111, 59, 51, 7, 35, 37, 38], [112, 60, 49, 42, 41, 8, 32], [113, 61, 46, 43, 9, 33, 40], [114, 62, 50, 43, 10, 40, 34], [115, 63, 51, 11, 41, 35, 42], [116, 64, 49, 48, 47, 46, 45], [109, 64, 37, 48, 47, 46, 44], [113, 64, 41, 48, 47, 45, 44], [82, 64, 13, 48, 46, 45, 44], [118, 64, 51, 47, 46, 45, 44], [116, 65, 50, 44, 12, 40, 36], [117, 67, 51, 14, 42, 49, 38], [118, 68, 15, 43, 48, 39, 50], [119, 60, 56, 54, 53, 16, 32], [120, 61, 57, 55, 17, 52, 33], [121, 62, 58, 55, 18, 52, 34], [123, 63, 59, 19, 53, 54, 35], [124, 65, 58, 57, 20, 52, 36], [125, 66, 59, 21, 53, 56, 37], [126, 67, 59, 22, 54, 56, 38], [127, 68, 23, 55, 57, 58, 39], [128, 65, 62, 61, 24, 52, 40], [129, 66, 63, 25, 53, 60, 41], [130, 67, 63, 26, 60, 54, 42], [131, 68, 27, 61, 55, 62, 43], [133, 66, 48, 47, 46, 45, 44], [132, 67, 66, 28, 60, 56, 49], [133, 68, 29, 61, 57, 65, 64], [134, 68, 30, 62, 65, 58, 50], [135, 31, 63, 66, 59, 67, 51], [104, 85, 77, 73, 0, 71, 70], [105, 86, 78, 74, 1, 72, 69], [106, 87, 79, 75, 2, 72, 69], [107, 90, 80, 76, 3, 70, 71], [108, 92, 81, 4, 75, 74, 69], [109, 93, 82, 5, 76, 70, 73], [110, 87, 83, 6, 76, 71, 73], [111, 94, 84, 7, 72, 74, 75], [112, 95, 81, 8, 79, 78, 69], [113, 96, 82, 9, 80, 70, 77], [114, 98, 83, 10, 80, 77, 71], [115, 99, 84, 11, 78, 72, 79], [116, 100, 12, 83, 82, 77, 73], [47, 101, 13, 84, 78, 74, 81], [117, 102, 14, 84, 79, 81, 75], [118, 103, 15, 80, 82, 76, 83], [119, 95, 92, 16, 88, 86, 69], [120, 96, 93, 17, 90, 85, 70], [122, 97, 75, 91, 89, 71, 88], [122, 97, 92, 91, 89, 85, 87], [122, 97, 94, 91, 90, 88, 87], [123, 99, 94, 19, 86, 89, 72], [122, 97, 22, 89, 18, 88, 87], [124, 100, 20, 88, 93, 85, 73], [125, 101, 21, 94, 86, 92, 74], [127, 103, 23, 90, 93, 89, 76], [128, 100, 24, 98, 96, 85, 77], [129, 101, 25, 99, 86, 95, 78], [122, 102, 91, 89, 98, 88, 87], [130, 102, 26, 99, 95, 97, 79], [131, 103, 27, 96, 90, 98, 80], [132, 28, 102, 101, 95, 92, 81], [133, 29, 103, 96, 93, 100, 82], [134, 30, 103, 98, 100, 97, 83], [135, 31, 99, 101, 94, 102, 84], [119, 112, 108, 32, 106, 105, 69], [120, 113, 109, 33, 107, 70, 104], [121, 114, 110, 34, 107, 71, 104], [123, 115, 111, 35, 72, 105, 106], [124, 116, 36, 110, 109, 73, 104], [125, 45, 37, 111, 74, 105, 108], [126, 117, 38, 111, 75, 106, 108], [127, 118, 39, 76, 107, 109, 110], [128, 116, 40, 114, 113, 77, 104], [129, 46, 41, 115, 78, 105, 112], [130, 117, 42, 115, 79, 112, 106], [131, 118, 43, 80, 113, 107, 114], [132, 49, 117, 44, 81, 112, 108], [134, 50, 118, 83, 114, 116, 110], [135, 51, 84, 115, 48, 111, 117], [128, 124, 52, 121, 120, 85, 104], [129, 125, 53, 123, 86, 119, 105], [130, 126, 54, 123, 122, 119, 106], [97, 126, 91, 89, 121, 88, 87], [131, 127, 55, 90, 120, 121, 107], [132, 56, 126, 125, 92, 119, 108], [133, 57, 127, 93, 120, 124, 109], [134, 58, 127, 122, 121, 124, 110], [135, 59, 94, 123, 125, 126, 111], [132, 60, 130, 129, 95, 119, 112], [133, 61, 131, 96, 120, 128, 113], [134, 62, 131, 98, 128, 121, 114], [135, 63, 99, 129, 123, 130, 115], [65, 134, 133, 100, 128, 124, 116], [66, 135, 101, 129, 125, 132, 64], [67, 135, 102, 130, 132, 126, 117], [68, 103, 131, 133, 127, 134, 118]]
def hom (v : List Int) : List Int := (1:Int) :: v
def sval (nv v : List Int) : Int := (nv.getD 0 0) + dot (nv.drop 1) v

theorem ziegler_dim_notsym :
    ((detN 8 ([0,1,2,3,4,5,6,7].map (fun i => hom (V.getD i [])))) != 0)
    && ((List.range 7).all (fun j => (V.map (fun v => v.getD j 0)).sum == 7))
    && ([0, 4, 5, 9].all (fun i => !(V.contains ((V.getD i []).map (fun x => 1 - x))))) = true := by decide

theorem ziegler_supporting :
    (List.range 136).all (fun k => let f := facets.getD k []; let nv := normals.getD k [];
      (List.range 14).all (fun i => let s := sval nv (V.getD i []);
        if f.contains i then s == 0 else s < 0)) = true := by decide

theorem ziegler_closed :
    (List.range 136).all (fun k => let f := facets.getD k [];
      (List.range 7).all (fun p => let j := (partner.getD k []).getD p 0;
        (j != k) && ((f.eraseIdx p).all (fun u => (facets.getD j []).contains u)))) = true := by decide

#print axioms ziegler_dim_notsym
#print axioms ziegler_supporting
#print axioms ziegler_closed