SubdivisionEncoding.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact whole-output serialization of four-edge subdivision. The input occurrence at index e produces the four adjacent rows at 4e,4e+1,4e+2,4e+3. The bit formula uses the same complete row output as the checked machine phase.

theorem OAI.MaxCutGames.Explicit.SubdivisionEncoding.subdivide_constraints line 18
theorem OAI.MaxCutGames.Explicit.SubdivisionEncoding.subdivide_constraints_flatMap line 35

theorem OAI.MaxCutGames.Explicit.SubdivisionEncoding.subdivide_gameWords line 43

Source documentation

Header and complete row words, in the original input occurrence order.

theorem subdivide_gameWords {q : Nat} (H : Instance q) :
    gameWords (subdivide H) =
      [H.vertices + 3 * H.constraints.length, q, 4 * H.constraints.length] ++
      (List.finRange H.constraints.length).flatMap (fun e =>
        (MachineSubdivisionRows.rows (vertexFields H e)
          H.constraints[e].permutation).flatMap constraintWords) := by
…

Mentions: OAI.MaxCutGames.Explicit.MachineSubdivisionRows.rows

theorem OAI.MaxCutGames.Explicit.SubdivisionEncoding.encodeWords_flatMap_inline_SubdivisionEncoding line 54

theorem OAI.MaxCutGames.Explicit.SubdivisionEncoding.subdivide_gameBits line 62

Source documentation

Exact output bytes for the whole controller to emit: one header followed by the verified four-row phase once per original occurrence.

theorem subdivide_gameBits {q : Nat} (H : Instance q) :
    gameBits (subdivide H) =
      encodeWords [H.vertices + 3 * H.constraints.length, q, 4 * H.constraints.length] ++
      (List.finRange H.constraints.length).flatMap (fun e =>
        MachineSubdivisionRows.rowBits (vertexFields H e) H.constraints[e].permutation) := by
…

Mentions: OAI.MaxCutGames.Explicit.MachineSubdivisionRows.rowBits

theorem OAI.MaxCutGames.Explicit.SubdivisionEncoding.subdivide_gameWords_length line 70

theorem OAI.MaxCutGames.Explicit.SubdivisionEncoding.subdivide_gameBits_length_le line 76

Source documentation

A polynomial output-size bound in the numeric parameters n,Q,q; the controller separately supplies its raw-input execution-time bound.

theorem subdivide_gameBits_length_le {q : Nat} (H : Instance q) :
    (gameBits (subdivide H)).length ≤
      H.vertices + 3 * H.constraints.length + q + 4 * H.constraints.length + 3 +
        (4 * H.constraints.length) *
          (2 * (H.vertices + 3 * H.constraints.length) + q * (q + 1)) := by
…