Chapter 54: Experimental and Computational Combinatorics

Can exhaustive experiments expose a false conjecture before a proof attempt?

Suppose every triangle-free graph you have inspected can be colored with two vertex colors so adjacent vertices differ. You might propose: every triangle-free graph is bipartite. Here triangle-free means no three vertices have all three possible edges; bipartite means such a proper two-coloring exists. The proposed implication is false, but checking only graphs with at most four vertices will not expose it.

A five-cycle is the smallest obstruction. Use vertices $0,1,2,3,4$ and edges $03,04,12,14,23$. Read these as unordered pairs. The cycle order is $2,3,0,4,1$, returning to two. There are no chords, hence no triangles. Along an odd cycle, colors must alternate, but the closing edge then joins equal colors. Thus this graph is triangle-free and not bipartite.

This example shows the two roles of computation. Exhaustive search can discover an object contradicting a universal statement. A small independent checker can validate that particular object without trusting how it was found. Neither a failed heuristic search nor a table of successful small cases establishes an all-size theorem.

The chapter foundation is the precise false claim, the five-cycle certificate, and the difference between finding and verifying. Later extensions build a reproducible experiment, explain its coverage and complexity, and translate corrected observations into proofs. Useful prerequisites are algorithmic generation, bijective and computer-assisted enumeration, and combinatorial algorithms. No external solver is needed for the running example.

54.1 Discovering patterns through exhaustive enumeration

Optional extension; not required to complete the chapter foundation.

An exhaustive enumeration must specify its objects and prove coverage. For a simple undirected graph on the fixed labeled vertex set $\{0,\ldots,n-1\}$, there are $N=\binom n2$ possible edges. List the unordered pairs in lexicographic order and let bit $i$ of an integer mask indicate whether pair $i$ is present. The masks from zero through $2^N-1$ are in bijection with all such graphs: each graph determines one edge subset and one mask, and each mask determines one graph.

This representation includes disconnected graphs and isolated vertices. It excludes loops and parallel edges. It counts labelings separately, so two isomorphic edge subsets can appear more than once as abstract graph types. That is intended here; removing repeated isomorphism types is a different enumeration problem.

Solved example. At $n=3$, eight masks encode all graphs. Seven are triangle-free and bipartite; the remaining complete graph is neither. At $n=4$, forty-one of sixty-four graphs are triangle-free, and all forty-one are bipartite. At $n=5$, there are 388 triangle-free graphs, of which 376 are bipartite. The twelve counterexamples are the twelve labelings of a five-cycle: $5!/(2\cdot5)=12$, since rotations and reversal preserve the cycle.

The counts were calculated by complete finite enumeration, not inferred by extrapolating the sequence. A change to unlabeled graphs would change the table: those twelve five-cycles represent one isomorphism type. A change to directed graphs would also change the encoding and the meaning of a cycle.

The established framework of canonical labeling and graph-isomorphism computation is described by McKay and Piperno. Scope: our labeled mask bijection is proved directly. The theory needed to generate exactly one representative per isomorphism class is omitted and is not assumed in the counts.

Exercise. How many labeled simple graphs on five vertices are encoded? Hint: count possible edges first. Solution: $2^{\binom52}=2^{10}=1024$. Using $2^{25}$ would incorrectly include ordered pairs and diagonal entries as separate edge choices.

54.2 Designing computational experiments

Optional extension; not required to complete the chapter foundation.

An experiment should separate its question, object generator, measurement, verification, and stopping rule. Our question is whether the false implication has a counterexample at each size. The generator visits every mask; measurements record total, triangle-free, and bipartite counts; the first counterexample is retained; the run still completes every mask at each requested size. Stopping at the first witness would be enough to refute the claim but would not produce the complete count table.

