def Hex.PermGroup.Blocks.Invariant {n : Nat} (S : Array (Perm n)) (R : Fin n → Fin n → Prop) : Prop

A relation preserved by every supplied generator.

Equations

• Hex.PermGroup.Blocks.Invariant S R = ∀ (s : Hex.Perm n), s ∈ S → ∀ (x y : Fin n), R x y → R (s.get x) (s.get y)

structure Hex.PermGroup.Blocks.Admissible {n : Nat} (S : Array (Perm n)) (seeds : List (Fin n × Fin n)) (R : Fin n → Fin n → Prop) : Prop

The equivalence relations admitted by a seeded block problem.

• equivalence : Equivalence R
• invariant : Invariant S R
• seeds (q : Fin n × Fin n) : q ∈ seeds → R q.fst q.snd

def Hex.PermGroup.Blocks.Forced {n : Nat} (S : Array (Perm n)) (seeds : List (Fin n × Fin n)) (p : Partition n) (x y : Fin n) : Prop

A merge is justified by a seed or by the image of two points already in the same block. Its preimage is obtained from the checked permutation.

Equations

• Hex.PermGroup.Blocks.Forced S seeds p x y = ((x, y) ∈ seeds ∨ ∃ (i : Fin S.size), p.Same (S[↑i].inv.get x) (S[↑i].inv.get y))

@[instance_reducible]

instance Hex.PermGroup.Blocks.instDecidableForced {n : Nat} (S : Array (Perm n)) (seeds : List (Fin n × Fin n)) (p : Partition n) (x y : Fin n) : Decidable (Forced S seeds p x y)

Equations

• Hex.PermGroup.Blocks.instDecidableForced S seeds p x y = { decide := decide ((x, y) ∈ seeds) || decide (∃ (i : Fin S.size), p.Same (S[↑i].inv.get x) (S[↑i].inv.get y)), reflects_decide := ⋯ }

theorem Hex.PermGroup.Blocks.Forced.mono {n : Nat} {S : Array (Perm n)} {seeds : List (Fin n × Fin n)} {p q : Partition n} (h : p.Refines q.Same) {x y : Fin n} (hf : Forced S seeds p x y) : Forced S seeds q x y

theorem Hex.PermGroup.Blocks.Forced.sound {n : Nat} {S : Array (Perm n)} {seeds : List (Fin n × Fin n)} {p : Partition n} {R : Fin n → Fin n → Prop} (hR : Admissible S seeds R) (hp : p.Refines R) {x y : Fin n} (hf : Forced S seeds p x y) : R x y

def Hex.PermGroup.Blocks.checkInvariant {n : Nat} (S : Array (Perm n)) (p : Partition n) : Bool

One test per point and generator suffices: a point's image must share a block with its representative's image. No pair table is allocated.

Equations

• Hex.PermGroup.Blocks.checkInvariant S p = decide (∀ (i : Fin S.size) (x : Fin n), p.Same (S[↑i].get x) (S[↑i].get p.labels[↑x]))

theorem Hex.PermGroup.Blocks.checkInvariant_iff {n : Nat} (S : Array (Perm n)) (p : Partition n) : checkInvariant S p = true ↔ Invariant S p.Same

def Hex.PermGroup.Blocks.replay {n : Nat} (S : Array (Perm n)) (seeds : List (Fin n × Fin n)) (p : Partition n) : List (Fin n × Fin n) → Option (Partition n)

Replay only effective forced unions. An untrusted trace may not introduce an arbitrary merge, even if its final partition happens to be invariant.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Blocks.replay S seeds p [] = some p

theorem Hex.PermGroup.Blocks.replay_append {n : Nat} (S : Array (Perm n)) (seeds : List (Fin n × Fin n)) (p : Partition n) (xs ys : List (Fin n × Fin n)) : replay S seeds p (xs ++ ys) = (replay S seeds p xs).bind fun (q : Partition n) => replay S seeds q ys

theorem Hex.PermGroup.Blocks.replay_least {n : Nat} {S : Array (Perm n)} {seeds trace : List (Fin n × Fin n)} {p q : Partition n} (h : replay S seeds p trace = some q) {R : Fin n → Fin n → Prop} (hR : Admissible S seeds R) (hp : p.Refines R) : q.Refines R

theorem Hex.PermGroup.Blocks.replay_length {n : Nat} {S : Array (Perm n)} {seeds trace : List (Fin n × Fin n)} {p q : Partition n} (h : replay S seeds p trace = some q) : q.roots.length + trace.length = p.roots.length

A successful replay records exactly one union per deleted root.

def Hex.PermGroup.Blocks.check {n : Nat} (S : Array (Perm n)) (seeds : List (Fin n × Fin n)) (p : Partition n) (trace : List (Fin n × Fin n)) : Bool

Completeness checks both the input seeds and terminal generator closure, in addition to replaying the forced unions from the discrete partition.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.PermGroup.Blocks.check_spec {n : Nat} {S : Array (Perm n)} {seeds trace : List (Fin n × Fin n)} {p : Partition n} (h : check S seeds p trace = true) : Admissible S seeds p.Same ∧ ∀ (R : Fin n → Fin n → Prop), Admissible S seeds R → p.Refines R

The checked partition is admissible and refines every admissible relation. The second conclusion is the minimality obligation.