ProductTarget.lean`

53 declarations, 0 contain sorry, 0 declared as axioms

Explicit numbered permutation-table outputs for bipartite graphs and products. All numbering maps are supplied as actual equivalences; the product uses the computable radix equivalence with division/remainder inverse, never an arbitrary finite-type enumeration. The value bridge preserves every list occurrence.

def OAI.MaxCutGames.Explicit.ProductTarget.fullTable line 24
Source documentation
Full forward and inverse tables of an explicit finite permutation.
```
def fullTable (p : Equiv.Perm (Fin q)) : PermutationTable q where
…
```
theorem OAI.MaxCutGames.Explicit.ProductTarget.fullTable_images line 30
theorem OAI.MaxCutGames.Explicit.ProductTarget.permutationEquiv_fullTable line 33
def OAI.MaxCutGames.Explicit.ProductTarget.row line 39
Source documentation
One explicitly addressed row, with a separately supplied complete table.
```
def row (G : BipartiteGame L R E (Fin q)) (vertices : (L ⊕ R) ≃ Fin N)
    (edges : Fin M ≃ E) (tables : E → PermutationTable q) (i : Fin M) :
    Constraint N q where
…
```
Mentions: OAI.MaxCutGames.Explicit.BipartiteGame
def OAI.MaxCutGames.Explicit.ProductTarget.render line 46
theorem OAI.MaxCutGames.Explicit.ProductTarget.render_length line 57
theorem OAI.MaxCutGames.Explicit.ProductTarget.render_get line 63
def OAI.MaxCutGames.Explicit.ProductTarget.render_simpleBipartite line 72

theorem OAI.MaxCutGames.Explicit.ProductTarget.render_count line 102

Source documentation

A full vertex labeling pulls back to two independently local labelings.

theorem render_count (G : BipartiteGame L R E (Fin q))
    (vertices : (L ⊕ R) ≃ Fin N) (edges : Fin M ≃ E)
    (tables : E → PermutationTable q) (hM : 0 < M)
    (htable : ∀ e, permutationEquiv (tables e) = G.permutation e)
    (labeling : Fin N → Fin q) :
    countSatisfied labeling (render G vertices edges tables hM).constraints =
      G.satisfiedCount (fun x => labeling (vertices (Sum.inl x)))
        (fun y => labeling (vertices (Sum.inr y))) := by
…

Mentions: OAI.MaxCutGames.Explicit.BipartiteGame, OAI.MaxCutGames.Explicit.ProductTarget.render

def OAI.MaxCutGames.Explicit.ProductTarget.mergeLabelings line 120
theorem OAI.MaxCutGames.Explicit.ProductTarget.mergeLabelings_left line 125
theorem OAI.MaxCutGames.Explicit.ProductTarget.mergeLabelings_right line 131
theorem OAI.MaxCutGames.Explicit.ProductTarget.render_count_merge line 137
theorem OAI.MaxCutGames.Explicit.ProductTarget.render_maxSatisfied line 147
theorem OAI.MaxCutGames.Explicit.ProductTarget.render_value line 167
def OAI.MaxCutGames.Explicit.ProductTarget.tuples line 181
Source documentation
The product order is increasing radix address, with coordinate zero the least significant digit. The inverse computes each digit by division/modulo.
```
def tuples (n t : ℕ) : List (Fin t → Fin n) :=
…
```
theorem OAI.MaxCutGames.Explicit.ProductTarget.tuples_length line 184
theorem OAI.MaxCutGames.Explicit.ProductTarget.tuples_mem line 187
theorem OAI.MaxCutGames.Explicit.ProductTarget.tuples_nodup line 191
theorem OAI.MaxCutGames.Explicit.ProductTarget.tuples_get line 194
theorem OAI.MaxCutGames.Explicit.ProductTarget.tuple_address line 199
theorem OAI.MaxCutGames.Explicit.ProductTarget.address_eq_ofDigits line 205
Source documentation
The explicit address and ofDigits share the same least-significant-first coordinate order, with no restriction on the radix beyond the digit type.
```
theorem address_eq_ofDigits {n t : ℕ} (f : Fin t → Fin n) :
    (finFunctionFinEquiv f : ℕ) = Nat.ofDigits n (List.ofFn (fun i => (f i : ℕ))) := by
