Theory Tame
section‹Tameness›
theory Tame
imports Graph ListSum
begin
subsection ‹Constants \label{sec:TameConstants}›
definition squanderTarget :: "nat" where
"squanderTarget ≡ 15410"
definition excessTCount :: "nat" (‹𝖺›)where
"𝖺 ≡ 6295"
definition squanderVertex :: "nat ⇒ nat ⇒ nat" (‹𝖻›)where
"𝖻 p q ≡ if p = 0 ∧ q = 3 then 6177
else if p = 0 ∧ q = 4 then 9696
else if p = 1 ∧ q = 2 then 6557
else if p = 1 ∧ q = 3 then 6176
else if p = 2 ∧ q = 1 then 7967
else if p = 2 ∧ q = 2 then 4116
else if p = 2 ∧ q = 3 then 12846
else if p = 3 ∧ q = 1 then 3106
else if p = 3 ∧ q = 2 then 8165
else if p = 4 ∧ q = 0 then 3466
else if p = 4 ∧ q = 1 then 3655
else if p = 5 ∧ q = 0 then 395
else if p = 5 ∧ q = 1 then 11354
else if p = 6 ∧ q = 0 then 6854
else if p = 7 ∧ q = 0 then 14493
else squanderTarget"
definition squanderFace :: "nat ⇒ nat" (‹𝖽›)where
"𝖽 n ≡ if n = 3 then 0
else if n = 4 then 2058
else if n = 5 then 4819
else if n = 6 then 7120
else squanderTarget"
text_raw‹
\index{‹𝖺›}
\index{‹𝖻›}
\index{‹𝖽›}
›
subsection‹Separated sets of vertices \label{sec:TameSeparated}›
text ‹A set of vertices $V$ is {\em separated},
\index{separated}
\index{‹separated›}
iff the following conditions hold:
›
text ‹2. No two vertices in V are adjacent:›
definition separated⇩2 :: "graph ⇒ vertex set ⇒ bool" where
"separated⇩2 g V ≡ ∀v ∈ V. ∀f ∈ set (facesAt g v). f∙v ∉ V"
text ‹3. No two vertices lie on a common quadrilateral:›
definition separated⇩3 :: "graph ⇒ vertex set ⇒ bool" where
"separated⇩3 g V ≡
∀v ∈ V. ∀f ∈ set (facesAt g v). |vertices f|≤4 ⟶ 𝒱 f ∩ V = {v}"
text ‹A set of vertices is called {\em separated},
\index{separated} \index{‹separated›}
iff no two vertices are adjacent or lie on a common quadrilateral:›
definition separated :: "graph ⇒ vertex set ⇒ bool" where
"separated g V ≡ separated⇩2 g V ∧ separated⇩3 g V"
subsection‹Admissible weight assignments\label{sec:TameAdmissible}›
text ‹
A weight assignment ‹w :: face ⇒ nat›
assigns a natural number to every face.
\index{‹admissible›}
\index{admissible weight assignment}
We formalize the admissibility requirements as follows:
›
definition admissible⇩1 :: "(face ⇒ nat) ⇒ graph ⇒ bool" where
"admissible⇩1 w g ≡ ∀f ∈ ℱ g. 𝖽 |vertices f| ≤ w f"
definition admissible⇩2 :: "(face ⇒ nat) ⇒ graph ⇒ bool" where
"admissible⇩2 w g ≡
∀v ∈ 𝒱 g. except g v = 0 ⟶ 𝖻 (tri g v) (quad g v) ≤ (∑⇘f∈facesAt g v⇙ w f)"
definition admissible⇩3 :: "(face ⇒ nat) ⇒ graph ⇒ bool" where
"admissible⇩3 w g ≡
∀v ∈ 𝒱 g. vertextype g v = (5,0,1) ⟶ (∑⇘f∈filter triangle (facesAt g v)⇙ w(f)) ≥ 𝖺"
text ‹Finally we define admissibility of weights functions.›
definition admissible :: "(face ⇒ nat) ⇒ graph ⇒ bool" where
"admissible w g ≡ admissible⇩1 w g ∧ admissible⇩2 w g ∧ admissible⇩3 w g"
subsection‹Tameness \label{sec:TameDef}›
definition tame9a :: "graph ⇒ bool" where
"tame9a g ≡ ∀f ∈ ℱ g. 3 ≤ |vertices f| ∧ |vertices f| ≤ 6"
definition tame10 :: "graph ⇒ bool" where
"tame10 g = (let n = countVertices g in 13 ≤ n ∧ n ≤ 15)"
definition tame10ub :: "graph ⇒ bool" where
"tame10ub g = (countVertices g ≤ 15)"
definition tame11a :: "graph ⇒ bool" where
"tame11a g = (∀v ∈ 𝒱 g. 3 ≤ degree g v)"
definition tame11b :: "graph ⇒ bool" where
"tame11b g = (∀v ∈ 𝒱 g. degree g v ≤ (if except g v = 0 then 7 else 6))"
definition tame12o :: "graph ⇒ bool" where
"tame12o g =
(∀v ∈ 𝒱 g. except g v ≠ 0 ∧ degree g v = 6 ⟶ vertextype g v = (5,0,1))"
text ‹7. There exists an admissible weight assignment of total
weight less than the target:›
definition tame13a :: "graph ⇒ bool" where
"tame13a g = (∃w. admissible w g ∧ (∑⇘f ∈ faces g⇙ w f) < squanderTarget)"
text ‹Finally we define the notion of tameness.›
definition tame :: "graph ⇒ bool" where
"tame g ≡ tame9a g ∧ tame10 g ∧ tame11a g ∧ tame11b g ∧ tame12o g ∧ tame13a g"
end