@[reducible, inline]

abbrev Hex.PermGroup.Search.CheckedBool (expected : Bool) : Type

Equations

• Hex.PermGroup.Search.CheckedBool expected = { value : Bool // value = expected }

def Hex.PermGroup.Execution.Meter.sift {budget : Budget} {n : Nat} (m : Meter budget) (G : Group n) (p : Perm n) : Measured budget (Search.CheckedBool (G.contains p))

Charge each visited level and permutation allocation in a membership query.

Equations

• m.sift G p = m.execute do let result ← G.chain.siftBudgeted 0 p pure ⟨result.val.accepted, ⋯⟩

@[irreducible]

def Hex.PermGroup.Search.siftFrom {budget : Budget} {n : Nat} (G : Group n) (size : Nat) (values : Fin size → Perm n) (imageCost start : Nat) : Execution.Run budget (CheckedBool (decide (∀ (i : Fin size), start ≤ ↑i → G.contains (values i) = true)))

Query a finite family without materializing it. The caller supplies the permutation-image reservation needed to evaluate one entry of the family.

Equations

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

def Hex.PermGroup.Execution.Meter.allSifts {budget : Budget} {n : Nat} (m : Meter budget) (G : Group n) (size : Nat) (values : Fin size → Perm n) (imageCost : Nat := 0) : Measured budget (Search.CheckedBool (decide (∀ (i : Fin size), G.contains (values i) = true)))

Check a finite generator family, stopping at its first failed membership query or exhausted reservation. Image costs cover any generated query values.

Equations

• m.allSifts G size values imageCost = m.execute do let result ← Hex.PermGroup.Search.siftFrom G size values imageCost 0 pure ⟨result.val, ⋯⟩

def Hex.PermGroup.Search.Node.coveredBudgeted {n : Nat} {budget : Budget} {G : Group n} (t : Node G) (K : Group n) (m : Meter budget) : Measured budget (CheckedBool (t.covered K))

Coverage requires both the prefix and every suffix generator. A partial family check cannot certify coverage or its negation.

Equations

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

@[reducible, inline]

abbrev Hex.PermGroup.Search.Evaluator {n : Nat} (test : Perm n → Bool) (budget : Budget) : Type

A budgeted leaf evaluator retains the exact executable predicate. The standard evaluators count its membership queries in the shared meter.

Equations

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

@[reducible, inline]

abbrev Hex.PermGroup.Search.Tester {n : Nat} (P : Predicate n) (budget : Budget) : Type

Equations

• Hex.PermGroup.Search.Tester P budget = Hex.PermGroup.Search.Evaluator P.test budget

def Hex.PermGroup.Search.Evaluator.pure {n : Nat} {budget : Budget} (test : Perm n → Bool) : Evaluator test budget

Equations

• Hex.PermGroup.Search.Evaluator.pure test p meter = Hex.PermGroup.Execution.Measured.ok ⟨test p, ⋯⟩ meter

def Hex.PermGroup.Search.Tester.pure {n : Nat} {budget : Budget} (P : Predicate n) : Tester P budget

Predicates containing no membership queries can use this evaluator.

Equations

• Hex.PermGroup.Search.Tester.pure P = Hex.PermGroup.Search.Evaluator.pure P.test

def Hex.PermGroup.Search.Tester.subgroup {n : Nat} {budget : Budget} (H : Group n) : Tester (Predicate.subgroup H) budget

Equations

• Hex.PermGroup.Search.Tester.subgroup H p meter = meter.sift H p

def Hex.PermGroup.Search.Pruner.refineBudgeted {n : Nat} {budget : Budget} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) (t : Node G) (m : Meter budget) : Measured budget (Option { r : C.Reason // C.reject t r = true })

Each attempted pruning reason is charged separately. Completing the scan without finding a reason allows traversal to continue; exhausting it does not.

Equations

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