Inventories and physical constructions

def MacMahon.HasCorner (p : Pair) (c : Corner) : Prop

A variety offers a specified oriented corner.

Equations

• MacMahon.HasCorner p c = (c ∈ MacMahon.cornerList p.1 p.2)

@[instance_reducible]

instance MacMahon.instDecidableHasCorner (p : Pair) (c : Corner) : Decidable (HasCorner p c)

Equations

• MacMahon.instDecidableHasCorner p c = { decide := decide (List.elem c (MacMahon.cornerList p.1 p.2) = true), reflects_decide := ⋯ }

def MacMahon.Usable (t p : Pair) : Prop

A physical cube shares at least one oriented corner with the target variety.

Equations

• MacMahon.Usable t p = ∃ (c : MacMahon.Corner), MacMahon.HasCorner t c ∧ MacMahon.HasCorner p c

@[instance_reducible]

instance MacMahon.instDecidableUsable (t p : Pair) : Decidable (Usable t p)

Equations

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

def MacMahon.FaceFits (t p : Pair) (k : Slot) (r : Fin 24) : Prop

After a specified proper rotation, a cube matches the target on all three outward faces.

Equations

• MacMahon.FaceFits t p k r = ∀ (f : Fin 3), MacMahon.faceColours p.1 p.2 (MacMahon.rotations r (MacMahon.exposedFaces k f)) = MacMahon.faceColours t.1 t.2 (MacMahon.exposedFaces k f)

@[instance_reducible]

instance MacMahon.instDecidableFaceFits (t p : Pair) (k : Slot) (r : Fin 24) : Decidable (FaceFits t p k r)

Equations

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

@[reducible, inline]

abbrev MacMahon.Stock (a : Inventory) : Type

Distinct physical copies of the varieties with the prescribed multiplicities.

Equations

• MacMahon.Stock a = ((p : MacMahon.Pair) × Fin (a p))

def MacMahon.Builds (a : Inventory) (t : Pair) : Prop

An injective allocation of eight physical copies matching the target corners.

Equations

• MacMahon.Builds a t = ∃ (f : MacMahon.Slot ↪ MacMahon.Stock a), ∀ (k : MacMahon.Slot), MacMahon.HasCorner (f k).fst (MacMahon.cornerAt t.1 t.2 k)

def MacMahon.PhysicalBuilds (a : Inventory) (t : Pair) : Prop

Eight distinct cubes with proper rotations matching all outward target faces.

Equations

• MacMahon.PhysicalBuilds a t = ∃ (f : MacMahon.Slot ↪ MacMahon.Stock a), ∀ (k : MacMahon.Slot), ∃ (r : Fin 24), MacMahon.FaceFits t (f k).fst k r

def MacMahon.PhysicalUniversal (a : Inventory) : Prop

Every valid target variety admits a physical assembly from the inventory.

Equations

• MacMahon.PhysicalUniversal a = ∀ (i j : MacMahon.Label), i ≠ j → MacMahon.PhysicalBuilds a (i, j)

def MacMahon.Universal (a : Inventory) : Prop

Every valid target variety admits a corner-matching assembly from the inventory.

Equations

• MacMahon.Universal a = ∀ (i j : MacMahon.Label), i ≠ j → MacMahon.Builds a (i, j)

def MacMahon.DiagonalZero (a : Inventory) : Prop

The invalid diagonal tableau entries have zero multiplicity.

Equations

• MacMahon.DiagonalZero a = ∀ (i : MacMahon.Label), a (i, i) = 0

def MacMahon.total (a : Inventory) : ℕ

The number of physical cubes in an inventory.

Equations

• MacMahon.total a = ∑ p : MacMahon.Pair, a p

def MacMahon.row (a : Inventory) (i : Label) : ℕ

The total multiplicity in a fixed Conway tableau row.

Equations

• MacMahon.row a i = ∑ j : MacMahon.Label, a (i, j)

def MacMahon.col (a : Inventory) (j : Label) : ℕ

The total multiplicity in a fixed Conway tableau column.

Equations

• MacMahon.col a j = ∑ i : MacMahon.Label, a (i, j)

def MacMahon.usableCount (a : Inventory) (t : Pair) : ℕ

The number of physical copies sharing a corner with a given target.

Equations

• MacMahon.usableCount a t = ∑ p : MacMahon.Pair, if MacMahon.Usable t p then a p else 0