Subdivision.lean`

38 declarations, 0 contain sorry, 0 declared as axioms

The four-edge subdivision. Every input occurrence has its own three interior vertices, even when the original endpoints coincide or another occurrence has the same endpoints. The left/right presentation inverts the permutation on the fourth edge.

def OAI.MaxCutGames.Explicit.OccurrenceGame.satisfiedCount line 21
theorem OAI.MaxCutGames.Explicit.OccurrenceGame.satisfiedCount_eq_sum_satisfied line 24
def OAI.MaxCutGames.Explicit.OccurrenceGame.maxSatisfied line 39
def OAI.MaxCutGames.Explicit.OccurrenceGame.value line 43
theorem OAI.MaxCutGames.Explicit.OccurrenceGame.satisfiedCount_le_maxSatisfied line 46
theorem OAI.MaxCutGames.Explicit.OccurrenceGame.maxSatisfied_attained line 51
def OAI.MaxCutGames.Explicit.BipartiteGame.satisfiedCount line 64
theorem OAI.MaxCutGames.Explicit.BipartiteGame.satisfiedCount_eq_sum_satisfied line 67
def OAI.MaxCutGames.Explicit.BipartiteGame.maxSatisfied line 83
def OAI.MaxCutGames.Explicit.BipartiteGame.value line 87
theorem OAI.MaxCutGames.Explicit.BipartiteGame.satisfiedCount_le_maxSatisfied line 90
theorem OAI.MaxCutGames.Explicit.BipartiteGame.maxSatisfied_attained line 96
abbrev OAI.MaxCutGames.Explicit.Subdivision.Left line 111
Source documentation
Original vertices and the middle vertices q_e.
```
abbrev Left (V E : Type*) := V ⊕ E
```
abbrev OAI.MaxCutGames.Explicit.Subdivision.Right line 114
Source documentation
false is p_e, and true is r_e.
```
abbrev Right (E : Type*) := E × Bool
```
abbrev OAI.MaxCutGames.Explicit.Subdivision.Edge line 116
def OAI.MaxCutGames.Explicit.Subdivision.left line 118
def OAI.MaxCutGames.Explicit.Subdivision.right line 123
def OAI.MaxCutGames.Explicit.Subdivision.permutation line 125
theorem OAI.MaxCutGames.Explicit.Subdivision.endpoints_injective line 130
Source documentation
The private occurrence identifier prevents parallel edges after subdivision. This also handles a loop, which becomes a genuine four-cycle.
```
theorem endpoints_injective (g : OccurrenceGame V E A) :
    Function.Injective (fun ei : Edge E => (left g ei, right ei)) := by
…
```
Mentions: OAI.MaxCutGames.Explicit.OccurrenceGame, OAI.MaxCutGames.Explicit.Subdivision.Edge, OAI.MaxCutGames.Explicit.Subdivision.left, OAI.MaxCutGames.Explicit.Subdivision.right
def OAI.MaxCutGames.Explicit.Subdivision.game line 137
theorem OAI.MaxCutGames.Explicit.Subdivision.isTranslation line 145
Source documentation
Reversing the last edge negates its translation offset.
```
theorem isTranslation [AddGroup A] (g : OccurrenceGame V E A)
    (hg : g.IsTranslation) : (game g).IsTranslation := by
…
```
Mentions: OAI.MaxCutGames.Explicit.OccurrenceGame, OAI.MaxCutGames.Explicit.Subdivision.game
theorem OAI.MaxCutGames.Explicit.Subdivision.binary_translation_offsets line 158
Source documentation
In a binary additive alphabet the inverse offset is the original offset.
```
theorem binary_translation_offsets [AddGroup A]
    (hbinary : ∀ a : A, a + a = 0) (g : OccurrenceGame V E A)
    (c : E → A) (hc : ∀ e a, g.permutation e a = a + c e) :
    ∀ ei a, (game g).permutation ei a =
      a + (if ei.2 = 3 then c ei.1 else 0) := by
…
```
Mentions: OAI.MaxCutGames.Explicit.OccurrenceGame, OAI.MaxCutGames.Explicit.Subdivision.game, OAI.MaxCutGames.Explicit.Subdivision.permutation
def OAI.MaxCutGames.Explicit.Subdivision.restrict line 171
Source documentation
Restrict any output labeling to the original vertices.
```
def restrict (a : Left V E → A) : V → A := fun v => a (Sum.inl v)
```
Mentions: OAI.MaxCutGames.Explicit.Subdivision.Left
def OAI.MaxCutGames.Explicit.Subdivision.extendLeft line 173
def OAI.MaxCutGames.Explicit.Subdivision.extendRight line 176
theorem OAI.MaxCutGames.Explicit.Subdivision.restrict_extendLeft line 179
theorem OAI.MaxCutGames.Explicit.Subdivision.four_satisfied_implies_original line 183
Source documentation
All four equations along the path force the original permutation equation.
```
theorem four_satisfied_implies_original (ρ : Equiv.Perm A) (u p q r v : A)
    (h₀ : u = p) (h₁ : q = p) (h₂ : q = r) (h₃ : ρ.symm v = r) :
    ρ u = v := by
…
```

theorem OAI.MaxCutGames.Explicit.Subdivision.local_count_le line 193

Source documentation

The strongest possible path score for fixed endpoint labels is exactly three plus the old satisfaction indicator.

theorem local_count_le (ρ : Equiv.Perm A) (u p q r v : A) :
    (if u = p then 1 else 0) + (if q = p then 1 else 0) +
      (if q = r then 1 else 0) + (if ρ.symm v = r then 1 else 0) ≤
        3 + (if ρ u = v then 1 else 0 : Nat) := by
…

theorem OAI.MaxCutGames.Explicit.Subdivision.local_count_extend line 201
theorem OAI.MaxCutGames.Explicit.Subdivision.count_on_occurrence_le line 214
theorem OAI.MaxCutGames.Explicit.Subdivision.count_on_occurrence_extend line 225
theorem OAI.MaxCutGames.Explicit.Subdivision.satisfiedCount_le line 236
theorem OAI.MaxCutGames.Explicit.Subdivision.satisfiedCount_extend line 249
Source documentation
Fresh interiors can be assigned independently, so the upper bound is attained.
```
theorem satisfiedCount_extend (g : OccurrenceGame V E A) (a : V → A) :
    (game g).satisfiedCount (extendLeft g a) (extendRight g a) =
      3 * Fintype.card E + g.satisfiedCount a := by
…
```
Mentions: OAI.MaxCutGames.Explicit.OccurrenceGame, OAI.MaxCutGames.Explicit.Subdivision.game, OAI.MaxCutGames.Explicit.Subdivision.extendLeft, OAI.MaxCutGames.Explicit.Subdivision.extendRight
theorem OAI.MaxCutGames.Explicit.Subdivision.edge_count line 257
theorem OAI.MaxCutGames.Explicit.Subdivision.left_count line 260
theorem OAI.MaxCutGames.Explicit.Subdivision.right_count line 264
theorem OAI.MaxCutGames.Explicit.Subdivision.maxSatisfied_eq line 269
theorem OAI.MaxCutGames.Explicit.Subdivision.value_eq line 281