ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

KNN symmetrization changes a graph cut

Example

Take $x_{1} = 0$ , $x_{2} = 1$ , and $x_{3} = 3$ on $R$ , and let each point choose its unique nearest neighbor ( $k = 1$ ). Define the union graph to contain a unit-weight edge when either directed nearest-neighbor choice selects it, and the mutual graph to contain a unit-weight edge only when both directions select it. For the partition ${1, 2}, {3}$ , the RatioCut is $3 / 2$ on the union graph and $0$ on the mutual graph.

Example references

Ulrike von Luxburg, A Tutorial on Spectral Clustering, Statistics and Computing 17(4), 2007

Jean Gallier, Notes on Elementary Spectral Graph Theory: Applications to Graph Clustering Using Normalized Cuts, 2013

Graph diagrams

The labels are vertex indices, and each drawn edge has unit weight. The left path is the union symmetrization; the right single edge is the mutual symmetrization. The verification above computes the cuts from the stated edge sets.

diagram failed to render:
\begin{tikzpicture}
\node[draw,circle] (u1) at (0,0) {$1$};
\node[draw,circle] (u2) at (1.5,0) {$2$};
\node[draw,circle] (u3) at (3,0) {$3$};
\draw (u1)--node[above] {$1$}(u2);
\draw (u2)--node[above] {$1$}(u3);
\node at (1.5,-0.8) {Union};
\node[draw,circle] (m1) at (5,0) {$1$};
\node[draw,circle] (m2) at (6.5,0) {$2$};
\node[draw,circle] (m3) at (8,0) {$3$};
\draw (m1)--node[above] {$1$}(m2);
\node at (6.5,-0.8) {Mutual};
\end{tikzpicture}

Facts & Assumptions

Given: Three real data points $x_{1} = 0$ , $x_{2} = 1$ , $x_{3} = 3$ , one-nearest-neighbor selection with no distance ties, and the union and mutual graph rules in the Example.

[A1]

The Euclidean distance on $R$ is $d (x, y) = ∣ x - y ∣$ .

[F1]

Finite weighted graph Laplacian: an admissible graph has symmetric nonnegative weights and zero diagonal; its support edge ${i, j}$ is present exactly when $w_{i j} > 0$ .

[F2]

RatioCut and normalized cut for a finite weighted graph: $cut (A, A^{c}) = \sum_{i \in A, j \notin A} w_{i j}$ and $RatioCut (A_{1}, A_{2}) = cut (A_{1}, A_{1}^{c}) / ∣ A_{1} ∣ + cut (A_{2}, A_{2}^{c}) / ∣ A_{2} ∣$ .

Verification

1.1givenA1algebra

The pairwise Euclidean distances are $∣ x_{1} - x_{2} ∣ = 1$ , $∣ x_{2} - x_{3} ∣ = 2$ , and $∣ x_{1} - x_{3} ∣ = 3$ . Therefore the directed choices are $1 \to 2$ , $2 \to 1$ , and $3 \to 2$ .

2.1givenF1step 1.1algebra

The union rule keeps an edge selected in either direction, so its undirected edges are ${1, 2}$ and ${2, 3}$ . The mutual rule keeps only edges selected in both directions, so its only edge is ${1, 2}$ . Both weight matrices satisfy [F1].

3.1F1step 2.1algebra

In the union graph, the only crossing edge for $A_{1} = {1, 2}$ and $A_{2} = {3}$ is ${2, 3}$ , of weight $1$ ; hence both one-sided cuts equal $1$ . In the mutual graph there is no crossing edge, so both cuts equal $0$ .

4.1F2step 3.1algebra∎

By [F2], the union RatioCut is $1 / 2 + 1 = 3 / 2$ , while the mutual RatioCut is $0 / 2 + 0 / 1 = 0$ . Thus the fixed data, neighbor count, and partition have different cut values under the two symmetrizations.

Graph diagrams

diagram failed to render:
\begin{tikzpicture}
\node[draw,circle] (u1) at (0,0) {$1$};
\node[draw,circle] (u2) at (1.5,0) {$2$};
\node[draw,circle] (u3) at (3,0) {$3$};
\draw (u1)--node[above] {$1$}(u2);
\draw (u2)--node[above] {$1$}(u3);
\node at (1.5,-0.8) {Union};
\node[draw,circle] (m1) at (5,0) {$1$};
\node[draw,circle] (m2) at (6.5,0) {$2$};
\node[draw,circle] (m3) at (8,0) {$3$};
\draw (m1)--node[above] {$1$}(m2);
\node at (6.5,-0.8) {Mutual};
\end{tikzpicture}

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · one level

2 results within one dependency step of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Ulrike von Luxburg, A Tutorial on Spectral Clustering, Statistics and Computing 17(4), 2007 (standard reference, not scraped)
Jean Gallier, Notes on Elementary Spectral Graph Theory: Applications to Graph Clustering Using Normalized Cuts, 2013 (standard reference, not scraped)