OAI/Computability/MaxCut/Games/PoweringGlobalEnumeration.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Explicit executable enumeration of the global powering tapes

The four header tapes come first, followed by the eleven shared roles, the bounded trajectory tapes, and the final output tape. Both directions use constructor cases and arithmetic sum encodings. No enumeration is selected from a cardinality theorem.

  1. def OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.headerTapeEquiv line 19
  2. def OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.unitTapeEquiv line 31

    Source documentation

    The single extra output tape occupies its unique local index.

    def unitTapeEquiv : Unit ≃ Fin 1 where
…
  3. def OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.sharedTapeEquiv line 37
  4. def OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.extraTapeEquiv line 40
  5. def OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.globalTapeEquiv line 44

    Source documentation

    Exact arithmetic numbering of every physical global tape.

    def globalTapeEquiv (max : Nat) : GlobalTape max ≃ Fin (4 + (11 + max + 1)) :=
…
  6. def OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.enumeration line 48

    Source documentation

    The executable equivalence consumed by Finish and DrainMany.

    def enumeration (max : Nat) : Fin (4 + (11 + max + 1)) ≃ GlobalTape max :=
…
  7. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.globalTapeEquiv_enumeration line 51
  8. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.enumeration_globalTapeEquiv line 55
  9. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.source_index line 59
  10. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.counter_index line 62
  11. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.vertices_index line 65
  12. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.darts_index line 68
  13. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.sharedRole_index line 71
  14. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.trajectory_index line 74
  15. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.finalOutput_index line 77
  16. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.card_globalTape line 81

    Source documentation

    The exact cardinality follows from the explicit executable bijection.

    theorem card_globalTape (max : Nat) :
    Fintype.card (GlobalTape max) = 4 + (11 + max + 1) := by
…
  17. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.natCard_globalTape line 85
  18. def OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.allTapes line 90

    Source documentation

    A fixed finite list of all tape names is available without ambient search.

    def allTapes (max : Nat) : List (GlobalTape max) := List.ofFn (enumeration max)

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.enumeration

  19. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.allTapes_length line 92
  20. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalEnumeration.mem_allTapes line 95