From 9ef8f9efda50f6df545b169169af3e3f907a725c Mon Sep 17 00:00:00 2001 From: zbrachinara Date: Sat, 23 Nov 2024 21:14:30 -0500 Subject: [PATCH] first attempt at defining three partition problem --- .../Proofs/S4_EightColumn/ThreePartition.lean | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 NpTetris/Proofs/S4_EightColumn/ThreePartition.lean diff --git a/NpTetris/Proofs/S4_EightColumn/ThreePartition.lean b/NpTetris/Proofs/S4_EightColumn/ThreePartition.lean new file mode 100644 index 0000000..0a106e0 --- /dev/null +++ b/NpTetris/Proofs/S4_EightColumn/ThreePartition.lean @@ -0,0 +1,18 @@ +import Mathlib.Data.Multiset.Basic +import Mathlib.Data.Multiset.Fold + +structure ThreePartitionProblem (size : ℕ) (int_set : Multiset ℕ) (T : ℕ) where +set_size : int_set.card = 3 * size +partitionable : int_set.sum = size * T +normal x : x ∈ int_set → T / 4 < x ∧ x < T / 2 + +namespace ThreePartitionProblem + +variable {size int_set T} (problem : ThreePartitionProblem size int_set T) + +structure solution (problem : ThreePartitionProblem size int_set T) where +part : List (ℕ × ℕ × ℕ) +partition_valid : part.foldr (λ ⟨a,b,c⟩ x ↦ {a,b,c} ∪ x) ∅ = int_set +partitions_sum x y z : ⟨x,y,z⟩ ∈ part → x + y + z = T + +def partition_exists := Inhabited problem.solution