structure Hex.PermGroup.ProductLimits : Type

Product dimensions and cumulative producer allowances are independent. Declared fixed points contribute to the degree even when all generators fix them.

• degree : Nat

  Largest permitted output permutation degree.

• generators : Nat

  Largest permitted number of materialized input generators.

• work : Execution.Budget

  Shared materialization and recursive chain-construction budget.

inductive Hex.PermGroup.ProductLimit : Type

A dimension limit reports the actual dimension required by the operation.

• degree (required cap : Nat) : ProductLimit
• generators (required cap : Nat) : ProductLimit

def Hex.PermGroup.instDecidableEqProductLimit.decEq (x✝ x✝¹ : ProductLimit) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.instDecidableEqProductLimit.decEq (Hex.PermGroup.ProductLimit.degree required cap) (Hex.PermGroup.ProductLimit.generators required_1 cap_1) = isFalse ⋯
• Hex.PermGroup.instDecidableEqProductLimit.decEq (Hex.PermGroup.ProductLimit.generators required cap) (Hex.PermGroup.ProductLimit.degree required_1 cap_1) = isFalse ⋯

@[instance_reducible]

instance Hex.PermGroup.instDecidableEqProductLimit : DecidableEq ProductLimit

Equations

• Hex.PermGroup.instDecidableEqProductLimit = Hex.PermGroup.instDecidableEqProductLimit.decEq

@[instance_reducible]

instance Hex.PermGroup.instReprProductLimit : Repr ProductLimit

Equations

• Hex.PermGroup.instReprProductLimit = { reprPrec := Hex.PermGroup.instReprProductLimit.repr }

def Hex.PermGroup.instReprProductLimit.repr : ProductLimit → Nat → Std.Format

Equations

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

def Hex.PermGroup.Group.directProductBudgeted {n m : Nat} (limits : ProductLimits) (G : Group n) (H : Group m) : Except ProductLimit (Execution.Measured limits.work { K : Group (n + m) // K = G.directProduct H })

Direct products check n+m and rG+rH before either generator map runs. Image reservations include the degree-sized output arrays and factor identities. Chain construction then continues with the same meter.

Equations

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

def Hex.PermGroup.Group.wreathProductBudgeted {n m : Nat} (limits : ProductLimits) (G : Group n) (H : Group m) : Except ProductLimit (Execution.Measured limits.work { K : Group (n * m) // K = G.wreathProduct H })

The imprimitive product checks n*m and m*rG+rH, including fixed blocks. The native wreath action caches one base permutation per block before building its point images.

Equations

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

theorem Hex.PermGroup.Group.directProductBudgeted_degree {n m : Nat} (limits : ProductLimits) (G : Group n) (H : Group m) (h : limits.degree < n + m) : directProductBudgeted limits G H = Except.error (ProductLimit.degree (n + m) limits.degree)

Degree rejection happens before any direct-product allocation or chain work.

theorem Hex.PermGroup.Group.wreathProductBudgeted_degree {n m : Nat} (limits : ProductLimits) (G : Group n) (H : Group m) (h : limits.degree < n * m) : wreathProductBudgeted limits G H = Except.error (ProductLimit.degree (n * m) limits.degree)

Wreath degree rejection retains the full declared product degree.