@[irreducible]

def Hex.PermGroup.Search.Bounded.visit {n : Nat} {G : Group n} {P : Predicate n} {budget : Budget} (C : Constraint G P) (Q : Tester P budget) (t : Node G) (a : Accumulator G P) (m : Meter budget) : Result C t a budget

The bounded traversal uses the same checked node decomposition and coverage rules as exact search. Every stopping point retains a verified lower bound; only a complete traversal returns a completeness certificate.

Equations

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

inductive Hex.PermGroup.Search.Outcome {n : Nat} {G : Group n} {P : Predicate n} (C : Constraint G P) (budget : Budget) : Type

Incomplete subgroup output has only lower-bound semantics. Its own chain is checked, but it has no certificate claiming equality to the search result.

• complete {n : Nat} {G : Group n} {P : Predicate n} {C : Constraint G P} {budget : Budget} (solution : Solution C) (meter : Meter budget) : Outcome C budget
• incomplete {n : Nat} {G : Group n} {P : Predicate n} {C : Constraint G P} {budget : Budget} (lowerBound : Accumulator G P) (failure : Exhausted budget) : Outcome C budget

def Hex.PermGroup.Search.solveBudgeted {n : Nat} (budget : Budget) {G : Group n} {P : Predicate n} (C : Constraint G P) (Q : Tester P budget) : Outcome C budget

Budgeted exact subgroup search. The leaf evaluator shares the same sift counter with prefix coverage and redundant-generator checks.

Equations

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