Solved design. For each $n=0,\ldots,5$, decode masks in increasing order. Test triangle-freeness using all vertex triples. For survivors, run a breadth-first two-coloring procedure over every connected component. If it encounters an edge whose endpoints have the same color, reconstruct an odd cycle from the two parent paths. Count all survivors and record the first failure. The default search inspects $1+1+2+8+64+1024=1100$ masks, including the empty graph.

No random seed is needed for this deterministic experiment. The result depends on the stated edge order if “first” refers to a mask, but the minimum counterexample size does not. The first five-vertex witness has mask 220 under our convention; another implementation could return an isomorphic five-cycle with a different mask.

For comparison, independent fair edge bits produce the uniform labeled random graph on five vertices. A counterexample has probability $12/1024=3/256$ per proposal, so one hundred independent proposals miss all counterexamples with probability $(253/256)^{100}$, about $0.308$. Conditional on triangle-freeness, the counterexample probability is instead $12/388=3/97$. The conditioning changes the sample space. These are exact sampling calculations, not simulated observations.

Exercise. Why record the stopping rule? Hint: compare early discovery with completed enumeration. Solution: a run stopped after the first witness has not measured the number of all witnesses or all triangle-free graphs. Its output supports a different claim.

54.3 Enumerating small counterexamples

Optional extension; not required to complete the chapter foundation.

Language-independent pseudocode is: for each size, create the ordered list of possible edges; for each bit mask, decode its edge subset; discard graphs with a triangle; attempt two-coloring in every component; count successes and failures; save the first failing graph with an odd cycle; after completing all masks, check the saved object independently and serialize the results.

The Python panel implements that procedure using only the standard library. The producer uses a set-based triple test. The witness checker uses an adjacency matrix and the number of closed walks of length three, which equals six times the number of triangles in a simple undirected graph. It also checks the odd-cycle certificate explicitly, without reusing the producer's two-coloring algorithm. Verification failures raise exceptions, so they remain active when Python assertions are disabled.

from collections import deque
from hashlib import sha256
from itertools import combinations
import json
import platform


def triangle_free(n, edges):
    present = set(edges)
    return all(not ({(a, b), (a, c), (b, c)} <= present)
               for a, b, c in combinations(range(n), 3))


def odd_cycle(n, edges):
    adj = [[] for _ in range(n)]
    for u, v in edges:
        adj[u].append(v)
        adj[v].append(u)
    color = [-1] * n
    parent = [-1] * n
    for root in range(n):
        if color[root] != -1:
            continue
        color[root] = 0
        queue = deque([root])
        while queue:
            u = queue.popleft()
            for v in adj[u]:
                if color[v] == -1:
                    color[v] = 1 - color[u]
                    parent[v] = u
                    queue.append(v)
                elif color[v] == color[u]:
                    left, right = [], []
                    a, b = u, v
                    while a != -1:
                        left.append(a)
                        a = parent[a]
                    while b != -1:
                        right.append(b)
                        b = parent[b]
                    common = next(a for a in left if a in set(right))
                    return (left[:left.index(common) + 1]
                            + list(reversed(right[:right.index(common)])))
    return None


def verify_witness(record):
    n = record["n"]
    if type(n) is not int or n < 0:
        raise ValueError("invalid vertex count")
    edges = record["edges"]
    present = set()
    matrix = [[0] * n for _ in range(n)]
    for edge in edges:
        if len(edge) != 2:
            raise ValueError("an edge must have two endpoints")
        u, v = edge
        if not (type(u) is int and type(v) is int and 0 <= u < v < n):
            raise ValueError("invalid simple edge")
        if (u, v) in present:
            raise ValueError("duplicate edge")
        present.add((u, v))
        matrix[u][v] = matrix[v][u] = 1
    closed_walks = sum(matrix[i][j] * matrix[j][k] * matrix[k][i]
                       for i in range(n) for j in range(n) for k in range(n))
    if closed_walks != 0:
        raise ValueError("graph contains a triangle")
    cycle = record["odd_cycle"]
    if len(cycle) < 3 or len(cycle) % 2 == 0 or len(set(cycle)) != len(cycle):
        raise ValueError("not a simple odd cycle")
    if any(type(v) is not int or not 0 <= v < n for v in cycle):
        raise ValueError("invalid cycle vertex")
    for u, v in zip(cycle, cycle[1:] + cycle[:1]):
        if tuple(sorted((u, v))) not in present:
            raise ValueError("missing cycle edge")
    return True


