theorem Hex.PermGroup.choice_card {n : ℕ} (c : Chain n) : Nat.card c.Choice = c.orbitProduct

The Cartesian choices have the chain's orbit-product cardinality.

noncomputable def Hex.PermGroup.choiceEquiv {n : ℕ} {S : Array (Perm n)} {c : Chain n} (h : checkChain S c = true) : c.Choice ≃ ↥(closure S)

The representative product identifies Cartesian choices with the original mathematical subgroup. This equivalence is used for cardinality; executable membership continues to use sifting.

Equations

• Hex.PermGroup.choiceEquiv h = Equiv.ofBijective (fun (digits : c.Choice) => ⟨(c.value digits).toEquiv, ⋯⟩) ⋯

theorem Hex.PermGroup.checkChain_card {n : ℕ} {S : Array (Perm n)} {c : Chain n} (h : checkChain S c = true) : c.orbitProduct = Nat.card ↥(closure S)

The orbit-size product is the exact cardinality of the original subgroup.

theorem Hex.PermGroup.checkChain_spec {n : ℕ} {S : Array (Perm n)} {c : Chain n} (h : checkChain S c = true) : (∀ (p : Perm n), c.accepts 0 p = true ↔ p.toEquiv ∈ closure S) ∧ c.orbitProduct = Nat.card ↥(closure S)

Headline complete-chain correspondence: exact membership and exact order, with the action degree and original generator array retained.