FormalConjectures/WrittenOnTheWallII/GraphConjecture314.lean

GitHub source file

4 declarations, 1 contain sorry, 0 declared as axioms

1. def WrittenOnTheWallII.GraphConjecture314.largestInducedPathSize The size of a largest induced path of $G$, as a natural number line 49 source

   Source documentation

   The size of a largest induced path of $G$, as a natural number.

   A subset $s \subseteq V(G)$ is an induced path when the induced subgraph G.induce s is a tree in which every vertex has degree at most $2$ (equivalently: a tree that is itself a path graph). We define largestInducedPathSize G as the supremum of s.card over all such subsets.

   Disambiguation. This is not the SimpleGraph.path invariant, which is the floor of the average distance — that one is the wrong tool for WOWII Conjecture 314, where $\mathrm{path}(G)$ denotes the size of a largest induced path.

   TODO: it would probably be clearer to rename the SimpleGraph.path invariant to something like pathBound / floorAvgDist to avoid this naming collision.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat

   Proof uses: SupSet.sSup, Set.ofPred, Exists, Finset, And, Eq, Finset.card, SimpleGraph.IsTree, SimpleGraph.induce, LE.le, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Subtype, Function.Embedding, Function.Embedding.subtype, OfNat.ofNat

   13 instances, coercions and auxiliary constants left out.

   noncomputable def largestInducedPathSize (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
   …

2. theorem WrittenOnTheWallII.GraphConjecture314.conjecture314 WOWII Conjecture 314: For every finite simple connected graph $G$ with $n > 1$ vertices, if $G$ is triangle-free and $\mathrm{path}(G) \le 4$, then $G$ is well totally dominated sorry line 81 source

   Source documentation

   WOWII Conjecture 314:

   For every finite simple connected graph $G$ with $n > 1$ vertices, if $G$ is triangle-free and $\mathrm{path}(G) \le 4$, then $G$ is well totally dominated.

   Here $\mathrm{path}(G) = \mathrm{largestInducedPathSize}\, G$ is the size of a largest induced path in $G$, defined locally above.

   Disambiguation. Earlier revisions of this file used the SimpleGraph.path invariant, but that is the floor of the average distance, not the size of a largest induced path — a different quantity that makes Conjecture 314 vacuous in many cases.

   Proof summary. In a connected, $K_{3}$-free, induced-$P_{5}$-free graph $G$:

   1. No minimal total dominating set has fewer than two vertices.
   2. No minimal total dominating set has more than three vertices.
   3. Minimal total dominating sets of sizes two and three cannot coexist.

   Thus, each minimal total dominating set in $G$ has the same size.

   The Lean proof was generated by OpenAI GPT-5.6 Sol.

   L4DEL explanation

   WOWII Conjecture 314: For every finite simple connected graph $G$ with $n > 1$ vertices, if $G$ is triangle-free and $\mathrm{path}(G) \le 4$, then $G$ is well totally dominated. Here $\mathrm{path}(G) = \mathrm{largestInducedPathSize}\, G$ is the size of a largest induced path in $G$, defined locally above. Disambiguation. Earlier revisions of this file used the SimpleGraph.path invariant, but that is the floor of the average distance, not the size of a largest induced path — a different quantity that makes Conjecture 314 vacuous in many cases. Proof summary. In a connected, $K_{3}$-free, induced-$P_{5}$-free graph $G$: 1. No minimal total dominating set has fewer than two vertices. 2. No minimal total dominating set has more than three vertices. 3. Minimal total dominating sets of sizes two and three cannot coexist. Thus, each minimal total dominating set in $G$ has the same size. The Lean proof was generated by OpenAI GPT-5.6 Sol.

   Sources and attribution: Pinned Lean source (1646ca16afd6)

   depends on sorry what this means

   Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, False, LE.le, Nat, WrittenOnTheWallII.GraphConjecture314.largestInducedPathSize, OfNat.ofNat, SimpleGraph.IsWellTotallyDominated

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   4 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

   Open to load the checked before-and-after goal states.

   theorem conjecture314 [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj]
       (hG : G.Connected)
       (hTriFree : ∀ a b c : α, G.Adj a b → G.Adj b c → G.Adj c a → False)
       (hPath : largestInducedPathSize G ≤ 4) :
       IsWellTotallyDominated G := by
   …

   Mentions: c, WrittenOnTheWallII.GraphConjecture314.largestInducedPathSize

3. example WrittenOnTheWallII.GraphConjecture314.(example at line 92) line 92 source

   Source documentation

   The complete graph $K_3$ has a triangle.

   example : ∃ a b c : Fin 3, (⊤ : SimpleGraph (Fin 3)).Adj a b ∧
       (⊤ : SimpleGraph (Fin 3)).Adj b c ∧ (⊤ : SimpleGraph (Fin 3)).Adj c a := by
   …

   Mentions: c

4. example WrittenOnTheWallII.GraphConjecture314.(example at line 98) line 98 source

   Source documentation

   largestInducedPathSize G is nonneg.

   example (G : SimpleGraph (Fin 3)) [DecidableRel G.Adj] :
       0 ≤ largestInducedPathSize G := Nat.zero_le _
   …

   Mentions: WrittenOnTheWallII.GraphConjecture314.largestInducedPathSize