def run(max_n=5):
    if type(max_n) is not int or not 0 <= max_n <= 6:
        raise ValueError("this illustrative search supports 0 through 6")
    summaries = []
    first = None
    for n in range(max_n + 1):
        slots = list(combinations(range(n), 2))
        tf_count = bip_count = 0
        for mask in range(1 << len(slots)):
            edges = [edge for i, edge in enumerate(slots) if (mask >> i) & 1]
            if not triangle_free(n, edges):
                continue
            tf_count += 1
            cycle = odd_cycle(n, edges)
            if cycle is None:
                bip_count += 1
            elif first is None:
                first = {"n": n, "mask": mask,
                         "edges": [list(edge) for edge in edges],
                         "odd_cycle": cycle}
        summaries.append({"n": n, "all_graphs": 1 << len(slots),
                          "triangle_free": tf_count, "bipartite": bip_count,
                          "counterexamples": tf_count - bip_count})
    if first is not None:
        roundtrip = json.loads(json.dumps(first))
        verify_witness(roundtrip)
        graph = {"n": first["n"], "edges": first["edges"]}
        payload = json.dumps(graph, sort_keys=True, separators=(",", ":"))
        first["graph_sha256"] = sha256(payload.encode("utf-8")).hexdigest()
    return {"python_version": platform.python_version(),
            "max_n": max_n, "summaries": summaries,
            "first_counterexample": first}


if __name__ == "__main__":
    print(json.dumps(run(5), sort_keys=True, indent=2))

Correctness. The mask bijection proves generator coverage. During breadth-first search, each newly reached vertex gets the opposite color to its parent. If every edge joins opposite colors, the assignments form a valid two-coloring. If an edge joins equal colors, the parent paths have equal depth parity; deleting their common prefix produces an even-length tree path between its endpoints, and the offending edge closes an odd cycle. The verifier checks that this cycle is simple and present. Its triangle check relies on symmetric zero-one adjacency with a zero diagonal, which the schema checks enforce.

For a fixed size, decoding costs $O(n^2)$, the triangle test costs $O(n^3)$, and breadth-first search plus certificate reconstruction is polynomial. The simple worst-case total is $O(2^{\binom n2}n^3)$, with $O(n^2)$ working space for a graph and checker matrix, plus the small summary. The program deliberately limits the illustrative range to at most six vertices. Its counts are labeled, and it does not use isomorphism pruning or an external SAT solver.

Solved output. The default run returns mask 220, edges $03,04,12,14,23$, and odd-cycle certificate $[2,3,0,4,1]$. It continues through all 1024 masks at size five and reports twelve failures. The first-record choice and the complete counts answer different questions.

Exercise. Why loop over every root in odd_cycle? Hint: the graph may be disconnected. Solution: a conflict can lie in a component not reached from vertex zero. A checker limited to one component would wrongly accept some non-bipartite graphs.

54.4 Constructing and validating combinatorial objects

Optional extension; not required to complete the chapter foundation.

A producer may use heuristics, randomness, search pruning, or a solver. A verifier should accept a clearly defined exported object and establish the required properties without trusting the producer's internal state. Its checks need to cover the object schema as well as the mathematical constraints. Otherwise a malformed graph can accidentally satisfy a test that was designed only for valid input.

Solved witness audit. For our graph, the verifier establishes five vertices, five distinct simple edges, symmetric adjacency, and no loops. Matrix multiplication gives $\operatorname{tr}(A^3)=0$, so the triangle count is zero. The supplied cycle contains five distinct valid vertices and all five required edges, including the closing edge $12$. These two properties refute the conjecture. Merely checking that each vertex has degree two would not certify that the component is an odd cycle.

