docs: specify verified graph canonical labelling

[kim-em]

Summary

• specify the Mathlib-free ordered-coloured graph representation, canonical-form biconditional, bounded certificate checkers, and graph_iso tactic
• specify the Mathlib SimpleGraph correspondence and ground-term tactic extension
• pin exact nauty 2.9.3 conformance semantics, fixtures, hard families, and benchmark comparisons
• require a Petersen-graph manual example covering positive, negative, ordered-colour, and distinct-vertex-type goals
• defer complete automorphism-group generators to a later extension

Independent review

A Fable review checked theorem soundness, the tactic trust boundary, nauty source details and fixture counts, library separation, and the manual example. Its actionable findings were incorporated, including bounded positive search, precise indexed-colour claims, artifact mirroring, colour-sorted reference enumeration, and positive coloured manual coverage.

Validation

• git diff --cached --check
• Markdown parsing with markdown-it for all four changed files
• relative link and heading checks
• exhaustive fixture-count arithmetic checked independently

Documentation only; no Lean source or CI workflow changes.