WOWII 146 / Agent A: formalize graph-square distance and radius

[akakabrian]

Parent: #1

Objective

Formalize the metric identity for the square graph and derive the radius formula needed for Written on the Wall II Conjecture 146.

The verified human proof uses

• d_{G²}(a,b) = ceil(d_G(a,b)/2), represented on naturals as (G.dist a b + 1) / 2;
• graphSquareRadius G = ceil(rad(G)/2).

Target environment

• Lean 4.27.0
• Mathlib v4.27.0
• Upstream Formal Conjectures pinned in this repository's lakefile.toml
• Definitions: SimpleGraph.graphSquare, SimpleGraph.dist, SimpleGraph.radius, and WrittenOnTheWallII.GraphConjecture146.graphSquareRadius

Deliverables

1. A sorry-free lemma equivalent to:

lemma graphSquare_dist (h : G.Connected) (a b : α) :
    (graphSquare G).dist a b = (G.dist a b + 1) / 2

2. A sorry-free radius consequence in the exact repository types; note that SimpleGraph.radius is ℕ∞, while graphSquareRadius is radius.toNat.
3. Unit/regression examples on paths of lengths 1–5.
4. #print axioms audit showing only standard Lean axioms.
5. CI command passing with -DwarningAsError=true.

Proof guidance

• Upper bound: take a G-geodesic and pair consecutive edges to build a walk in graphSquare G.
• Lower bound: map each square-graph edge to a G walk of length at most 2, concatenate, and compare with G.dist.
• Keep disconnected-graph dist = 0 conventions out of the main statement by retaining connectedness.

Commit work to branch wowii-146-proof or provide a cherry-pickable commit.

[akakabrian]

Migrated to the dedicated public repository: akakabrian/WOW-146#2. Closing this duplicate assignment in agent-workflows.

[akakabrian]

Moved to the dedicated public repository: akakabrian/WOW-146#2. Closing this duplicate.