For a simple undirected graph, a triangle contributes six closed three-step walks, one for each starting vertex and direction. Conversely, a closed walk of length three must use three distinct vertices because loops are forbidden; its three edges form a triangle. This proves the matrix check, rather than treating a library output as an unexplained oracle.

A negative certificate is different from a positive one. For bipartiteness, a coloring verifies success by checking every edge. For non-bipartiteness, a simple odd cycle verifies failure by the alternating-color contradiction. Neither certificate requires repeating the full search over color assignments.

Validation should reject deliberate corruptions. Duplicate an edge, insert a loop, remove a required cycle edge, repeat a cycle vertex, or use an out-of-range label. Also add a chord to the five-cycle: every such chord creates a triangle, so the triangle-free requirement should fail. These tests distinguish an object certificate from a visually plausible picture.

The separation between search and independently checkable proof is a central feature of certified SAT verification. Scope: our checker is ordinary executable Python, not a formally verified proof assistant. Different representations and tests reduce shared mistakes but do not eliminate every possible implementation error.

Exercise. Can a checksum replace the odd-cycle and triangle checks? Hint: what does a digest say about mathematical properties? Solution: no. It identifies bytes under a stated encoding; it does not prove that the encoded graph satisfies any constraint.

54.5 SAT, SMT, and integer-programming formulations

Optional extension; not required to complete the chapter foundation.

A SAT model uses Boolean variables and clauses; SMT adds specified theories such as integer arithmetic; an integer program uses linear constraints together with integrality. Correctness requires an equivalence between models and the intended combinatorial objects. A solver certificate for the wrong encoding proves the wrong statement.

Solved two-coloring formulation. For a fixed graph, let $y_v$ indicate a vertex color. Every edge $uv$ requires $y_u\ne y_v$. In SAT this is the pair of clauses $(y_u\vee y_v)$ and $(\neg y_u\vee\neg y_v)$. The first forbids both false; the second forbids both true. Together they allow exactly the two opposite-color assignments. For the five-cycle there are five variables and ten edge clauses.

As an integer program, use $y_v\in\{0,1\}$ and $y_u+y_v=1$ for every edge. Summing the five cycle equalities gives $2\sum_v y_v=5$, impossible for integers. This is a short exact infeasibility certificate. Dropping integrality permits $y_v=1/2$ for every vertex, so the linear relaxation is feasible. LP feasibility is not a binary coloring.

An SMT formulation over integers can use the same equations with $0\le y_v\le1$. Over real arithmetic those bounds would not enforce integrality. The SMT-LIB standard specifies theory and language conventions; record the actual logic used rather than only the solver's name. The example is solved algebraically here; no external solver run is being claimed.

For graph synthesis, edge variables $e_{uv}$ can encode a candidate graph. Triangle-freeness uses a clause $\neg e_{ab}\vee\neg e_{ac}\vee\neg e_{bc}$ for every vertex triple. Non-bipartiteness needs to exclude every coloring, not exhibit one bad coloring. For each fixed color assignment $s$, add a clause requiring at least one present edge with equal-colored endpoints: $\bigvee_{u\lt v,\ s_u=s_v}e_{uv}$. The conjunction over assignments expresses the universal obstruction. Complementary colorings yield the same clause, so for $n\ge1$ one may restrict to $s_0=0$. That symmetry reduction needs the color-complement argument; it is not an arbitrary pruning rule.

Exercise. Why is “there exists a coloring with a monochromatic edge” the wrong synthesis constraint? Hint: color all vertices alike. Solution: every nonempty graph satisfies it, even a single edge, which is bipartite. The correct obstruction quantifies over all colorings.

Omitted prerequisites: solver-specific proof logging, proof checking after preprocessing, and numerical tolerances in general integer optimization. The tiny formulations and parity certificate above are fully explicit.

