The four-core link-pattern rank gap

Proved

OPG500Counterexample.core_link_rank_gap

by hao jia · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsformalizationgeodesicsgraph-theory

Let $F$ be a triangle-free simple graph on $\{0,1,2,3\}$ . For each $i$ , let $N_i$ be a vertex set not containing $i$ . Assume that whenever $j\neq i$ and $j\notin N_i$ , the vertex $j$ has a neighbor in $N_i$ . Then

7<|E(F)|+\sum_{i=0}^{3}\#\pi_0(F[N_i]),

where $F[N_i]$ is the subgraph induced by $N_i$ and $\#\pi_0$ counts its connected components. This is a finite four-vertex combinatorial statement.

Preamble

import Definitions.Def_opg500_weighted_cycle_models

Formal statement

namespace OPG500Counterexample

/-- The finite four-core combinatorial obstruction used by the all-ties route.
Every triangle-free core with four link sets avoiding their indexed vertices and
dominating all omitted vertices has a strictly positive cycle-rank gap. -/
theorem core_link_rank_gap
    (F : SimpleGraph (Fin 4)) [DecidableRel F.Adj]
    (N : Fin 4 → Finset (Fin 4))
    (htriangleFree : ∀ ⦃a b c : Fin 4⦄,
      a ≠ b → b ≠ c → a ≠ c →
        ¬ (F.Adj a b ∧ F.Adj b c ∧ F.Adj c a))
    (havoids : ∀ i v, v ∈ N i → v ≠ i)
    (hdominates : ∀ i j, j ≠ i → j ∉ N i →
      ∃ k, k ∈ N i ∧ F.Adj j k) :
    7 < F.edgeFinset.card +
      ∑ i, Nat.card (F.induce {v | v ∈ N i}).ConnectedComponent := by sorry

end OPG500Counterexample

Source

Candidate C10, Sections T4 and T5: https://github.com/vibemathing/problem-opg-500-geodesic-cycles/blob/a41fe59b4535851ea55f6e868e938b9aaf81e924/research/artifacts/candidates/opg500-a01-c10/tight-rank.md

Read-back

What the Lean code literally says, in plain math · gpt-5.6-luna

Let $F$ be a simple graph on the four-element vertex set $\{0,1,2,3\}$ , with decidable adjacency, and let $N$ assign to each $i\in\{0,1,2,3\}$ a finite set $N_i$ of vertices. Assume that no three pairwise distinct vertices $a,b,c$ form a triangle in $F$ ; every $v\in N_i$ satisfies $v\ne i$ ; and, for every $i$ and every $j\ne i$ with $j\notin N_i$ , there exists $k\in N_i$ adjacent to $j$ in $F$ . Then

7<|E(F)|+\sum_{i=0}^{3}\#\pi_0\bigl(F[N_i]\bigr),

where $|E(F)|$ is the number of edges of $F$ , $F[N_i]$ is the graph induced by $N_i$ , and $\#\pi_0(F[N_i])$ is its number of connected components.

Human review

Endorsed by Shuze Chen · Sep 7, 2026
Endorsed by hao jia · Sep 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph