theorem
Hex.GraphIso.Nauty.oneCell_flip_data
{n : Nat}
{ctx : Ctx n}
{st : RefineSt n}
{level tc te oU oV : Nat}
(hIt : IterOk ctx level st)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (z w : Nat), z < n → w < n → ctx.g[z]!.mem w = ctx.g[w]!.mem z)
(hloop : ∀ (z : Nat), z < n → ctx.g[z]!.mem z = false)
(hE : Equitable ctx level st.lab st.ptn)
(hC : (tc, te) ∈ cells st.ptn level n)
(hm : te + 1 - tc ≤ 5)
(hsing : ∀ (q : Nat × Nat), q ∈ cells st.ptn level n → q ≠ (tc, te) → q.snd = q.fst)
(hoU : oU ≤ te - tc)
(hoV : oV ≤ te - tc)
(hne : oU ≠ oV)
:
The flip data at a nontrivial cell of size at most five whose companions are all singletons: the differ classification of the two chosen members is forced by the window row sums, and the flip is the bare transposition or the crossed double swap.
theorem
Hex.GraphIso.Nauty.twoTriple_sw2
{n : Nat}
{ctx : Ctx n}
{st : RefineSt n}
{level tc d2 oU oV pa pb : Nat}
(hIt : IterOk ctx level st)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (z w : Nat), z < n → w < n → ctx.g[z]!.mem w = ctx.g[w]!.mem z)
(hloop : ∀ (z : Nat), z < n → ctx.g[z]!.mem z = false)
(hE : Equitable ctx level st.lab st.ptn)
(hT1 : (tc, tc + 2) ∈ cells st.ptn level n)
(hT2 : (d2, d2 + 2) ∈ cells st.ptn level n)
(hT12 : tc ≠ d2)
(hsing : ∀ (q : Nat × Nat), q ∈ cells st.ptn level n → q ≠ (tc, tc + 2) → q ≠ (d2, d2 + 2) → q.snd = q.fst)
(hoU : oU ≤ 2)
(hoV : oV ≤ 2)
(hne : oU ≠ oV)
(hpa : pa ≤ 2)
(hpb : pb ≤ 2)
(hpab : pa ≠ pb)
(hfixT1 :
∀ (w : Nat),
w ≤ 2 →
w ≠ oU →
w ≠ oV →
ctx.g[st.lab[tc + w]!]!.mem st.lab[tc + oU]! = ctx.g[st.lab[tc + w]!]!.mem st.lab[tc + oV]! ∧ ctx.g[st.lab[tc + w]!]!.mem st.lab[d2 + pa]! = ctx.g[st.lab[tc + w]!]!.mem st.lab[d2 + pb]!)
(hfixT2 :
∀ (w : Nat),
w ≤ 2 →
w ≠ pa →
w ≠ pb →
ctx.g[st.lab[d2 + w]!]!.mem st.lab[tc + oU]! = ctx.g[st.lab[d2 + w]!]!.mem st.lab[tc + oV]! ∧ ctx.g[st.lab[d2 + w]!]!.mem st.lab[d2 + pa]! = ctx.g[st.lab[d2 + w]!]!.mem st.lab[d2 + pb]!)
(hc1 : ctx.g[st.lab[tc + oU]!]!.mem st.lab[d2 + pa]! = ctx.g[st.lab[tc + oV]!]!.mem st.lab[d2 + pb]!)
(hc2 : ctx.g[st.lab[tc + oU]!]!.mem st.lab[d2 + pb]! = ctx.g[st.lab[tc + oV]!]!.mem st.lab[d2 + pa]!)
:
The cross-cell double swap: the two chosen members of the target triple swap together with their partners in the other triple.
theorem
Hex.GraphIso.Nauty.twoTriple_sw1
{n : Nat}
{ctx : Ctx n}
{st : RefineSt n}
{level tc d2 oU oV : Nat}
(hIt : IterOk ctx level st)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (z w : Nat), z < n → w < n → ctx.g[z]!.mem w = ctx.g[w]!.mem z)
(hloop : ∀ (z : Nat), z < n → ctx.g[z]!.mem z = false)
(hE : Equitable ctx level st.lab st.ptn)
(hT1 : (tc, tc + 2) ∈ cells st.ptn level n)
(hT2 : (d2, d2 + 2) ∈ cells st.ptn level n)
(hT12 : tc ≠ d2)
(hsing : ∀ (q : Nat × Nat), q ∈ cells st.ptn level n → q ≠ (tc, tc + 2) → q ≠ (d2, d2 + 2) → q.snd = q.fst)
(hoU : oU ≤ 2)
(hoV : oV ≤ 2)
(hne : oU ≠ oV)
(huni :
∀ (q : Nat), q ≤ 2 → ctx.g[st.lab[tc + oU]!]!.mem st.lab[d2 + q]! = ctx.g[st.lab[tc + oV]!]!.mem st.lab[d2 + q]!)
:
The uniform cross-count route: the other triple's bits do not distinguish the two chosen members, so the bare transposition suffices.
theorem
Hex.GraphIso.Nauty.twoTriple_flip_data
{n : Nat}
{ctx : Ctx n}
{st : RefineSt n}
{level tc d2 oU oV : Nat}
(hIt : IterOk ctx level st)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (z w : Nat), z < n → w < n → ctx.g[z]!.mem w = ctx.g[w]!.mem z)
(hloop : ∀ (z : Nat), z < n → ctx.g[z]!.mem z = false)
(hE : Equitable ctx level st.lab st.ptn)
(hT1 : (tc, tc + 2) ∈ cells st.ptn level n)
(hT2 : (d2, d2 + 2) ∈ cells st.ptn level n)
(hT12 : tc ≠ d2)
(hsing : ∀ (q : Nat × Nat), q ∈ cells st.ptn level n → q ≠ (tc, tc + 2) → q ≠ (d2, d2 + 2) → q.snd = q.fst)
(hoU : oU ≤ 2)
(hoV : oV ≤ 2)
(hne : oU ≠ oV)
:
The flip data at a triple target beside a second triple, all other
cells singletons: the constant cross-count is uniform (0 or 3,
reducing to the bare transposition) or matched (1 or 2, pairing
each chosen member with its unique minority partner and swapping the
partners along).
theorem
Hex.GraphIso.Nauty.fourPair_sw2
{n : Nat}
{ctx : Ctx n}
{st : RefineSt n}
{level tc d2 oU oV w1 w2 : Nat}
(hIt : IterOk ctx level st)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (z w : Nat), z < n → w < n → ctx.g[z]!.mem w = ctx.g[w]!.mem z)
(hloop : ∀ (z : Nat), z < n → ctx.g[z]!.mem z = false)
(hE : Equitable ctx level st.lab st.ptn)
(hC : (tc, tc + 3) ∈ cells st.ptn level n)
(hP : (d2, d2 + 1) ∈ cells st.ptn level n)
(hCP : tc ≠ d2)
(hsing : ∀ (q : Nat × Nat), q ∈ cells st.ptn level n → q ≠ (tc, tc + 3) → q ≠ (d2, d2 + 1) → q.snd = q.fst)
(hoU : oU ≤ 3)
(hoV : oV ≤ 3)
(hw1 : w1 ≤ 3)
(hw2 : w2 ≤ 3)
(hUV : oU ≠ oV)
(hUw1 : oU ≠ w1)
(hUw2 : oU ≠ w2)
(hVw1 : oV ≠ w1)
(hVw2 : oV ≠ w2)
(h12 : w1 ≠ w2)
(hPfix :
∀ (q : Nat),
q ≤ 1 →
ctx.g[st.lab[d2 + q]!]!.mem st.lab[tc + oU]! = ctx.g[st.lab[d2 + q]!]!.mem st.lab[tc + oV]! ∧ ctx.g[st.lab[d2 + q]!]!.mem st.lab[tc + w1]! = ctx.g[st.lab[d2 + q]!]!.mem st.lab[tc + w2]!)
:
The double-swap route at a four-cell beside a pair.
theorem
Hex.GraphIso.Nauty.fourPair_sw3
{n : Nat}
{ctx : Ctx n}
{st : RefineSt n}
{level tc d2 oU oV w1 w2 : Nat}
(hIt : IterOk ctx level st)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (z w : Nat), z < n → w < n → ctx.g[z]!.mem w = ctx.g[w]!.mem z)
(hloop : ∀ (z : Nat), z < n → ctx.g[z]!.mem z = false)
(hE : Equitable ctx level st.lab st.ptn)
(hC : (tc, tc + 3) ∈ cells st.ptn level n)
(hP : (d2, d2 + 1) ∈ cells st.ptn level n)
(hCP : tc ≠ d2)
(hsing : ∀ (q : Nat × Nat), q ∈ cells st.ptn level n → q ≠ (tc, tc + 3) → q ≠ (d2, d2 + 1) → q.snd = q.fst)
(hoU : oU ≤ 3)
(hoV : oV ≤ 3)
(hw1 : w1 ≤ 3)
(hw2 : w2 ≤ 3)
(hUV : oU ≠ oV)
(hUw1 : oU ≠ w1)
(hUw2 : oU ≠ w2)
(hVw1 : oV ≠ w1)
(hVw2 : oV ≠ w2)
(h12 : w1 ≠ w2)
(hUV0 : ctx.g[st.lab[tc + oU]!]!.mem st.lab[d2 + 0]! = ctx.g[st.lab[tc + oV]!]!.mem st.lab[d2 + 1]!)
(hUV1 : ctx.g[st.lab[tc + oU]!]!.mem st.lab[d2 + 1]! = ctx.g[st.lab[tc + oV]!]!.mem st.lab[d2 + 0]!)
(hW0 : ctx.g[st.lab[tc + w1]!]!.mem st.lab[d2 + 0]! = ctx.g[st.lab[tc + w2]!]!.mem st.lab[d2 + 1]!)
(hW1 : ctx.g[st.lab[tc + w1]!]!.mem st.lab[d2 + 1]! = ctx.g[st.lab[tc + w2]!]!.mem st.lab[d2 + 0]!)
:
The triple-swap route at a four-cell beside a pair: the chosen members cross the pair coherently, as they do on opposite sides of a matched split.
theorem
Hex.GraphIso.Nauty.fourPair_flip_data
{n : Nat}
{ctx : Ctx n}
{st : RefineSt n}
{level tc d2 oU oV : Nat}
(hIt : IterOk ctx level st)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (z w : Nat), z < n → w < n → ctx.g[z]!.mem w = ctx.g[w]!.mem z)
(hloop : ∀ (z : Nat), z < n → ctx.g[z]!.mem z = false)
(hE : Equitable ctx level st.lab st.ptn)
(hC : (tc, tc + 3) ∈ cells st.ptn level n)
(hP : (d2, d2 + 1) ∈ cells st.ptn level n)
(hCP : tc ≠ d2)
(hsing : ∀ (q : Nat × Nat), q ∈ cells st.ptn level n → q ≠ (tc, tc + 3) → q ≠ (d2, d2 + 1) → q.snd = q.fst)
(hoU : oU ≤ 3)
(hoV : oV ≤ 3)
(hne : oU ≠ oV)
:
The flip data at a four-cell target beside a pair, all other cells singletons.
theorem
Hex.GraphIso.Nauty.pairFour_sw1
{n : Nat}
{ctx : Ctx n}
{st : RefineSt n}
{level tc d2 qU qV : Nat}
(hIt : IterOk ctx level st)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (z w : Nat), z < n → w < n → ctx.g[z]!.mem w = ctx.g[w]!.mem z)
(hloop : ∀ (z : Nat), z < n → ctx.g[z]!.mem z = false)
(hE : Equitable ctx level st.lab st.ptn)
(hC : (tc, tc + 3) ∈ cells st.ptn level n)
(hP : (d2, d2 + 1) ∈ cells st.ptn level n)
(hCP : tc ≠ d2)
(hsing : ∀ (q : Nat × Nat), q ∈ cells st.ptn level n → q ≠ (tc, tc + 3) → q ≠ (d2, d2 + 1) → q.snd = q.fst)
(hqU : qU ≤ 1)
(hqV : qV ≤ 1)
(hqne : qU ≠ qV)
(huni :
∀ (o : Nat), o ≤ 3 → ctx.g[st.lab[tc + o]!]!.mem st.lab[d2 + qU]! = ctx.g[st.lab[tc + o]!]!.mem st.lab[d2 + qV]!)
:
The transposition route at a pair target beside a four-cell.
theorem
Hex.GraphIso.Nauty.pairFour_flip_data
{n : Nat}
{ctx : Ctx n}
{st : RefineSt n}
{level tc d2 qU qV : Nat}
(hIt : IterOk ctx level st)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (z w : Nat), z < n → w < n → ctx.g[z]!.mem w = ctx.g[w]!.mem z)
(hloop : ∀ (z : Nat), z < n → ctx.g[z]!.mem z = false)
(hE : Equitable ctx level st.lab st.ptn)
(hC : (tc, tc + 3) ∈ cells st.ptn level n)
(hP : (d2, d2 + 1) ∈ cells st.ptn level n)
(hCP : tc ≠ d2)
(hsing : ∀ (q : Nat × Nat), q ∈ cells st.ptn level n → q ≠ (tc, tc + 3) → q ≠ (d2, d2 + 1) → q.snd = q.fst)
(hqU : qU ≤ 1)
(hqV : qV ≤ 1)
(hqne : qU ≠ qV)
:
The flip data at a pair target beside a four-cell, all other cells singletons.
theorem
Hex.GraphIso.Nauty.defect4_flip_data
{n : Nat}
{ctx : Ctx n}
{st : RefineSt n}
{level tc te oU oV : Nat}
(hIt : IterOk ctx level st)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (z w : Nat), z < n → w < n → ctx.g[z]!.mem w = ctx.g[w]!.mem z)
(hloop : ∀ (z : Nat), z < n → ctx.g[z]!.mem z = false)
(hE : Equitable ctx level st.lab st.ptn)
(hdef : n - (cells st.ptn level n).length ≤ 4)
(hT : (tc, te) ∈ cells st.ptn level n)
(hoU : oU ≤ te - tc)
(hoV : oV ≤ te - tc)
(hne : oU ≠ oV)
:
Flip data at every cell of a partition whose defect is at most four. This is the shape the cheapautom guard's second branch admits; it dispatches to the pair and triple routes of the first branch together with the four exotic routes.