#!/usr/bin/env python3 """Exact/computational attack on Graffiti 292. Statement (Written on the Wall numbering, as independently transcribed in CE10): For connected simple graphs G with girth at least five, min {lambda > 0 : lambda is an adjacency eigenvalue of G} <= |V(G)| / mean(Gr(G)), where Gr_uv = deg(u)deg(v)/((n-1)dist(u,v)) off-diagonal and zero on the diagonal, and mean is over all n^2 entries. The right side is positive. This program computes certified lower bounds on it that expose a normalization mismatch, and searches representative graphs. """ from __future__ import annotations from dataclasses import dataclass from fractions import Fraction import math import networkx as nx import numpy as np EPS = 1e-9 @dataclass(frozen=True) class Evaluation: name: str n: int m: int girth: int | float max_degree: int min_positive_adjacency_eigenvalue: float | None mean_gravity: float rhs: float margin: float | None def graph_girth(graph: nx.Graph) -> int | float: if nx.is_forest(graph): return math.inf best = math.inf for source in graph: distances = {source: 0} parent = {source: None} queue = [source] for vertex in queue: for neighbor in graph[vertex]: if neighbor not in distances: distances[neighbor] = distances[vertex] + 1 parent[neighbor] = vertex queue.append(neighbor) elif parent[vertex] != neighbor: best = min(best, distances[vertex] + distances[neighbor] + 1) return int(best) def gravity_mean_exact(graph: nx.Graph) -> Fraction: if not nx.is_connected(graph): raise ValueError("graph must be connected") n = graph.number_of_nodes() degrees = dict(graph.degree()) total = Fraction(0, 1) for source in graph: distances = nx.single_source_shortest_path_length(graph, source) for target in graph: if source != target: total += Fraction(degrees[source] * degrees[target], (n - 1) * distances[target]) return total / (n * n) def evaluate(name: str, graph: nx.Graph) -> Evaluation: if graph.is_directed() or graph.is_multigraph() or not nx.is_connected(graph): raise ValueError(f"{name}: expected connected simple graph") g = graph_girth(graph) if g < 5: raise ValueError(f"{name}: girth {g} < 5") adjacency = nx.to_numpy_array(graph, dtype=float) eigenvalues = np.linalg.eigvalsh(adjacency) positive = eigenvalues[eigenvalues > EPS] minimum_positive = float(positive[0]) if len(positive) else None mean_exact = gravity_mean_exact(graph) mean_gravity = float(mean_exact) # The one-vertex graph has zero mean gravity. Interpret n/0 as +infinity; # the inequality is then vacuous. All connected graphs with n >= 2 have # positive mean gravity. rhs = math.inf if mean_gravity == 0 else graph.number_of_nodes() / mean_gravity margin = None if minimum_positive is None else minimum_positive - rhs return Evaluation( name=name, n=graph.number_of_nodes(), m=graph.number_of_edges(), girth=g, max_degree=max(dict(graph.degree()).values()), min_positive_adjacency_eigenvalue=minimum_positive, mean_gravity=mean_gravity, rhs=rhs, margin=margin, ) def named_graphs() -> list[tuple[str, nx.Graph]]: constructors = [ ("path_2", lambda: nx.path_graph(2)), ("path_10", lambda: nx.path_graph(10)), ("cycle_5", lambda: nx.cycle_graph(5)), ("cycle_17", lambda: nx.cycle_graph(17)), ("petersen", nx.petersen_graph), ("heawood", nx.heawood_graph), ("pappus", nx.pappus_graph), ("desargues", nx.desargues_graph), ("mobius_kantor", nx.moebius_kantor_graph), ("hoffman_singleton", nx.hoffman_singleton_graph), ] return [(name, constructor()) for name, constructor in constructors] def random_regular_girth_graphs() -> list[tuple[str, nx.Graph]]: found: list[tuple[str, nx.Graph]] = [] for degree, n, trials in [(3, 20, 500), (3, 30, 1000), (4, 30, 2000)]: for seed in range(trials): graph = nx.random_regular_graph(degree, n, seed=seed) if nx.is_connected(graph) and graph_girth(graph) >= 5: found.append((f"random_{degree}reg_n{n}_seed{seed}", graph)) break return found def theorem_bounds(graph: nx.Graph) -> dict[str, Fraction | int]: n = graph.number_of_nodes() m = graph.number_of_edges() delta = max(dict(graph.degree()).values()) # Every off-diagonal gravity entry is at most Delta^2/(n-1), so # mean(Gr) <= Delta^2/n and n/mean(Gr) >= n^2/Delta^2. rhs_lower_from_delta = math.inf if delta == 0 else Fraction(n * n, delta * delta) # Since 2m <= n Delta, the stronger-looking degree-sum bound # mean(Gr) <= (2m)^2/((n-1)n^2) implies: rhs_lower_from_edges = math.inf if m == 0 else Fraction((n - 1) * n**3, (2 * m) ** 2) # Spectral radius <= Delta, hence every positive adjacency eigenvalue <= Delta. return { "n": n, "m": m, "Delta": delta, "rhs_lower_from_delta": rhs_lower_from_delta, "rhs_lower_from_edges": rhs_lower_from_edges, "positive_eigenvalue_upper": delta, } def main() -> None: rows = [] for name, graph in named_graphs() + random_regular_girth_graphs(): row = evaluate(name, graph) rows.append(row) print( f"{row.name:34s} n={row.n:3d} m={row.m:4d} g={str(row.girth):>3s} " f"Delta={row.max_degree:2d} minpos={row.min_positive_adjacency_eigenvalue!s:>20s} " f"meanGr={row.mean_gravity:.12g} rhs={row.rhs:.12g} margin={row.margin!s}" ) bounds = theorem_bounds(graph) if math.isfinite(row.rhs) and row.rhs + 1e-9 < float(bounds["rhs_lower_from_delta"]): raise AssertionError((row, bounds)) if row.min_positive_adjacency_eigenvalue is not None: if row.min_positive_adjacency_eigenvalue > row.max_degree + 1e-8: raise AssertionError((row, bounds)) if row.margin is not None and row.margin > 1e-8: raise AssertionError(f"candidate counterexample found: {row}") # Exhaust all connected graph-atlas graphs (all simple graphs up to 7 vertices). atlas_checked = 0 for index, graph in enumerate(nx.graph_atlas_g()): if graph.number_of_nodes() == 0 or not nx.is_connected(graph): continue if graph_girth(graph) < 5: continue atlas_checked += 1 row = evaluate(f"atlas_{index}", graph) if row.margin is not None and row.margin > 1e-8: raise AssertionError(f"atlas counterexample: {row}") print(f"atlas_checked={atlas_checked}") # Structural proof check on representative graph: RHS >= n^2/Delta^2. # Thus if Delta^3 <= n^2, then RHS >= Delta >= every positive eigenvalue. proved_by_delta = sum( row.max_degree**3 <= row.n**2 for row in rows ) print(f"representatives_proved_by_Delta_cubed_le_n_squared={proved_by_delta}/{len(rows)}") print("OK: no counterexample; normalization yields a broad elementary proof region.") if __name__ == "__main__": main()