Mathesis

Dhruv GuptaZetetic-Dhruvperson2026-09-24T00:00:00Z

Dirac's lemma, strong form: in a chordless-cycle-free adjacency structure, every vertex set is a clique or contains two nonadjacent simplicial vertices.

DeclHiddenChannelCapacity.dirac_strong

∀ {ι : Type u_1} [inst : DecidableEq ι] (𝒞 : Finset (Finset ι)),
  (¬∃ l, HiddenChannelCapacity.IsChordlessCycle 𝒞 l) →
    ∀ (S : Finset ι),
      (∀ x ∈ S, ∀ y ∈ S, x ≠ y → HiddenChannelCapacity.Adj 𝒞 x y) ∨
        ∃ u w,
          HiddenChannelCapacity.SimpIn 𝒞 S u ∧
            HiddenChannelCapacity.SimpIn 𝒞 S w ∧ u ≠ w ∧ ¬HiddenChannelCapacity.Adj 𝒞 u w

TopicGraphical models

ThesisStepHypothesisDefinition

DeclHiddenChannelCapacity.dirac_strongDeclaration kindtheorem
```
∀ {ι : Type u_1} [inst : DecidableEq ι] (𝒞 : Finset (Finset ι)),
  (¬∃ l, HiddenChannelCapacity.IsChordlessCycle 𝒞 l) →
    ∀ (S : Finset ι),
      (∀ x ∈ S, ∀ y ∈ S, x ≠ y → HiddenChannelCapacity.Adj 𝒞 x y) ∨
        ∃ u w,
          HiddenChannelCapacity.SimpIn 𝒞 S u ∧
            HiddenChannelCapacity.SimpIn 𝒞 S w ∧ u ≠ w ∧ ¬HiddenChannelCapacity.Adj 𝒞 u w
```
HiddenChannelCapacity.Adj HiddenChannelCapacity.IsChordlessCycle HiddenChannelCapacity.IsWalkOn HiddenChannelCapacity.ReachOn HiddenChannelCapacity.SimpIn HiddenChannelCapacity.instDecidableAdj
Uses

DeclHiddenChannelCapacity.sep_clique_stepDeclaration kindtheorem

The assembled-cycle contradiction: two length-minimal x-y connectors through disjoint, mutually non-adjacent sides cannot coexist with chordless-cycle-freeness when x and y are non-adjacent.

∀ {ι : Type u_1} [inst : DecidableEq ι] {𝒞 : Finset (Finset ι)},
  (¬∃ l, HiddenChannelCapacity.IsChordlessCycle 𝒞 l) →
    ∀ {QA QB : ι → Prop} {x y : ι},
      x ≠ y →
        ¬HiddenChannelCapacity.Adj 𝒞 x y →
          ¬QB x →
            ¬QB y →
              (∀ (v : ι), QA v → QB v → False) →
                (∀ (u v : ι), QA u → QB v → ¬HiddenChannelCapacity.Adj 𝒞 u v) →
                  ∀ (pA : List ι),
                    List.IsChain (HiddenChannelCapacity.Adj 𝒞) pA →
                      pA.Nodup →
                        pA.head? = some x →
                          pA.getLast? = some y →
                            (∀ v ∈ pA, v = x ∨ v = y ∨ QA v) →
                              (∀ (q : List ι),
                                  (List.IsChain (HiddenChannelCapacity.Adj 𝒞) q ∧
                                      q.Nodup ∧
                                        q.head? = some x ∧ q.getLast? = some y ∧ ∀ v ∈ q, v = x ∨ v = y ∨ QA v) →
                                    pA.length ≤ q.length) →
                                ∀ (pB : List ι),
                                  List.IsChain (HiddenChannelCapacity.Adj 𝒞) pB →
                                    pB.Nodup →
                                      pB.head? = some x →
                                        pB.getLast? = some y →
                                          (∀ v ∈ pB, v = x ∨ v = y ∨ QB v) →
                                            (∀ (q : List ι),
                                                (List.IsChain (HiddenChannelCapacity.Adj 𝒞) q ∧
                                                    q.Nodup ∧
                                                      q.head? = some x ∧
                                                        q.getLast? = some y ∧ ∀ v ∈ q, v = x ∨ v = y ∨ QB v) →
                                                  pB.length ≤ q.length) →
                                              False

HiddenChannelCapacity.Adj HiddenChannelCapacity.IsChordlessCycle HiddenChannelCapacity.cyclePairs

