OAI/Computability/MaxCut/Machines/MachineRhsLoad.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Execute all fixed outcome rows after the existing RHS loader. A single dispatcher freezes the loaded finite RHS vector into labels. Every row is an actual address-edge phase; no row-run or whole-loop execution is assumed. Program definitions contain only fixed templates, literal permutations, and tape/label placement. Numeric names, radix, and capacity occur only in tapes and the semantic correctness hypotheses.

  1. abbrev OAI.MaxCutGames.Reduction.MachineRhsLoad.State line 11
  2. abbrev OAI.MaxCutGames.Reduction.MachineRhsLoad.Alphabet line 12
  3. def OAI.MaxCutGames.Reduction.MachineRhsLoad.rhs line 14
  4. def OAI.MaxCutGames.Reduction.MachineRhsLoad.setRhs line 16
  5. theorem OAI.MaxCutGames.Reduction.MachineRhsLoad.rhs_setRhs line 19
  6. theorem OAI.MaxCutGames.Reduction.MachineRhsLoad.setRhs_setRhs line 22
  7. theorem OAI.MaxCutGames.Reduction.MachineRhsLoad.setRhs_same line 25
  8. def OAI.MaxCutGames.Reduction.MachineRhsLoad.fill line 27
  9. theorem OAI.MaxCutGames.Reduction.MachineRhsLoad.fill_apply line 30
  10. theorem OAI.MaxCutGames.Reduction.MachineRhsLoad.fill_all line 43
  11. def OAI.MaxCutGames.Reduction.MachineRhsLoad.finish line 51
  12. def OAI.MaxCutGames.Reduction.MachineRhsLoad.peekChain line 56
  13. def OAI.MaxCutGames.Reduction.MachineRhsLoad.statement line 64
  14. def OAI.MaxCutGames.Reduction.MachineRhsLoad.readRhs line 67
  15. theorem OAI.MaxCutGames.Reduction.MachineRhsLoad.stepAux_peekChain line 70
  16. theorem OAI.MaxCutGames.Reduction.MachineRhsLoad.stepAux_statement line 81
  17. theorem OAI.MaxCutGames.Reduction.MachineRhsLoad.readRhs_of_unary line 88
  18. theorem OAI.MaxCutGames.Reduction.MachineRhsLoad.loadStep line 98

    Source documentation

    One actual transition loads every RHS register while preserving all tapes, caller registers, and the existing optional head register.

    theorem loadStep (field : Fin k → K) (entry : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State k σ))
…

    Mentions: OAI.MaxCutGames.Reduction.MachineRhsLoad.Alphabet, OAI.MaxCutGames.Reduction.MachineRhsLoad.State

  19. def OAI.MaxCutGames.Reduction.MachineRhsLoad.loadInTime line 109
  20. theorem OAI.MaxCutGames.Reduction.MachineRhsLoad.peekChain_pushBound line 125
  21. theorem OAI.MaxCutGames.Reduction.MachineRhsLoad.statement_pushBound line 132
  22. structure OAI.MaxCutGames.Reduction.MachineOutcomeRows.Spec line 150
  23. structure OAI.MaxCutGames.Reduction.MachineOutcomeRows.Values line 156

    Source documentation

    Numeric interpretations are proof-side data, separate from the program.

    structure Values (width : Nat) where
