OAI/Computability/MaxCut/Machines/MachineProductGatherBounds.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Bounds on the actual work stacks left by the preserving gather. These bounds justify clearing the query/scan remnants after each product field; they are consequences of the exact tape formulas, not runtime assumptions.

  1. theorem OAI.MaxCutGames.Explicit.MachineProductGather.affine_final_length line 17
  2. theorem OAI.MaxCutGames.Explicit.MachineProductGather.finalTapes_length line 51

    Source documentation

    One field query adds at most one table's worth of bits to any tape. A width-fold gather therefore has a uniform linear-in-width space bound.

    theorem finalTapes_length (values : List Nat) (coefficient width : Nat)
    (placement : Tape width → K) (distinct : Function.Injective placement)
    (indices offsets fields : Fin width → Nat)
    (selected : ∀ i, values[coefficient * indices i + offsets i]? = some (fields i))
    (base : K → List Bool) (k : K) :
    (finalTapes values coefficient width placement indices offsets fields base k).length ≤
      (base k).length + width * ((encodeWords values).length + 1) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductGather.Tape, OAI.MaxCutGames.Explicit.MachineProductGather.finalTapes

  3. theorem OAI.MaxCutGames.Explicit.MachineProductField.mem_clearTapes line 90
  4. theorem OAI.MaxCutGames.Explicit.MachineProductField.extra_not_mem_clearTapes line 96
  5. theorem OAI.MaxCutGames.Explicit.MachineProductField.Ready.empty_clearTapes line 105
  6. theorem OAI.MaxCutGames.Explicit.MachineProductField.gathered_frame line 112
  7. theorem OAI.MaxCutGames.Explicit.MachineProductField.finalTapes_eq line 123

    Source documentation

    The complete row-field phase changes just the output accumulator.

    theorem finalTapes_eq (slots : Layout width ↪ K) (values : List Nat) (coefficient : Nat)
    (indices offsets fields : Fin width → Nat) (base : K → List Bool)
    (ready : Ready slots base) (value : Nat) :
    finalTapes slots values coefficient indices offsets fields base value =
      Function.update base (slots (.inr 6))
        ((encodeWord value).reverse ++ base (slots (.inr 6))) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductField.Layout, OAI.MaxCutGames.Explicit.MachineProductField.Ready, OAI.MaxCutGames.Explicit.MachineProductField.finalTapes

  8. theorem OAI.MaxCutGames.Explicit.MachineProductField.Ready.output_update line 150

    Source documentation

    The output update preserves all work-tape entry conditions.

    theorem Ready.output_update (slots : Layout width ↪ K) (base : K → List Bool)
    (ready : Ready slots base) (word : List Bool) :
    Ready slots (Function.update base (slots (.inr 6)) word) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductField.Layout, OAI.MaxCutGames.Explicit.MachineProductField.Ready

  9. theorem OAI.MaxCutGames.Explicit.MachineProductField.final_ready line 167
  10. theorem OAI.MaxCutGames.Explicit.MachineProductField.emitted_clear_length line 175

    Source documentation

    Cleanup only touches gather work; it never scans the global accumulator.

    theorem emitted_clear_length (slots : Layout width ↪ K) (values : List Nat) (coefficient : Nat)
    (indices offsets fields : Fin width → Nat)
    (selected : ∀ i, values[coefficient * indices i + offsets i]? = some (fields i))
    (base : K → List Bool) (ready : Ready slots base) (value : Nat)
    (k : K) (member : k ∈ clearTapes slots) :
    (emitted slots values coefficient indices offsets fields base value k).length ≤
      width * ((encodeWords values).length + 1) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductField.Layout, OAI.MaxCutGames.Explicit.MachineProductField.Ready, OAI.MaxCutGames.Explicit.MachineProductField.clearTapes, OAI.MaxCutGames.Explicit.MachineProductField.emitted

  11. theorem OAI.MaxCutGames.Explicit.MachineProductField.clearTapes_length line 193
  12. theorem OAI.MaxCutGames.Explicit.MachineProductField.cleanup_steps_le line 196
  13. abbrev OAI.MaxCutGames.Explicit.MachineProductRow.Layout line 234
  14. abbrev OAI.MaxCutGames.Explicit.MachineProductRow.Command line 235
  15. def OAI.MaxCutGames.Explicit.MachineProductRow.fieldRole line 238

    Source documentation

    Only the radix tape is switched between endpoint and alphabet fields.

    def fieldRole (useAlphabet : Bool) : MachineProductField.Layout width → Layout width
  | .inr 0 => if useAlphabet then .inr () else .inl (.inr 0)
  | tape => .inl tape

    Mentions: OAI.MaxCutGames.Explicit.MachineProductField.Layout, OAI.MaxCutGames.Explicit.MachineProductRow.Layout

  16. theorem OAI.MaxCutGames.Explicit.MachineProductRow.fieldRole_injective line 242
  17. def OAI.MaxCutGames.Explicit.MachineProductRow.fieldSlots line 255
  18. abbrev OAI.MaxCutGames.Explicit.MachineProductRow.LocalLabel line 259
  19. abbrev OAI.MaxCutGames.Explicit.MachineProductRow.Label line 262
  20. def OAI.MaxCutGames.Explicit.MachineProductRow.localMain line 265
  21. def OAI.MaxCutGames.Explicit.MachineProductRow.localInstruction line 268
  22. def OAI.MaxCutGames.Explicit.MachineProductRow.entry line 273
  23. def OAI.MaxCutGames.Explicit.MachineProductRow.instruction line 277
  24. def OAI.MaxCutGames.Explicit.MachineProductRow.outputTape line 283
  25. def OAI.MaxCutGames.Explicit.MachineProductRow.appendField line 285
  26. def OAI.MaxCutGames.Explicit.MachineProductRow.rowBits line 289

    Source documentation

    Exact literal output of the command list in field order.

    def rowBits (values : Command width → Nat) (commands : List (Command width)) : List Bool :=
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductRow.Command

  27. def OAI.MaxCutGames.Explicit.MachineProductRow.result line 292
  28. theorem OAI.MaxCutGames.Explicit.MachineProductRow.resultOf_eq line 296
  29. structure OAI.MaxCutGames.Explicit.MachineProductRow.Ready line 309

    Source documentation

    The input-dependent data needed for one whole row, held invariant by all physical field executions.

    structure Ready (slots : Layout width ↪ K) (table : List Nat) (indices : Fin width → Nat)
    (radices : Bool → Nat) (base : K → List Bool) : Prop where
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductRow.Layout

  30. theorem OAI.MaxCutGames.Explicit.MachineProductRow.Ready.appendField line 316
  31. theorem OAI.MaxCutGames.Explicit.MachineProductRow.rowTrace line 339

    Source documentation

    Complete row trace from the concrete field implementation. The only premises concerning values are literal indexed-table identities and the Horner interpretation of those values.

    theorem rowTrace (slots : Layout width ↪ K) (table : List Nat) (coefficient : Nat)
    (indices : Fin width → Nat) (radices : Bool → Nat) (commands : List (Command width))
    (fields : Command width → Fin width → Nat) (digits : Command width → Nat → Nat)
    (selected : ∀ command ∈ commands, ∀ i,
      table[coefficient * indices i + command.2 i]? = some (fields command i))
    (reversed : ∀ command ∈ commands, ∀ i : Fin width,
      digits command i.val = fields command i.rev)
    (labels : Label slots commands → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
    (atLabels : ∀ l, program (labels l) = instruction slots coefficient commands labels exit l)
    (base : K → List Bool) (ready : Ready slots table indices radices base) (ambient : σ) :
    let values := fun c : Command width => MachineHorner.value (radices c.1) (digits c) width
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductRow.Layout, OAI.MaxCutGames.Explicit.MachineProductRow.Command, OAI.MaxCutGames.Explicit.MachineProductRow.Label, OAI.MaxCutGames.Explicit.MachineProductRow.instruction, OAI.MaxCutGames.Explicit.MachineProductRow.Ready

  32. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.row_table_lookup line 400

    Source documentation

    Indexing a flattened constant-width row list preserves the literal field position, not merely the multiset of row contents.

    theorem row_table_lookup (constraints : List (Constraint n q))
    (e : Fin constraints.length) (field : Fin (q + 2)) :
    (constraints.flatMap constraintWords)[(q + 2) * e.val + field.val]? =
      (constraintWords constraints[e])[field.val]? := by
…
  33. def OAI.MaxCutGames.Explicit.ProductMachineSemantics.inputTable line 421
  34. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.inputTable_source line 423
  35. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.inputTable_target line 428
  36. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.inputTable_image line 433
  37. def OAI.MaxCutGames.Explicit.ProductMachineSemantics.reverseDigits line 440
  38. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.reverseDigits_at line 443
  39. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.reverseDigits_words line 446
  40. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.horner_ofFin line 459
  41. def OAI.MaxCutGames.Explicit.ProductMachineSemantics.sourceCommand line 465
  42. def OAI.MaxCutGames.Explicit.ProductMachineSemantics.targetCommand line 466
  43. def OAI.MaxCutGames.Explicit.ProductMachineSemantics.imageCommand line 467
  44. def OAI.MaxCutGames.Explicit.ProductMachineSemantics.commands line 472

    Source documentation

    The complete fixed-alphabet row schedule: two endpoints followed by every forward-table entry in increasing numeric label order.

    def commands (q t : ℕ) : List (MachineProductRow.Command t) :=
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductRow.Command

  45. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.commands_length line 475
  46. def OAI.MaxCutGames.Explicit.ProductMachineSemantics.fields line 478
  47. def OAI.MaxCutGames.Explicit.ProductMachineSemantics.fieldValue line 482
  48. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.source_fields line 487
  49. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.target_fields line 492
  50. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.image_fields line 497
  51. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.selected line 507

    Source documentation

    Every scheduled lookup selects an actual word in the input table.

    theorem selected (H : Instance q) (edges : Fin t → Fin H.constraints.length)
    (c : MachineProductRow.Command t) (hc : c ∈ commands q t) (i : Fin t) :
    (inputTable H)[(q + 2) * (edges i).val + c.2 i]? =
      some (fields H edges c i) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductRow.Command, OAI.MaxCutGames.Explicit.ProductMachineSemantics.commands, OAI.MaxCutGames.Explicit.ProductMachineSemantics.inputTable, OAI.MaxCutGames.Explicit.ProductMachineSemantics.fields

  52. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.command_offset_lt line 519
  53. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.fields_lt line 530
  54. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.source_value line 543
  55. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.target_value line 550
  56. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.image_value line 557
  57. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.encodeWords_map_inline_ProductMachineSemantics line 567
  58. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.rowBits_eq line 575

    Source documentation

    The controller's literal field-command output is the serialized semantic row, including every forward permutation-table entry.

    theorem rowBits_eq (H : Instance q) (presentation : SimpleBipartite H)
    (t : ℕ) (ht : 0 < t) (i : Fin (H.constraints.length ^ t)) :
    MachineProductRow.rowBits (fieldValue H (finFunctionFinEquiv.symm i)) (commands q t) =
      encodeWords (constraintWords (ProductPaddedOutput.outputRow H presentation t ht i)) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductRow.rowBits, OAI.MaxCutGames.Explicit.ProductMachineSemantics.fieldValue, OAI.MaxCutGames.Explicit.ProductMachineSemantics.commands, OAI.MaxCutGames.Explicit.ProductPaddedOutput.outputRow

  59. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.encodeWords_flatMap_inline_ProductMachineSemantics line 601
  60. def OAI.MaxCutGames.Explicit.ProductMachineSemantics.allRowsBits line 609

    Source documentation

    Product rows are emitted in ascending radix address, exactly the literal order of the output constraint list.

    def allRowsBits (H : Instance q) (t : ℕ) : List Bool :=
…
  61. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.allRowsBits_eq line 613
  62. theorem OAI.MaxCutGames.Explicit.ProductMachineSemantics.gameBits_eq line 629

    Source documentation

    Concatenating the three computed headers and all physical row fields yields precisely the target serialization, including list order and full tables.

    theorem gameBits_eq (H : Instance q) (presentation : SimpleBipartite H)
    (t : ℕ) (ht : 0 < t) :
    encodeWords [H.vertices ^ t, q ^ t, H.constraints.length ^ t] ++ allRowsBits H t =
      gameBits (ProductPaddedOutput.output H presentation t ht) := by
…

    Mentions: OAI.MaxCutGames.Explicit.ProductMachineSemantics.allRowsBits, OAI.MaxCutGames.Explicit.ProductPaddedOutput.output

  63. def OAI.MaxCutGames.Explicit.MachineProductPower.digits line 651
  64. theorem OAI.MaxCutGames.Explicit.MachineProductPower.value_eq line 653
  65. abbrev OAI.MaxCutGames.Explicit.MachineProductPower.Label line 660
  66. def OAI.MaxCutGames.Explicit.MachineProductPower.instruction line 662
  67. def OAI.MaxCutGames.Explicit.MachineProductPower.steps line 669
  68. theorem OAI.MaxCutGames.Explicit.MachineProductPower.powerTrace line 674

    Source documentation

    Header powers are computed from a unary input radix, not stored in an unbounded register. Only the output accumulator changes at the boundary.

    theorem powerTrace (slots : MachineHorner.Layout (exponent + 1) ↪ K) (output : K)
    (outside : ∀ i, output ≠ slots i) (labels : Label exponent → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
    (atLabels : ∀ l, program (labels l) = instruction slots output labels exit l)
    (base : K → List Bool) (radix : Nat)
    (radixWord : base (slots (.inl 0)) = encodeWord radix)
    (digitWords : ∀ i : Fin (exponent + 1), base (slots (.inr i)) = encodeWord (digits i.val))
    (clean : MachineHorner.Clean slots base) (fieldEmpty : base (slots (.inl 3)) = [])
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[steps radix exponent]
      (some ⟨some (labels (.inl .start)), ((ambient, ()), register), base⟩) =
      some ⟨exit, ((ambient, ()), none),
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductPower.Label, OAI.MaxCutGames.Explicit.MachineProductPower.instruction, OAI.MaxCutGames.Explicit.MachineProductPower.digits, OAI.MaxCutGames.Explicit.MachineProductPower.steps

  69. def OAI.MaxCutGames.Explicit.MachineProductPower.timePolynomial line 716
  70. theorem OAI.MaxCutGames.Explicit.MachineProductPower.steps_le line 720