54.6 Computer-assisted proofs

Optional extension; not required to complete the chapter foundation.

A computer-assisted proof must explain why the computation establishes the mathematical statement. For a finite exhaustive claim, that includes a representation theorem, coverage, a correct predicate, and trustworthy execution or checkable proof artifacts. For an unbounded theorem, one additionally needs a reduction to the finite computation or a separate general argument. A large search is not automatically a large proof.

Solved finite proof structure. To show there is no triangle-free non-bipartite graph on at most four vertices, our mask bijection covers every labeled graph in that range, and correct tests classify all survivors as bipartite. Every abstract finite simple graph has a labeling, so labeled coverage suffices for this nonexistence statement. The returned five-cycle provides a separate existence certificate at five vertices.

There is also a short structural proof of the same minimality. A non-bipartite graph has an odd cycle. A triangle-free graph has no odd cycle of length three, so its smallest possible odd cycle has at least five vertices. The two arguments are valuable cross-checks; the structural proof extends beyond a particular executable's output.

SAT-based proofs separate a search engine from a proof checker. For satisfiability, export and validate an assignment. For unsatisfiability, a clause-derivation certificate can be checked against the exact input formula. Cruz-Filipe and collaborators describe LRAT verification and certified checkers. Omitted prerequisites: the resolution-asymmetric-tautology rule, hint formats, and formal checker correctness. A solver's timeout or “unknown” result is not an unsatisfiability proof.

A historical example is the Heule–Kullmann–Marek Boolean Pythagorean-triples computation, which combined a SAT encoding, structured search, and verification. Its role here is to illustrate proof production and checking, not to claim that this chapter reproduces that computation or needs its scale.

When a search uses symmetry, each excluded case must be equivalent to a retained one under a proved transformation preserving the property. When a run is partitioned, its jobs must cover the whole universe with no gaps. Checksums can track files; they cannot establish either mathematical equivalence or coverage by themselves.

Exercise. A solver has checked ninety-nine of one hundred jobs, all with no solutions. Is the global search complete? Hint: inspect the missing job's domain. Solution: no. Even if all completed certificates verify, an unchecked part remains. Report the exact covered range and outstanding job.

54.7 Symbolic algebra and generating-function packages

Optional extension; not required to complete the chapter foundation.

Symbolic computation can expand polynomials, derive recurrences, manipulate generating functions, and check proposed identities. Specify the coefficient domain: exact integers, rational numbers, finite fields, and floating-point numbers support different conclusions. Equality after numerical evaluation at a few points is weaker than equality of symbolic coefficients.

Solved generating-function example. Let $b_n$ count independent sets in the path on $n$ vertices. Deleting the final vertex gives $b_n=b_{n-1}+b_{n-2}$ for $n\ge2$, with $b_0=1,b_1=2$. If $B(z)=\sum_{n\ge0}b_nz^n$, coefficient comparison gives

$$(1-z-z^2)B(z)=1+z,\qquad B(z)=\frac{1+z}{1-z-z^2}.$$

The first values are $1,2,3,5,8,13,21$. A package can verify the rational expansion, but the combinatorial deletion argument establishes why it counts these objects at every size. A recurrence guessed from a short table requires a proof or a rigorous finite-certification theorem with its hypotheses checked.

For example, $B(z)+z^6$ has the same coefficients through degree five but gives twenty-two instead of twenty-one at degree six. Thus even another rational generating function can agree with a finite table and later diverge. An apparently compelling fit is still underdetermined.

For a rational identity $P/Q=R/S$, exact cross-multiplication checks $PS=RQ$ as polynomials, while respecting denominators when evaluating at particular arguments. For a formal power-series identity, the denominator must have a nonzero constant term to admit a formal inverse. Branch choices also matter for algebraic equations: a quadratic may have two formal solutions, only one with the correct base coefficient.

