feat: add four Meinhold coset graphs Sab(G₂(2), K, D)

Four new coset graphs of G₂(2) with full Sabidussi proofs:

- Meinhold-504 (504v, 24-regular, girth 4) via K = S₄
- Meinhold-576 (576v, 7-regular, girth 6) via K = C₇:C₃
- Meinhold-1344 (1344v, 9-regular, girth 6) via K = C₃×C₃
- Meinhold-2016 (2016v, 6-regular, girth 8) via K = C₆

Each graph is defined via its Sabidussi connection set and G₂(2)
generators on the coset space. Properties proved: connected,
triangle-free, cycle witnesses, and the Sabidussi isomorphism.

Also corrects the Meinhold family table in MeinholdGraphs.lean
(Meinhold-504 is 24-regular, not 6-regular as previously claimed).

Author: RaggedR

Archive.lean

@@ -67,6 +67,10 @@ import Archive.Imo.Imo2024Q6
 import Archive.Imo.Imo2025Q3
 import Archive.KleinSurface
 import Archive.Kuratowski
+import Archive.Meinhold1344
+import Archive.Meinhold2016
+import Archive.Meinhold504
+import Archive.Meinhold576
 import Archive.MeinholdGraphs
 import Archive.MinimalSheffer
 import Archive.MiuLanguage.Basic

Archive/Meinhold1344.lean

@@ -9,13 +9,12 @@ import Mathlib.Combinatorics.SimpleGraph.Finite
 import Mathlib.Combinatorics.SimpleGraph.SabidussiWitness
 
 /-!
-# Meinhold-72: quotient of the Clayworth graph via PSL(3,2)
+# Meinhold-72: Sabidussi coset graph Sab(G₂(2), PSL(3,2))
 
-The **Meinhold-72** graph (72 vertices, 7-regular, girth 4, diameter 5) is the
-block quotient of the Clayworth graph (4032 vertices, cubic) by the intermediate
-subgroup K ≅ PSL(3,2) of order 168.
-
-`Aut(Meinhold-72) = G₂(2)`, order 12096.
+The **Meinhold-72** graph (72 vertices, 7-regular, girth 4) is the coset graph
+`Sab(G₂(2), PSL(3,2), D)` with `72 = 12096/168` vertices. Equivalently, it is
+the block quotient of the Clayworth graph (4032 vertices, cubic) via the natural
+projection G₂(2)/C₃ → G₂(2)/PSL(3,2), with uniform fibers of size 56.
 
 Named after Nick Meinhold, co-founder of Imagineering Melbourne.
 
@@ -31,15 +30,17 @@ Furthermore, the three order-192 overgroups of C₃ have structure
 
 ## The Meinhold family
 
-Five quotients of Clayworth named for their sparsity and symmetry:
+Five coset graphs `Sab(G₂(2), K, D)` for intermediate subgroups C₃ ≤ K ≤ G₂(2):
+
+| Graph | V | Deg | Girth | K | |K| |
+|-------|-----|-----|-------|-------|-----|
+| Meinhold-72 | 72 | 7 | 4 | PSL(3,2) | 168 |
+| Meinhold-504 | 504 | 24 | 4 | S₄ | 24 |
+| Meinhold-576 | 576 | 7 | 6 | C₇:C₃ | 21 |
+| Meinhold-1344 | 1344 | 9 | 6 | C₃×C₃ | 9 |
+| Meinhold-2016 | 2016 | 6 | 8 | C₆ | 6 |
 
-| Graph | V | Deg | Girth | Aut | Via K |
-|-------|-----|-----|-------|-----|-------|
-| Meinhold-72 | 72 | 7 | 4 | G₂(2) | PSL(3,2) |
-| Meinhold-504 | 504 | 6 | 6 | G₂(2) | S₄ |
-| Meinhold-576 | 576 | 7 | 6 | G₂(2) | C₇:C₃ |
-| Meinhold-1344 | 1344 | 9 | 6 | 4·G₂(2) | C₃×C₃ |
-| Meinhold-2016 | 2016 | 6 | 8 | G₂(2) | C₆ |
+Each is defined in its own file: `Archive.MeinholdNNN`.
 
 ## Visualizations