CFGraphExample

Chip firing, graph divisors, and their combinatorial properties.

inductive ChipFiring.Person : Type

Four vertices used in the concrete chip-firing examples.

• A : Person
• B : Person
• C : Person
• E : Person

@[instance_reducible]

instance ChipFiring.instDecidableEqPerson : DecidableEq Person

Equations

• ChipFiring.instDecidableEqPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ChipFiring.instFintypePerson : Fintype Person

Equations

• ChipFiring.instFintypePerson = { elems := {ChipFiring.Person.A, ChipFiring.Person.B, ChipFiring.Person.C, ChipFiring.Person.E}, complete := ChipFiring.instFintypePerson._proof_3 }

instance ChipFiring.instNonemptyPerson : Nonempty Person

def ChipFiring.exampleEdges : Multiset (Person × Person)

Three-edge path on the example vertices.

Equations

• ChipFiring.exampleEdges = ↑[(ChipFiring.Person.A, ChipFiring.Person.B), (ChipFiring.Person.B, ChipFiring.Person.C), (ChipFiring.Person.C, ChipFiring.Person.E)]

def ChipFiring.edgesWithLoop : Multiset (Person × Person)

Example edge multiset containing a loop at A.

Equations

• ChipFiring.edgesWithLoop = ↑[(ChipFiring.Person.A, ChipFiring.Person.B), (ChipFiring.Person.A, ChipFiring.Person.A), (ChipFiring.Person.B, ChipFiring.Person.C)]

def ChipFiring.exampleGraph : CFGraph

Four-vertex loopless multigraph used to test firing and borrowing operations.

Equations

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

def ChipFiring.initialWealth : CFDiv exampleGraph

Initial divisor with wealth 2, -3, 4, and -1 at A, B, C, and E.

Equations

• ChipFiring.initialWealth ChipFiring.Person.A = 2
• ChipFiring.initialWealth ChipFiring.Person.B = -3
• ChipFiring.initialWealth ChipFiring.Person.C = 4
• ChipFiring.initialWealth ChipFiring.Person.E = -1

def ChipFiring.afterCharlieLends : CFDiv exampleGraph

Divisor after C fires once from the initial configuration.

Equations

• ChipFiring.afterCharlieLends = ChipFiring.firingMove ChipFiring.exampleGraph ChipFiring.initialWealth ChipFiring.Person.C

def ChipFiring.W₁ : Finset exampleGraph.V

First set of vertices fired in the example sequence.

Equations

• ChipFiring.W₁ = {ChipFiring.Person.A, ChipFiring.Person.E, ChipFiring.Person.C}

def ChipFiring.afterW₁Firing : CFDiv exampleGraph

Divisor after firing A, E, and C from the initial configuration.

Equations

• ChipFiring.afterW₁Firing = ChipFiring.setFiring ChipFiring.exampleGraph ChipFiring.initialWealth ChipFiring.W₁

def ChipFiring.W₂ : Finset exampleGraph.V

Second firing set, repeating the first set of vertices.

Equations

• ChipFiring.W₂ = ChipFiring.W₁

def ChipFiring.afterW₂Firing : CFDiv exampleGraph

Divisor after the second firing of A, E, and C.

Equations

• ChipFiring.afterW₂Firing = ChipFiring.setFiring ChipFiring.exampleGraph ChipFiring.afterW₁Firing ChipFiring.W₂

def ChipFiring.W₃ : Finset exampleGraph.V

Final firing set consisting of B and C.

Equations

• ChipFiring.W₃ = {ChipFiring.Person.B, ChipFiring.Person.C}

def ChipFiring.afterW₃Firing : CFDiv exampleGraph

Effective divisor obtained after the three set-firing steps.

Equations

• ChipFiring.afterW₃Firing = ChipFiring.setFiring ChipFiring.exampleGraph ChipFiring.afterW₂Firing ChipFiring.W₃

def ChipFiring.afterBobBorrows : CFDiv exampleGraph

Divisor after B borrows once from the initial configuration.

Equations

• ChipFiring.afterBobBorrows = ChipFiring.borrowingMove ChipFiring.exampleGraph ChipFiring.initialWealth ChipFiring.Person.B

def ChipFiring.exampleLaplacian : Matrix exampleGraph.V exampleGraph.V ℤ

Integer Laplacian matrix of the example multigraph.

Equations

• ChipFiring.exampleLaplacian = ChipFiring.laplacianMatrix ChipFiring.exampleGraph

def ChipFiring.firingScriptExample : firingScript exampleGraph

Firing script in which C fires once and B borrows once.

Equations

• ChipFiring.firingScriptExample ChipFiring.Person.A = 0
• ChipFiring.firingScriptExample ChipFiring.Person.B = -1
• ChipFiring.firingScriptExample ChipFiring.Person.C = 1
• ChipFiring.firingScriptExample ChipFiring.Person.E = 0

def ChipFiring.resDivPostLapBasedScriptFiring : CFDiv exampleGraph

Divisor obtained by applying the example firing script through the Laplacian.

Equations

• ChipFiring.resDivPostLapBasedScriptFiring = ChipFiring.applyLaplacian ChipFiring.exampleGraph ChipFiring.firingScriptExample ChipFiring.initialWealth

def ChipFiring.nonQReducedExample : CFDiv exampleGraph

Example divisor that is not A-reduced because B has negative wealth.

Equations

• ChipFiring.nonQReducedExample ChipFiring.Person.A = 1
• ChipFiring.nonQReducedExample ChipFiring.Person.B = -1
• ChipFiring.nonQReducedExample ChipFiring.Person.C = 2
• ChipFiring.nonQReducedExample ChipFiring.Person.E = 1