OAI/Combinatorics/Hamiltonian/StateDisk.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Minimal links, incidence states, and the signed disk identity.

  1. lemma OAI.Barnette.Network.Duality.symm line 14
  2. lemma OAI.Barnette.Network.Duality.vertex_flow_circuit line 19
  3. lemma OAI.Barnette.Network.cut_restrict_conserved line 81
  4. lemma OAI.Barnette.Network.FlowCircuit.no_split line 108
  5. theorem OAI.Barnette.Network.mixed_corner_on_boundary line 129
  6. def OAI.Barnette.Network.cycleVertices line 169
  7. lemma OAI.Barnette.Network.mem_cycleVertices line 173
  8. lemma OAI.Barnette.Network.incident_cycle_iff line 178
  9. lemma OAI.Barnette.Network.regionVertices_iff_face line 193
  10. def OAI.Barnette.Network.blackEndpoint line 212
  11. lemma OAI.Barnette.Network.blackEndpoint_spec line 216
  12. lemma OAI.Barnette.Network.blackEndpoint_eq line 225
  13. def OAI.Barnette.Network.blackCut line 235
  14. lemma OAI.Barnette.Network.cubic_black_region_count line 239
  15. theorem OAI.Barnette.Network.state_disk_count line 260
  16. def OAI.Barnette.Network.blackDelta line 385
  17. lemma OAI.Barnette.Network.blackDelta_cut line 390
  18. lemma OAI.Barnette.Network.cycle_cut_scalar line 416
  19. lemma OAI.Barnette.Network.disk_boundary_imbalance line 428
  20. theorem OAI.Barnette.Network.state_disk_delta line 442