…
  24. abbrev OAI.MaxCutGames.Reduction.MachineOutcomeRows.Rhs line 162
  25. abbrev OAI.MaxCutGames.Reduction.MachineOutcomeRows.Row line 163
  26. abbrev OAI.MaxCutGames.Reduction.MachineOutcomeRows.State line 164
  27. abbrev OAI.MaxCutGames.Reduction.MachineOutcomeRows.Alphabet line 165
  28. abbrev OAI.MaxCutGames.Reduction.MachineOutcomeRows.LocalLabel line 169
  29. def OAI.MaxCutGames.Reduction.MachineOutcomeRows.localMain line 173
  30. def OAI.MaxCutGames.Reduction.MachineOutcomeRows.localInstruction line 178
  31. def OAI.MaxCutGames.Reduction.MachineOutcomeRows.payload line 183
  32. def OAI.MaxCutGames.Reduction.MachineOutcomeRows.rowResult line 187
  33. def OAI.MaxCutGames.Reduction.MachineOutcomeRows.rowCost line 192
  34. def OAI.MaxCutGames.Reduction.MachineOutcomeRows.rowCosts line 199

    Source documentation

    Exact per-row costs at their actual accumulated output frames.

    def rowCosts (slots : MachineAddressEdge.Tape q width ↪ K)
    (B C : Nat) (values : Spec q width → Values width) :
    List (Spec q width) → (K → List Bool) → List Nat
  | [], _ => []
  | row :: rows, base => rowCost slots B C values row base ::
      rowCosts slots B C values rows (rowResult slots B C values row base)

    Mentions: OAI.MaxCutGames.Reduction.MachineAddressEdge.Tape, OAI.MaxCutGames.Reduction.MachineOutcomeRows.Spec, OAI.MaxCutGames.Reduction.MachineOutcomeRows.Values, OAI.MaxCutGames.Reduction.MachineOutcomeRows.rowCost, OAI.MaxCutGames.Reduction.MachineOutcomeRows.rowResult

  35. theorem OAI.MaxCutGames.Reduction.MachineOutcomeRows.rowCosts_length line 206
  36. structure OAI.MaxCutGames.Reduction.MachineOutcomeRows.Invariant line 214
  37. theorem OAI.MaxCutGames.Reduction.MachineOutcomeRows.Invariant.appended line 228
  38. theorem OAI.MaxCutGames.Reduction.MachineOutcomeRows.appended_nil line 239
  39. theorem OAI.MaxCutGames.Reduction.MachineOutcomeRows.sequence_result line 243
  40. theorem OAI.MaxCutGames.Reduction.MachineOutcomeRows.sequence_steps line 255
  41. def OAI.MaxCutGames.Reduction.MachineOutcomeRows.sequenceInstruction line 264
  42. theorem OAI.MaxCutGames.Reduction.MachineOutcomeRows.sequenceTrace line 272

    Source documentation

    The generic finite-sequence local obligation is discharged by the concrete edge program, including its address arithmetic and capacity restoration.

    theorem sequenceTrace (slots : MachineAddressEdge.Tape q width ↪ K)
    (rows : List (Spec q width))
    (place : MachineFiniteSequence.Label (LocalLabel slots) rows → Λ) (exit : Option Λ)
    (P : Λ → TM2.Stmt (Alphabet (K := K)) Λ (MachineAddressEdge.State σ))
…

    Mentions: OAI.MaxCutGames.Reduction.MachineAddressEdge.Tape, OAI.MaxCutGames.Reduction.MachineOutcomeRows.Spec, OAI.MaxCutGames.Reduction.MachineOutcomeRows.LocalLabel, OAI.MaxCutGames.Reduction.MachineOutcomeRows.Alphabet, OAI.MaxCutGames.Reduction.MachineAddressEdge.State

  43. def OAI.MaxCutGames.Reduction.MachineOutcomeRows.selected line 299
  44. theorem OAI.MaxCutGames.Reduction.MachineOutcomeRows.selected_length line 302
  45. abbrev OAI.MaxCutGames.Reduction.MachineOutcomeRows.Label line 305
  46. instance OAI.MaxCutGames.Reduction.MachineOutcomeRows.localLabelFintype line 308
  47. instance OAI.MaxCutGames.Reduction.MachineOutcomeRows.localLabelDecidableEq line 311
  48. instance OAI.MaxCutGames.Reduction.MachineOutcomeRows.labelFintype line 322
  49. instance OAI.MaxCutGames.Reduction.MachineOutcomeRows.labelDecidableEq line 325
  50. def OAI.MaxCutGames.Reduction.MachineOutcomeRows.sequenceEntry line 328
  51. def OAI.MaxCutGames.Reduction.MachineOutcomeRows.dispatcher line 336

    Source documentation

    Reuse the RHS vector already loaded by MachineRhsLoad; dispatch takes one real transition, and resets only the optional temporary bit.

    def dispatcher (slots : MachineAddressEdge.Tape q width ↪ K) :
    (rows : List (Row k q width)) → (Label slots rows → Λ) → Option Λ →
      TM2.Stmt (Alphabet (K := K)) Λ (State k σ)