Uses

HiddenChannelCapacity.Adj.symm'
HiddenChannelCapacity.getElem_cyclePairs
HiddenChannelCapacity.getLast_getElem
HiddenChannelCapacity.head_getElem
HiddenChannelCapacity.length_cyclePairs
HiddenChannelCapacity.mod_succ_cases
HiddenChannelCapacity.no_chord_of_minimal

Used by

HiddenChannelCapacity.dirac_strong

DeclHiddenChannelCapacity.no_chord_of_minimalDeclaration kindtheorem

Minimality kills chords: a length-minimal constrained x-y path has no adjacency between positions at distance ≥ 2.

∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {Q : ι → Prop} {x y : ι} {p : List ι},
  List.IsChain (HiddenChannelCapacity.Adj 𝒞) p →
    p.head? = some x →
      p.getLast? = some y →
        (∀ v ∈ p, v = x ∨ v = y ∨ Q v) →
          (∀ (q : List ι),
              (List.IsChain (HiddenChannelCapacity.Adj 𝒞) q ∧
                  q.Nodup ∧ q.head? = some x ∧ q.getLast? = some y ∧ ∀ v ∈ q, v = x ∨ v = y ∨ Q v) →
                p.length ≤ q.length) →
            p.Nodup →
              ∀ {i j : ℕ} (hi : i < p.length) (hj : j < p.length), i + 2 ≤ j → ¬HiddenChannelCapacity.Adj 𝒞 p[i] p[j]

HiddenChannelCapacity.Adj

Uses

HiddenChannelCapacity.isChain_drop
HiddenChannelCapacity.isChain_take

Used by

HiddenChannelCapacity.sep_clique_step

DeclHiddenChannelCapacity.mod_succ_casesDeclaration kindtheorem
```
∀ (n i : ℕ), i < n → (i + 1) % n = i + 1 ∧ i + 1 < n ∨ (i + 1) % n = 0 ∧ i + 1 = n
```
Used by
- HiddenChannelCapacity.sep_clique_step

DeclHiddenChannelCapacity.getLast_getElemDeclaration kindtheorem

∀ {ι : Type u_1} {p : List ι} {y : ι}, p.getLast? = some y → ∀ (h0 : 0 < p.length), p[p.length - 1] = y

Used by

HiddenChannelCapacity.sep_clique_step

DeclHiddenChannelCapacity.getElem_cyclePairsDeclaration kindtheorem

∀ {ι : Type u_1} [inst : DecidableEq ι] (l : List ι) (h0 : 0 < l.length) (i : ℕ)
  (h : i < (HiddenChannelCapacity.cyclePairs l).length),
  (HiddenChannelCapacity.cyclePairs l)[i] = {l[i], l[(i + 1) % l.length]}

HiddenChannelCapacity.cyclePairs

Uses

HiddenChannelCapacity.length_cyclePairs

Used by

HiddenChannelCapacity.sep_clique_step

