inductive Person : Type

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

@[implicit_reducible]

instance instDecidableEqPerson : DecidableEq Person

Equations

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

@[implicit_reducible]

instance instFintypePerson : Fintype Person

Equations

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

instance instNonemptyPerson : Nonempty Person

def exampleEdges : Multiset (Person × Person)

Equations

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

theorem loopless_example_edges (v : Person) : (v, v) ∉ exampleEdges

def edgesWithLoop : Multiset (Person × Person)

Equations

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

theorem loopless_test_edges_with_loop : ¬∀ (v : Person), (v, v) ∉ edgesWithLoop

def example_graph : CFGraph

Equations

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

def initial_wealth : CFDiv example_graph

Equations

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

theorem vertex_degree_A : vertex_degree example_graph Person.A = 4

theorem vertex_degree_B : vertex_degree example_graph Person.B = 2

theorem vertex_degree_C : vertex_degree example_graph Person.C = 3

theorem vertex_degree_E : vertex_degree example_graph Person.E = 3

theorem edge_count_AB : num_edges example_graph Person.A Person.B = 1

theorem edge_count_BA : num_edges example_graph Person.B Person.A = 1

theorem edge_count_BC : num_edges example_graph Person.B Person.C = 1

theorem edge_count_CB : num_edges example_graph Person.C Person.B = 1

theorem edge_count_AC : num_edges example_graph Person.A Person.C = 1

theorem edge_count_CA : num_edges example_graph Person.C Person.A = 1

theorem edge_count_AE : num_edges example_graph Person.A Person.E = 2

theorem edge_count_EA : num_edges example_graph Person.E Person.A = 2

theorem edge_count_EC : num_edges example_graph Person.E Person.C = 1

theorem edge_count_CE : num_edges example_graph Person.C Person.E = 1

theorem edge_count_BE : num_edges example_graph Person.B Person.E = 0

theorem edge_count_EB : num_edges example_graph Person.E Person.B = 0

theorem edge_count_AA : num_edges example_graph Person.A Person.A = 0

theorem edge_count_BB : num_edges example_graph Person.B Person.B = 0

theorem edge_count_CC : num_edges example_graph Person.C Person.C = 0

theorem edge_count_EE : num_edges example_graph Person.E Person.E = 0

def after_charlie_lends : CFDiv example_graph

Equations

• after_charlie_lends = firing_move example_graph initial_wealth Person.C

theorem charlie_wealth_after_lending : after_charlie_lends Person.C = 1

theorem bob_wealth_after_charlie_lends : after_charlie_lends Person.B = -2

def W₁ : Finset example_graph.V

Equations

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

def after_W₁_firing : CFDiv example_graph

Equations

• after_W₁_firing = set_firing example_graph initial_wealth W₁

theorem alice_wealth_after_W₁ : after_W₁_firing Person.A = 1

theorem bob_wealth_after_W₁ : after_W₁_firing Person.B = -1

theorem charlie_wealth_after_W₁ : after_W₁_firing Person.C = 3

theorem elise_wealth_after_W₁ : after_W₁_firing Person.E = -1

def W₂ : Finset example_graph.V

Equations

• W₂ = W₁

def after_W₂_firing : CFDiv example_graph

Equations

• after_W₂_firing = set_firing example_graph after_W₁_firing W₂

theorem alice_wealth_after_W₂ : after_W₂_firing Person.A = 0

theorem bob_wealth_after_W₂ : after_W₂_firing Person.B = 1

theorem charlie_wealth_after_W₂ : after_W₂_firing Person.C = 2

theorem elise_wealth_after_W₂ : after_W₂_firing Person.E = -1

def W₃ : Finset example_graph.V

Equations

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

def after_W₃_firing : CFDiv example_graph

Equations

• after_W₃_firing = set_firing example_graph after_W₂_firing W₃

theorem alice_wealth_after_W₃ : after_W₃_firing Person.A = 2

theorem bob_wealth_after_W₃ : after_W₃_firing Person.B = 0

theorem charlie_wealth_after_W₃ : after_W₃_firing Person.C = 0

theorem elise_wealth_after_W₃ : after_W₃_firing Person.E = 0

def after_bob_borrows : CFDiv example_graph

Equations

• after_bob_borrows = borrowing_move example_graph initial_wealth Person.B

theorem bob_wealth_after_borrowing : after_bob_borrows Person.B = -1

theorem alice_wealth_after_bob_borrows : after_bob_borrows Person.A = 1

theorem charlie_wealth_after_bob_borrows : after_bob_borrows Person.C = 3

theorem initial_wealth_degree : deg initial_wealth = 2

theorem after_W₁_degree : deg after_W₁_firing = 2

theorem after_W₂_degree : deg after_W₂_firing = 2

theorem after_W₃_degree : deg after_W₃_firing = 2

theorem initial_not_effective : ¬effective initial_wealth

theorem after_W₃_firing_effective : effective after_W₃_firing

def example_laplacian : Matrix example_graph.V example_graph.V ℤ

Equations

• example_laplacian = laplacian_matrix example_graph

theorem laplacian_diagonal_A : example_laplacian Person.A Person.A = 4

theorem laplacian_diagonal_B : example_laplacian Person.B Person.B = 2

theorem laplacian_diagonal_C : example_laplacian Person.C Person.C = 3

theorem laplacian_diagonal_E : example_laplacian Person.E Person.E = 3

theorem laplacian_off_diagonal_AB : example_laplacian Person.A Person.B = -1

theorem laplacian_off_diagonal_AC : example_laplacian Person.A Person.C = -1

theorem laplacian_off_diagonal_AE : example_laplacian Person.A Person.E = -2

theorem laplacian_off_diagonal_BC : example_laplacian Person.B Person.C = -1

theorem laplacian_off_diagonal_BE : example_laplacian Person.B Person.E = 0

theorem laplacian_off_diagonal_CE : example_laplacian Person.C Person.E = -1

theorem check_example_laplacian_symmetry : example_laplacian.IsSymm

def firing_script_example : firing_script example_graph

Equations

• firing_script_example Person.A = 0
• firing_script_example Person.B = -1
• firing_script_example Person.C = 1
• firing_script_example Person.E = 0

def res_div_post_lap_based_script_firing : CFDiv example_graph

Equations

• res_div_post_lap_based_script_firing = apply_laplacian example_graph firing_script_example initial_wealth

theorem lap_based_script_firing_preserves_degree : deg res_div_post_lap_based_script_firing = 2

def non_q_reduced_example : CFDiv example_graph

Equations

• non_q_reduced_example Person.A = 1
• non_q_reduced_example Person.B = -1
• non_q_reduced_example Person.C = 2
• non_q_reduced_example Person.E = 1

theorem non_q_reduced_example_is_invalid : ¬q_reduced example_graph Person.A non_q_reduced_example