…
```
theorem OAI.MaxCutGames.Explicit.ProductTarget.address_eq_horner line 218
Source documentation
A forward Horner controller reads the coordinate words in reverse order. This is a word-order identity, separate from its machine execution theorem.
```
theorem address_eq_horner {n t : ℕ} (f : Fin t → Fin n) :
    (finFunctionFinEquiv f : ℕ) =
      (List.ofFn (fun i => (f i : ℕ))).reverse.foldl
        (fun acc digit => n * acc + digit) 0 := by
…
```
def OAI.MaxCutGames.Explicit.SubdivisionTarget.ofInstance line 240
Source documentation
Retain every original list occurrence as its own edge identifier.
```
def ofInstance {q : Nat} (H : Instance q) :
    OccurrenceGame (Fin H.vertices) (Fin H.constraints.length) (Fin q) where
…
```
Mentions: OAI.MaxCutGames.Explicit.OccurrenceGame
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.ofInstance_count line 246
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.ofInstance_maxSatisfied line 256
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.ofInstance_value line 266
def OAI.MaxCutGames.Explicit.SubdivisionTarget.numericRightEquiv line 273
Source documentation
Number p_e by 2e and r_e by 2e+1.
```
def numericRightEquiv (Q : Nat) : Fin Q × Bool ≃ Fin (Q * 2) :=
…
```
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.numericRightEquiv_false_val line 276
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.numericRightEquiv_true_val line 281
def OAI.MaxCutGames.Explicit.SubdivisionTarget.numericVertexEquiv line 287
Source documentation
Original vertices, middle vertices, then interleaved p_e,r_e.
```
def numericVertexEquiv (n Q : Nat) :
    (Fin n ⊕ Fin Q) ⊕ (Fin Q × Bool) ≃ Fin (n + 3 * Q) :=
…
```
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.numericVertexEquiv_original_val line 295
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.numericVertexEquiv_middle_val line 298
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.numericVertexEquiv_p_val line 301
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.numericVertexEquiv_r_val line 306
def OAI.MaxCutGames.Explicit.SubdivisionTarget.numericEdgeEquiv line 312
Source documentation
The occurrence e occupies output indices 4e,4e+1,4e+2,4e+3.
```
def numericEdgeEquiv (Q : Nat) : Fin (4 * Q) ≃ Fin Q × Fin 4 :=
…
```
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.numericEdgeEquiv_symm_val line 315
def OAI.MaxCutGames.Explicit.SubdivisionTarget.tables line 320
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.tables_correspond line 325
def OAI.MaxCutGames.Explicit.SubdivisionTarget.vertexFields line 334
Source documentation
The five physical fields consumed by the checked row-emission phase.
```
def vertexFields {q : Nat} (H : Instance q) (e : Fin H.constraints.length) :
    Fin 5 → Fin (H.vertices + 3 * H.constraints.length) :=
…
```
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.vertexFields_val line 342
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.rows_eq line 351
Source documentation
Four consecutive semantic rows are exactly the four full-table rows emitted by the machine phase, including the inverse table in the final row.
```
theorem rows_eq {q : Nat} (H : Instance q) (e : Fin H.constraints.length) :
    List.ofFn (fun i : Fin 4 => ProductTarget.row (Subdivision.game (ofInstance H))
      (numericVertexEquiv H.vertices H.constraints.length)
      (numericEdgeEquiv H.constraints.length) (tables H)
      ((numericEdgeEquiv H.constraints.length).symm (e, i))) =
    MachineSubdivisionRows.rows (vertexFields H e) H.constraints[e].permutation := by
