Adinkra formalization — mathlib contribution proposal

Stream: mathlib4

[reager]

I have a Lean4 formalization of Adinkras (combinatorial structures from supersymmetry) that I'd like to contribute to mathlib. Looking for feedback on:

1. API design: Predicate on SimpleGraph (like IsSRGWith) vs bundled structure?
2. Namespace: Mathlib.Combinatorics.SimpleGraph.Adinkra?
3. Scope: Core definitions + qOp theorems, or include equivalence proofs?

Current formalization:

• Uses mathlib's EdgeLabeling for coloring/dashing
• IsChromotopology (base structure: bipartite N-regular graph with N-edge-coloring + 4-cycle axiom)
• IsAdinkra (chromotopology + odd dashing axiom)
• qOp operators with commutativity proof
• ~1370 lines total, 5 files, no sorries
• Code: GitHub: adinkra-lean4

Key definitions:

/-- A chromotopology is a connected bipartite N-regular graph with N-edge-coloring
    satisfying the 4-cycle axiom. -/
structure SimpleGraph.IsChromotopology (G : SimpleGraph V) (N : ℕ)
    (c : EdgeColoring V G N) : Prop where
  connected : G.Connected
  bipartite : G.IsBipartite
  regular : ∀ v, (G.neighborFinset v).card = N
  colorRegular : IsColorRegular G N c
  fourCycleAxiom : ∀ i j : Fin N, i ≠ j → ∀ v : V, ∃! cyc, ...

/-- An Adinkra is a chromotopology with dashing satisfying odd 4-cycle condition. -/
structure SimpleGraph.IsAdinkra (G : SimpleGraph V) (N : ℕ)
    (c : EdgeColoring V G N) (d : EdgeDashing V G) : Prop where
  chromotopology : G.IsChromotopology N c
  oddDashing : ∀ cyc : TwoColoredFourCycle G N c, cyc.dashingSum d = 1

References:

• Zhang (2011), "Adinkras for Mathematicians" [arXiv:1111.6055]
• Eager et al. (2024), "Adinkras and Pure Spinors" [arXiv:2404.07167]

The code is available at https://github.com/rdeager/adinkra-lean4 for review.

[Yury G. Kudryashov]

Did you use AI tools to (a) write the code; (b) write this post? Either way, this should be disclosed.

[Yury G. Kudryashov]

Also, please don't put all your post in a code block and turn references into actual Markdown links to improve readability.

[reager]

Thank you. I am learning how to use Zulip. Authorship of all .lean files is clearly indicated.

[Kim Morrison]

I think this material is too specialized to go in Mathlib: it seems unlikely anyone will build on it.