inductive Hex.PermGroup.Search.Certificate (Reason : Type) : Type

Every branch is either expanded completely, rejected by a replayable constraint reason, checked at a leaf, or contained in the final subgroup.

• branch {Reason : Type} (children : Array (Certificate Reason)) : Certificate Reason
• rejected {Reason : Type} (reason : Reason) : Certificate Reason
• covered {Reason : Type} : Certificate Reason
• leaf {Reason : Type} : Certificate Reason

@[irreducible]

def Hex.PermGroup.Search.checkTree {n : Nat} {G : Group n} {P : Predicate n} (C : Constraint G P) (K : Group n) (t : Node G) (certificate : Certificate C.Reason) : Bool

Reconstruct child choices from the checked chain, rejecting missing or extra branches and validating all pruning against the final result group.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Search.checkTree C K t (Hex.PermGroup.Search.Certificate.rejected reason) = C.reject t reason
• Hex.PermGroup.Search.checkTree C K t Hex.PermGroup.Search.Certificate.covered = t.covered K

theorem Hex.PermGroup.Search.checkTree_branch {n : Nat} {G : Group n} {P : Predicate n} (C : Constraint G P) (K : Group n) (t : Node G) {level : Level n} {tail : Chain n} (hs : t.suffix = Chain.cons level tail) (children : Array (Certificate C.Reason)) : checkTree C K t (Certificate.branch children) = if hc : children.size = level.orbit.points.size then decide (∀ (i : Fin level.orbit.points.size), checkTree C K (t.child hs i) children[↑i] = true) else false

theorem Hex.PermGroup.Search.checkTree_branch_leaf {n : Nat} {G : Group n} {P : Predicate n} (C : Constraint G P) (K : Group n) (t : Node G) {S : Array (Perm n)} {words : Vector Program S.size} (hs : t.suffix = Chain.leaf S words) (children : Array (Certificate C.Reason)) : checkTree C K t (Certificate.branch children) = false

theorem Hex.PermGroup.Search.checkTree_sound {n : Nat} {G : Group n} {P : Predicate n} (C : Constraint G P) (K : Group n) (t : Node G) (certificate : Certificate C.Reason) (hc : checkTree C K t certificate = true) (p : Perm n) (hp : t.Contains p) (hP : P.test p = true) : Generated K.generators p

Replay accounts for every satisfying completion of a node.

theorem Hex.PermGroup.Search.checkTree_mono {n : Nat} {G : Group n} {P : Predicate n} (C : Constraint G P) (t : Node G) (certificate : Certificate C.Reason) {K L : Group n} (hkl : K.IsSubgroup L) (hc : checkTree C K t certificate = true) : checkTree C L t certificate = true

A certificate checked against an intermediate subgroup remains valid when that subgroup grows; earlier coverage claims can be replayed against the final one.

def Hex.PermGroup.Search.checkSearch {n : Nat} {G : Group n} {P : Predicate n} (C : Constraint G P) (K : Group n) (certificate : Certificate C.Reason) : Bool

A checked result subgroup and a complete account of the original search tree are both required; checking the result's chain alone is insufficient.

Equations

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

theorem Hex.PermGroup.Search.checkSearch_spec {n : Nat} {G : Group n} {P : Predicate n} (C : Constraint G P) (K : Group n) (certificate : Certificate C.Reason) (h : checkSearch C K certificate = true) (p : Perm n) : Generated K.generators p ↔ Generated G.generators p ∧ P.test p = true