The SageMath polynomial-ring documentation makes the base ring explicit. Scope: the chapter's graph experiment uses only exact integers in Python and needs no computer-algebra installation. The general proof of a generating-function identity should be retained independently of a package's simplified display.

Exercise. Is a near-zero floating residual enough to prove an integer polynomial identity? Hint: distinguish rounding error from exact coefficients. Solution: no. Expand and compare exact integer or rational coefficients, or supply a certified numerical bound appropriate to the claim.

54.8 Graph and hypergraph computation libraries

Optional extension; not required to complete the chapter foundation.

Graph libraries provide data structures, traversals, isomorphism methods, and file formats. A result is meaningful only when the library's object type matches the mathematical model: simple versus multigraph, directed versus undirected, labeled versus unlabeled, and explicit versus implicit isolated vertices. A method called “cycle” may return a witness, enumerate some cycles, or enumerate all cycles under a different convention.

Solved cross-check. Import the five-cycle edge list into an undirected simple graph and explicitly add vertices zero through four. A library bipartiteness routine should return false; an edge audit should still find exactly five edges and no triangle. The official NetworkX is_bipartite documentation states the predicate's meaning. Our standard-library experiment does not require that package, but a separately recorded library check can supplement the independent certificate verifier.

Do not identify graph isomorphism by degree sequence alone. An eight-cycle and two disjoint four-cycles both have eight vertices of degree two, and both are triangle-free, but one is connected and the other is not. A canonical-labeling computation must preserve the intended graph type. Primary algorithmic treatment: McKay and Piperno. Omitted prerequisites: canonical augmentation and the proof of an isomorph-free generator's coverage.

A hypergraph has subsets, or hyperedges, that may contain more than two vertices. Under weak two-coloring, each hyperedge must contain both colors. A single three-vertex hyperedge is weakly two-colorable, for example colors $0,0,1$. Replacing it by a triangle and requiring every pair to have different colors makes it impossible to two-color. Clique expansion has changed the constraint.

An incidence graph represents vertices on one side and hyperedges on the other, with membership edges between them. That incidence graph is bipartite by construction, even when the original hypergraph's weak-coloring problem is difficult or infeasible. A bipartiteness call on the incidence graph does not solve hypergraph two-colorability. Verify the original hyperedge constraints directly.

Exercise. What happens if a graph file lists edges but omits isolated vertices? Hint: consider the empty graph on five vertices. Solution: an importer may create zero vertices rather than five, changing the size and any enumeration claim. Record or explicitly create the full vertex set.

54.9 Reproducible experiments and independent verification

Optional extension; not required to complete the chapter foundation.

Reproducibility means another run can reconstruct the inputs, methods, and results. Mathematical accountability additionally requires understanding what those results establish. Retain the exact question, encoding, code, parameter range, complete summaries, witnesses, and verification procedure. For external tools record versions, options, preprocessing, and proof logs. For randomized experiments record the generator, seed, and sampling rule, together with any confidence statement's assumptions.

Solved reproducibility record. The embedded script was run with Python 3.12.14, standard-library imports only, and maximum size five. It examined 1100 masks and returned the witness in Section 54.3. Exported graph bytes use UTF-8 JSON with sorted object keys, no optional whitespace, and the edge list in the stated lexicographic order. The graph payload includes only n and edges; the cycle certificate and environment version are recorded separately.

For that graph payload the SHA-256 digest is 02cabc2e456a07238ad01f157b75da44e51667c171088a2d3a4bc1f609b2f3c6. This identifies the exact labeled serialization, not an isomorphism class. Relabeling the same abstract five-cycle usually changes it. A run with another Python version can legitimately differ in its metadata while retaining identical graph bytes and mathematical counts.

The producer's triangle predicate and the verifier's closed-walk predicate use different representations. For stronger coverage, a separate validation run can classify every graph by adjacency-matrix triangle counts and exhaustive vertex-color assignments. Agreement with the producer across all masks checks more than verifying the single first witness. It remains ordinary computational validation, not a formally certified execution of Python.