DeclHiddenChannelCapacity.length_cyclePairsDeclaration kindtheorem
```
∀ {ι : Type u_1} [inst : DecidableEq ι] (l : List ι), (HiddenChannelCapacity.cyclePairs l).length = l.length
```
HiddenChannelCapacity.cyclePairs
Used by
- HiddenChannelCapacity.getElem_cyclePairs
- HiddenChannelCapacity.sep_clique_step
DeclHiddenChannelCapacity.reachOn_transDeclaration kindtheorem
```
∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {P : ι → Prop} {u v w : ι},
  HiddenChannelCapacity.ReachOn 𝒞 P u v → HiddenChannelCapacity.ReachOn 𝒞 P v w → HiddenChannelCapacity.ReachOn 𝒞 P u w
```
HiddenChannelCapacity.Adj HiddenChannelCapacity.IsWalkOn HiddenChannelCapacity.ReachOn
Uses
- HiddenChannelCapacity.reachOn_of_walk
Used by
- HiddenChannelCapacity.dirac_strong
DeclHiddenChannelCapacity.reachOn_symmDeclaration kindtheorem
```
∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {P : ι → Prop} {u v : ι},
  HiddenChannelCapacity.ReachOn 𝒞 P u v → HiddenChannelCapacity.ReachOn 𝒞 P v u
```
HiddenChannelCapacity.Adj HiddenChannelCapacity.IsWalkOn HiddenChannelCapacity.ReachOn
Uses
- HiddenChannelCapacity.Adj.symm'
Used by
- HiddenChannelCapacity.dirac_strong
DeclHiddenChannelCapacity.reachOn_reflDeclaration kindtheorem
```
∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {P : ι → Prop} {u : ι}, P u → HiddenChannelCapacity.ReachOn 𝒞 P u u
```
HiddenChannelCapacity.Adj HiddenChannelCapacity.IsWalkOn HiddenChannelCapacity.ReachOn
Used by
- HiddenChannelCapacity.dirac_strong
DeclHiddenChannelCapacity.reachOn_of_mem_walkDeclaration kindtheorem
Every vertex on a walk is reachable from its head.
```
∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {P : ι → Prop} {u v : ι} {p : List ι},
  HiddenChannelCapacity.IsWalkOn 𝒞 P p → p.head? = some u → v ∈ p → HiddenChannelCapacity.ReachOn 𝒞 P u v
```
HiddenChannelCapacity.Adj HiddenChannelCapacity.IsWalkOn HiddenChannelCapacity.ReachOn
Uses
- HiddenChannelCapacity.isChain_take
- HiddenChannelCapacity.reachOn_of_walk
Used by
- HiddenChannelCapacity.dirac_strong
DeclHiddenChannelCapacity.reachOn_extendDeclaration kindtheorem
```
∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {P : ι → Prop} {u v w : ι},
  HiddenChannelCapacity.ReachOn 𝒞 P u v → HiddenChannelCapacity.Adj 𝒞 v w → P w → HiddenChannelCapacity.ReachOn 𝒞 P u w
```
HiddenChannelCapacity.Adj HiddenChannelCapacity.IsWalkOn HiddenChannelCapacity.ReachOn
Uses
- HiddenChannelCapacity.reachOn_of_walk
Used by
- HiddenChannelCapacity.dirac_strong

DeclHiddenChannelCapacity.exists_min_pathDeclaration kindtheorem

∀ {ι : Type u_1} {Q : List ι → Prop}, (∃ p, Q p) → ∃ p, Q p ∧ ∀ (q : List ι), Q q → p.length ≤ q.length

Used by

HiddenChannelCapacity.dirac_strong

DeclHiddenChannelCapacity.exists_connectorDeclaration kindtheorem

A connector: an x-y path with interior inside Q, from adjacent entry points and interior reachability.

∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {Q : ι → Prop} {x y u₁ u₂ : ι},
  x ≠ y →
    HiddenChannelCapacity.Adj 𝒞 x u₁ →
      HiddenChannelCapacity.Adj 𝒞 y u₂ →
        HiddenChannelCapacity.ReachOn 𝒞 Q u₁ u₂ →
          ¬Q x →
            ¬Q y →
              ∃ p,
                List.IsChain (HiddenChannelCapacity.Adj 𝒞) p ∧
                  p.Nodup ∧ p.head? = some x ∧ p.getLast? = some y ∧ ∀ v ∈ p, v = x ∨ v = y ∨ Q v

HiddenChannelCapacity.Adj HiddenChannelCapacity.IsWalkOn HiddenChannelCapacity.ReachOn

Uses

HiddenChannelCapacity.Adj.symm'

Used by

HiddenChannelCapacity.dirac_strong