…
```
Mentions: OAI.MaxCutGames.Explicit.ProductTarget.row, OAI.MaxCutGames.Explicit.Subdivision.game, OAI.MaxCutGames.Explicit.SubdivisionTarget.ofInstance, OAI.MaxCutGames.Explicit.SubdivisionTarget.numericVertexEquiv, OAI.MaxCutGames.Explicit.SubdivisionTarget.numericEdgeEquiv, OAI.MaxCutGames.Explicit.SubdivisionTarget.tables, OAI.MaxCutGames.Explicit.MachineSubdivisionRows.rows, OAI.MaxCutGames.Explicit.SubdivisionTarget.vertexFields
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.tables_translation line 360
def OAI.MaxCutGames.Explicit.SubdivisionTarget.subdivide line 380
Source documentation
A deterministic full-table occurrence list with exactly four rows per input row.
```
def subdivide {q : Nat} (H : Instance q) : Instance q :=
…
```
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.subdivide_vertices line 386
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.subdivide_length line 389
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.subdivide_translation line 393
def OAI.MaxCutGames.Explicit.SubdivisionTarget.simpleBipartite line 402
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.numeric_side line 405
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.simpleBipartite_side line 425
Source documentation
The concrete left side is precisely the first n+Q numeric names.
```
theorem simpleBipartite_side {q : Nat} (H : Instance q) (v : Fin (subdivide H).vertices) :
    (simpleBipartite H).side v = decide (H.vertices + H.constraints.length ≤ v.val) :=
…
```
Mentions: OAI.MaxCutGames.Explicit.SubdivisionTarget.subdivide, OAI.MaxCutGames.Explicit.SubdivisionTarget.simpleBipartite

theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.subdivide_count line 430

Source documentation

Satisfaction correspondence for every labeling of the actual numbered output.

theorem subdivide_count {q : Nat} (H : Instance q)
    (a : Fin (H.vertices + 3 * H.constraints.length) → Fin q) :
    countSatisfied a (subdivide H).constraints =
      (Subdivision.game (ofInstance H)).satisfiedCount
        (fun l => a (numericVertexEquiv H.vertices H.constraints.length (Sum.inl l)))
        (fun r => a (numericVertexEquiv H.vertices H.constraints.length (Sum.inr r))) :=
…

Mentions: OAI.MaxCutGames.Explicit.SubdivisionTarget.subdivide, OAI.MaxCutGames.Explicit.Subdivision.game, OAI.MaxCutGames.Explicit.SubdivisionTarget.ofInstance, OAI.MaxCutGames.Explicit.SubdivisionTarget.numericVertexEquiv

theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.subdivide_value line 439
Source documentation
The serialized output has exactly the abstract subdivision value.
```
theorem subdivide_value {q : Nat} (H : Instance q) :
    Integration.InstanceValue.value (subdivide H) =
      (Subdivision.game (ofInstance H)).value :=
…
```
Mentions: OAI.MaxCutGames.Integration.InstanceValue.value, OAI.MaxCutGames.Explicit.SubdivisionTarget.subdivide, OAI.MaxCutGames.Explicit.Subdivision.game, OAI.MaxCutGames.Explicit.SubdivisionTarget.ofInstance
theorem OAI.MaxCutGames.Explicit.SubdivisionTarget.value_eq line 445
Source documentation
Exact equation (bipartization-value) for the concrete list/table format.
```
theorem value_eq {q : Nat} (H : Instance q) (hq : 0 < q) :
    Integration.InstanceValue.value (subdivide H) =
      1 - (1 - Integration.InstanceValue.value H) / 4 := by
…
```
Mentions: OAI.MaxCutGames.Integration.InstanceValue.value, OAI.MaxCutGames.Explicit.SubdivisionTarget.subdivide