…

    Mentions: OAI.MaxCutGames.Reduction.MachineAddressEdge.Tape, OAI.MaxCutGames.Reduction.MachineOutcomeRows.Row, OAI.MaxCutGames.Reduction.MachineOutcomeRows.Label, OAI.MaxCutGames.Reduction.MachineOutcomeRows.Alphabet, OAI.MaxCutGames.Reduction.MachineOutcomeRows.State

  52. def OAI.MaxCutGames.Reduction.MachineOutcomeRows.instruction line 344
  53. def OAI.MaxCutGames.Reduction.MachineOutcomeRows.program line 351
  54. theorem OAI.MaxCutGames.Reduction.MachineOutcomeRows.dispatcherStep line 355
  55. theorem OAI.MaxCutGames.Reduction.MachineOutcomeRows.phaseTrace line 368
  56. def OAI.MaxCutGames.Reduction.MachineOutcomeRows.phaseInTime line 390
  57. theorem OAI.MaxCutGames.Reduction.MachineOutcomeRows.emitted_output line 407
  58. theorem OAI.MaxCutGames.Reduction.MachineOutcomeRows.exact_row_count line 416
  59. def OAI.MaxCutGames.Reduction.MachineOutcomeRows.timePolynomial line 424

    Source documentation

    Sum of fixed row polynomials; the additional constant is the dispatcher. This proof-side polynomial contains no runtime input field values.

    noncomputable def timePolynomial (rows : List (Spec q width)) : Polynomial Nat :=
…

    Mentions: OAI.MaxCutGames.Reduction.MachineOutcomeRows.Spec

  60. theorem OAI.MaxCutGames.Reduction.MachineOutcomeRows.rowCosts_sum_le line 428
  61. theorem OAI.MaxCutGames.Reduction.MachineOutcomeRows.phaseCost_le_timePolynomial line 459

    Source documentation

    The actual dispatcher-and-rows count is bounded by a fixed polynomial in explicit tape and digit magnitudes, using the checked edge arithmetic bound.

    theorem phaseCost_le_timePolynomial (slots : MachineAddressEdge.Tape q width ↪ K)
    (rows : List (Spec q width)) (base : K → List Bool)
    (B C : Nat) (values : Spec q width → Values width) (M : Nat)
    (clean : MachineAddressEdge.Clean slots base)
    (fieldsBound : ∀ j, (base (MachineAddressEdge.addressSlots slots (.field j))).length ≤ M)
    (radixBound : B ≤ M) (capacityBound : C ≤ M)
    (valuesBound : ∀ row ∈ rows,
      (encodeWords (values row).left).length ≤ M ∧
      (encodeWords (values row).right).length ≤ M ∧
      (∀ i, i < width → MachineTemplateAddress.digits (values row).left i ≤ M) ∧
      (∀ i, i < width → MachineTemplateAddress.digits (values row).right i ≤ M)) :
    (rowCosts slots B C values rows base).sum + 1 ≤ (timePolynomial rows).eval M := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineAddressEdge.Tape, OAI.MaxCutGames.Reduction.MachineOutcomeRows.Spec, OAI.MaxCutGames.Reduction.MachineOutcomeRows.Values, OAI.MaxCutGames.Reduction.MachineAddressEdge.Clean, OAI.MaxCutGames.Reduction.MachineAddressEdge.addressSlots, OAI.MaxCutGames.Reduction.MachineTemplateAddress.digits, OAI.MaxCutGames.Reduction.MachineOutcomeRows.rowCosts, OAI.MaxCutGames.Reduction.MachineOutcomeRows.timePolynomial