If a random experiment estimates the probability of a property from $M$ independent Bernoulli trials, Hoeffding's inequality gives $\Pr(|\widehat p-p|\ge\varepsilon)\le2e^{-2M\varepsilon^2}$. This requires independence and the specified sampling law. Recording a seed makes a run repeatable; it does not itself prove those hypotheses or turn random search into exhaustive coverage. Reusing the same seeded output is not a new independent sample.

Certified LRAT checking provides a stronger formal verification model for supported proof artifacts. Scope: the chapter demonstrates reproducible deterministic enumeration and independent object checks. It does not claim formal certification or cite a digest as a mathematical proof.

Exercise. A rerun gives the same witness but a different total count. Is that enough agreement? Hint: distinguish existence from enumeration. Solution: no. The witness can still refute the conjecture while a counting or coverage error remains. Investigate the full domain, predicates, and stopping rule.

54.10 From computational observation to rigorous conjecture

Optional extension; not required to complete the chapter foundation.

Translate an observation into a quantified statement before trying to prove it. Here the original claim ranges over all finite simple undirected triangle-free graphs and asserts existence of a proper vertex two-coloring. Its five-cycle counterexample invalidates the implication, so a proof attempt must change the claim rather than hide the witness.

Solved corrected theorem. A finite undirected graph is bipartite if and only if it contains no odd cycle. One direction follows from alternating colors around a cycle. For the other, use breadth-first search in each component and color vertices by distance parity. If an edge joins equal-parity vertices, their tree paths plus that edge yield an odd cycle, contradicting the hypothesis. Hence every edge joins opposite colors. This establishes the corrected all-size theorem and explains the algorithm's conflict certificate.

A different structural hypothesis suggested by enumeration is the edge bound for triangle-free graphs, $m\le\lfloor n^2/4\rfloor$. This is the established Mantel theorem, not a new conjecture. Proof: the zero-edge case is immediate. Assume $m\gt0$, so $n\gt0$. For an edge $uv$, the neighbor sets of $u$ and $v$ are disjoint, so $d(u)+d(v)\le n$. Summing over edges gives $\sum_vd(v)^2\le nm$. Cauchy–Schwarz gives $\sum_vd(v)^2\ge(2m)^2/n$. Combining and dividing by the positive quantities yields $m\le n^2/4$. The balanced complete bipartite graph attains the integer bound.

At five vertices the maximum is six, attained by $K_{2,3}$; a five-cycle has five edges. At six vertices the maximum is nine, attained by $K_{3,3}$. Exhaustive enumeration confirms those small optima, but the degree argument proves the bound at every size. The false bipartite implication and the true extremal bound concern related graph properties without being equivalent statements.

For proposed new questions, identify the exact graph class, extremal quantity, and parameter, then inspect current primary literature before labeling them open. A claim already refuted by a small object needs a corrected hypothesis. A claim already proved is a useful rediscovery exercise, not a research novelty. McKay–Piperno and Heule–Kullmann–Marek illustrate computational research methods; their results do not license unrelated conjectures without verification.

Exercise. Does Mantel's theorem imply every triangle-free graph is bipartite? Hint: test the edge inequality on the five-cycle. Solution: no. Its five edges are below the allowed six, so it satisfies the extremal bound while remaining non-bipartite.

Build a reproducible experiment with independent object verification

The investigation brings together complete generation, small counterexample search, exact object certificates, and a general corrected proof. Its application extends to validation of conflict constraints in scheduling or allocation: a solver may propose an assignment, while a separate checker verifies every original constraint and the exported data. Reproducibility ensures the result can be inspected; the logical reduction determines what it proves.

The graph conjecture is deliberately false and the corrected odd-cycle characterization and Mantel bound are established. This is a research-practice investigation, not a claim that those questions remain open. The optional extension changes the finite experiment explicitly and makes no unverified all-size novelty claim.