DeclHiddenChannelCapacity.erase_separatesDeclaration kindtheorem
If x has no neighbor reachable from a off the separator, then erasing x still separates: the first x-occurrence on any violating path has its predecessor reachable from a and adjacent to x.
```
∀ {ι : Type u_1} [inst : DecidableEq ι] {𝒞 : Finset (Finset ι)} {S Sep : Finset ι} {a b x : ι},
  x ≠ a →
    (∀ (u : ι),
        u ∈ S \ Sep ∧ HiddenChannelCapacity.ReachOn 𝒞 (fun v => v ∈ S \ Sep) a u → ¬HiddenChannelCapacity.Adj 𝒞 x u) →
      ¬HiddenChannelCapacity.ReachOn 𝒞 (fun v => v ∈ S \ Sep) a b →
        ¬HiddenChannelCapacity.ReachOn 𝒞 (fun v => v ∈ S \ Sep.erase x) a b
```
HiddenChannelCapacity.Adj HiddenChannelCapacity.IsWalkOn HiddenChannelCapacity.ReachOn
Uses
Used by
- HiddenChannelCapacity.dirac_strong
DeclHiddenChannelCapacity.reachOn_of_walkDeclaration kindtheorem
Every chained walk contains a duplicate-free path with the same endpoints and vertices.
```
∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {P : ι → Prop} (p : List ι),
  HiddenChannelCapacity.IsWalkOn 𝒞 P p →
    ∀ {u v : ι}, p.head? = some u → p.getLast? = some v → HiddenChannelCapacity.ReachOn 𝒞 P u v
```
HiddenChannelCapacity.Adj HiddenChannelCapacity.IsWalkOn HiddenChannelCapacity.ReachOn
Uses
- HiddenChannelCapacity.isChain_drop
- HiddenChannelCapacity.isChain_take
Used by
DeclHiddenChannelCapacity.isChain_dropDeclaration kindtheorem
```
∀ {ι : Type u_1} {R : ι → ι → Prop} {p : List ι}, List.IsChain R p → ∀ (n : ℕ), List.IsChain R (List.drop n p)
```
Used by
- HiddenChannelCapacity.no_chord_of_minimal
- HiddenChannelCapacity.reachOn_of_walk
DeclHiddenChannelCapacity.isChain_takeDeclaration kindtheorem
```
∀ {ι : Type u_1} {R : ι → ι → Prop} {p : List ι}, List.IsChain R p → ∀ (n : ℕ), List.IsChain R (List.take n p)
```
Used by
DeclHiddenChannelCapacity.head_getElemDeclaration kindtheorem
Positional form of the head.
```
∀ {ι : Type u_1} {p : List ι} {x : ι}, p.head? = some x → ∀ (h0 : 0 < p.length), p[0] = x
```
Used by
- HiddenChannelCapacity.erase_separates
- HiddenChannelCapacity.sep_clique_step

DeclHiddenChannelCapacity.gcast_listDeclaration kindtheorem

∀ {ι : Type u_1} (l : List ι) {s t : ℕ} (hs : s < l.length) (ht : t < l.length), s = t → l[s] = l[t]

Used by

HiddenChannelCapacity.erase_separates

DeclHiddenChannelCapacity.Adj.symm'Declaration kindtheorem
```
∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {u v : ι}, HiddenChannelCapacity.Adj 𝒞 u v → HiddenChannelCapacity.Adj 𝒞 v u
```
HiddenChannelCapacity.Adj
Used by

Hypothesishchord

¬∃ l, HiddenChannelCapacity.IsChordlessCycle 𝒞 l

DefinitionHiddenChannelCapacity.Adjdef
Primal adjacency: distinct co-hosted vertices.
```
{ι : Type u_1} → Finset (Finset ι) → ι → ι → Prop
```
DefinitionHiddenChannelCapacity.IsChordlessCycledef
A chordless cycle: duplicate-free, length ≥ 4, consecutive pairs hosted, and the only adjacencies among its vertices are the cyclically consecutive ones.
```
{ι : Type u_1} → [DecidableEq ι] → Finset (Finset ι) → List ι → Prop
```
DefinitionHiddenChannelCapacity.IsWalkOndef
A walk constrained to P: chained adjacencies, every vertex satisfies P.
```
{ι : Type u_1} → Finset (Finset ι) → (ι → Prop) → List ι → Prop
```
DefinitionHiddenChannelCapacity.ReachOndef
Reachability within P: a duplicate-free walk with the given endpoints.
```
{ι : Type u_1} → Finset (Finset ι) → (ι → Prop) → ι → ι → Prop
```
DefinitionHiddenChannelCapacity.SimpIndef
v is simplicial within the vertex set S: it lies in S and its 𝒞-neighbors inside S are pairwise adjacent.
```
{ι : Type u_1} → Finset (Finset ι) → Finset ι → ι → Prop
```
DefinitionHiddenChannelCapacity.cyclePairsdef
The consecutive-pair supports of a cyclic vertex list.
```
{ι : Type u_1} → [DecidableEq ι] → List ι → List (Finset ι)
```

DefinitionHiddenChannelCapacity.instDecidableAdjdef

{ι : Type u_1} → [DecidableEq ι] → (𝒞 : Finset (Finset ι)) → (u v : ι) → Decidable (HiddenChannelCapacity.Adj 𝒞 u v)

DOIMTH.R-2026-6020

Cite

Verification

Replay: accepted
Axioms: Classical.choiceQuot.soundpropext
Statement identity: not-applicable
Substrate: Lean 4 kernel v4.31.0
Dictionary pin: design-lab@5802df4 · initial
Frozen export: 20e38a6b8d2b
Verified: 2026-09-24T00:00:00Z