@[reducible, inline]

abbrev Hex.PermGroup.Build.Computation {α : Type} (budget : Execution.Budget) (value : α) : Type

A successful bounded computation retains the exact result of its unbounded counterpart. The equality is erased; it never runs the reference computation.

Equations

• Hex.PermGroup.Build.Computation budget value = Hex.PermGroup.Execution.Run budget { result : α // result = value }

def Hex.PermGroup.Build.scanBudgeted {n base : Nat} {S : Array (Perm n)} {ι : Type} {budget : Execution.Budget} (extend : Extender n base) (bounded : (T : Array (Perm n)) → (c : Construction T base) → (p : Perm n) → (h : Chain.Fixed base (T.push p)) → Computation budget (extend T c p h)) (family : ι → Candidate S base) (wordSize : ι → Nat) (s : State S base) (is : List ι) : Computation budget (State.scan extend family s is)

Stream the same Schreier candidates as State.scan. Every candidate reserves its permutation work before evaluation, and its word only after a failed sift. The recursive extender uses the caller's meter.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Build.scanBudgeted extend bounded family wordSize s [] = pure ⟨s, ⋯⟩

def Hex.PermGroup.Build.completeBudgeted {n base : Nat} {S : Array (Perm n)} {budget : Execution.Budget} (hbase : base < n) (normal : Normalized S) (hf : Chain.Fixed base S) (orbit : { c : Orbit n // Orbit.Valid normal.generators ⟨base, hbase⟩ c }) (extend : Extender n (base + 1)) (bounded : (T : Array (Perm n)) → (c : Construction T (base + 1)) → (p : Perm n) → (h : Chain.Fixed (base + 1) (T.push p)) → Computation budget (extend T c p h)) (initial : State normal.generators (base + 1)) : Computation budget (complete hbase normal hf orbit extend initial)

Reserve the work of one level scan and assemble it, as complete does.

Equations

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

def Hex.PermGroup.Build.normalizeBudgeted {n : Nat} {budget : Execution.Budget} (S : Array (Perm n)) : Execution.Run budget { normal : Normalized S // normal = normalize S }

Reserve normalization work in whole bounded batches.

Equations

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

def Hex.PermGroup.Build.orbitBudgeted {n : Nat} {budget : Execution.Budget} (S : Array (Perm n)) (a : Fin n) (hs : ∀ (p : Perm n), p ∈ S → p.inv ∈ S) : Execution.Run budget { orbit : { c : Orbit n // Orbit.Valid S a c } // orbit = Orbit.ofSymmetric S a hs }

Reserve orbit work in whole bounded batches. The point allowance covers the full degree, including declared fixed points.

Equations

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

def Hex.PermGroup.Build.resumeBudgeted {n base : Nat} {S : Array (Perm n)} {budget : Execution.Budget} (hbase : base < n) (c : Construction S base) {p : Perm n} (normal : Normalized (S.push p)) : Execution.Run budget { s : State normal.generators (base + 1) // s = resume hbase c normal }

Reserve the provenance transfer of resume: one index search per old level generator, and one substitution per retained suffix generator.

Equations

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

@[irreducible]

def Hex.PermGroup.Build.extendBudgeted {n : Nat} {budget : Execution.Budget} (base : Nat) (hb : base ≤ n) (S : Array (Perm n)) (c : Construction S base) (p : Perm n) (hf : Chain.Fixed base (S.push p)) : Computation budget (extend base hb S c p hf)

Extend a complete suffix within the caller's meter.

Equations

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

@[irreducible]

def Hex.PermGroup.Build.emptyBudgeted {n : Nat} {budget : Execution.Budget} (base : Nat) (hb : base ≤ n) : Computation budget (empty base hb)

The budgeted counterpart of empty.

Equations

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

def Hex.PermGroup.Build.bounded {n : Nat} {budget : Execution.Budget} (base : Nat) (hb : base ≤ n) (S : Array (Perm n)) (hf : Chain.Fixed base S) : Computation budget (build base hb S hf)

The budgeted counterpart of build, sharing the caller's meter with every recursive extension.

Equations

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

def Hex.PermGroup.Group.construct {n : Nat} {budget : Execution.Budget} (S : Array (Perm n)) : Build.Computation budget (ofGenerators S)

Construct a group using the current producer meter, including every recursive suffix extension.

Equations

• Hex.PermGroup.Group.construct S = do let c ← Hex.PermGroup.Build.bounded 0 ⋯ S ⋯ let G : Hex.PermGroup.Group n := { generators := S, chain := c.val.chain, valid := ⋯ } pure ⟨G, ⋯⟩

def Hex.PermGroup.Group.buildBudgeted {n : Nat} (budget : Execution.Budget) (S : Array (Perm n)) : Execution.Measured budget { G : Group n // G = ofGenerators S }

Construct a checked group within one shared producer budget. Exhaustion has no group output, so it cannot supply an ambient order or negative membership. Successful output is exactly ofGenerators S, with its acceptance proof.

Equations

• Hex.PermGroup.Group.buildBudgeted budget S = Hex.PermGroup.Execution.run budget (Hex.PermGroup.Group.construct S)