OAI/Computability/MaxCut/Machines/MachineFixedDivMod.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

The two actual division phases of the expander-row program. Static state conjugation connects the fixed-divisor machine to the common emitter state. Only the concrete statement placement equations are premises; no phase trace or whole-row execution is assumed. Each phase has exactly n + 2 transitions.

  1. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.Alphabet line 15
  2. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.State line 16
  3. def OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.residue line 18
  4. def OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.nextResidue line 21
  5. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.nextResidue_residue line 24
  6. def OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.scanLoop line 30
  7. def OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.emitter line 44

    Source documentation

    Each emitter is a fixed finite statement indexed by one of the d residues.

    def emitter (d : Nat) (positive : 0 < d) (remainder : K) (exit : Option Λ)
    (r : Fin d) : TM2.Stmt (Alphabet (K := K)) Λ (State σ d) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.State

  8. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.scanPushBound line 51
  9. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.emitterPushBound line 57
  10. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.tapes line 65

    Source documentation

    Three designated tapes, with the complete surrounding tape family retained.

    abbrev tapes (source quotient remainder : K) (base : K → List Bool)
    (input quotientWord remainderWord : List Bool) : K → List Bool :=
…
  11. def OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes line 69
  12. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_source line 74
  13. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_quotient line 82
  14. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_remainder line 89
  15. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_other line 96
  16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.update_source_inline_MachineFixedDivMod line 104
  17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.update_quotient_inline_MachineFixedDivMod line 122
  18. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.update_remainder_inline_MachineFixedDivMod line 136
  19. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.scanAux_true line 142
  20. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.scanAux_false line 158
  21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.scanStep_succ line 173

    Source documentation

    A scan transition updates the actual quotient and finite residue of the already-processed count. The count itself is a proof index, not machine state.

    theorem scanStep_succ (d : Nat) (positive : 0 < d) (source quotient remainder : K)
    (sourceQuotient : source ≠ quotient) (sourceRemainder : source ≠ remainder)
    (quotientRemainder : quotient ≠ remainder) (scanLabel : Λ) (emitterLabel : Fin d → Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ d))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.State

  22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.scanStep_zero line 200
  23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.emitterStep line 223
  24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.trace_fromCount line 249

    Source documentation

    The general invariant starts at the finite residue and unary quotient of k, then scans n additional input bits. It is an actual execution theorem.

    theorem trace_fromCount (d : Nat) (positive : 0 < d) (source quotient remainder : K)
    (sourceQuotient : source ≠ quotient) (sourceRemainder : source ≠ remainder)
    (quotientRemainder : quotient ≠ remainder) (scanLabel : Λ) (emitterLabel : Fin d → Λ)
    (exit : Option Λ) (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ d))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.State

  25. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.divModTrace line 287

    Source documentation

    Exact unary quotient and remainder, with both output counters initially zero.

    theorem divModTrace (d : Nat) (positive : 0 < d) (source quotient remainder : K)
    (sourceQuotient : source ≠ quotient) (sourceRemainder : source ≠ remainder)
    (quotientRemainder : quotient ≠ remainder) (scanLabel : Λ) (emitterLabel : Fin d → Λ)
    (exit : Option Λ) (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ d))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.State

  26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.divModFromTapes line 309

    Source documentation

    Caller-frame form: the only initial tape hypotheses are the three unary prefixes.

    theorem divModFromTapes (d : Nat) (positive : 0 < d) (source quotient remainder : K)
    (sourceQuotient : source ≠ quotient) (sourceRemainder : source ≠ remainder)
    (quotientRemainder : quotient ≠ remainder) (scanLabel : Λ) (emitterLabel : Fin d → Λ)
    (exit : Option Λ) (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ d))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.State

  27. def OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.divModInTime line 336
  28. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.scanTrace_fromCount line 361

    Source documentation

    Stop just before emission, retaining the final finite residue as actual control.

    theorem scanTrace_fromCount (d : Nat) (positive : 0 < d) (source quotient remainder : K)
    (sourceQuotient : source ≠ quotient) (sourceRemainder : source ≠ remainder)
    (quotientRemainder : quotient ≠ remainder) (scanLabel : Λ) (emitterLabel : Fin d → Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ d))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.State

  29. def OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.emitterWithFinish line 395

    Source documentation

    A fixed table on finite ambient control may retain the residue before local reset.

    def emitterWithFinish [Fintype σ] (d : Nat) (positive : 0 < d) (remainder : K)
    (exit : Option Λ) (finish : σ → Fin d → σ) (r : Fin d) :
    TM2.Stmt (Alphabet (K := K)) Λ (State σ d) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.State

  30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.emitterWithFinishPushBound line 403
  31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.emitterWithFinishStep line 411
  32. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.divModTraceWithFinish line 438

    Source documentation

    The callback is a fixed finite-control table, applied in the existing emitter transition.

    theorem divModTraceWithFinish [Fintype σ] (d : Nat) (positive : 0 < d)
    (source quotient remainder : K)
    (sourceQuotient : source ≠ quotient) (sourceRemainder : source ≠ remainder)
    (quotientRemainder : quotient ≠ remainder) (scanLabel : Λ) (emitterLabel : Fin d → Λ)
    (exit : Option Λ) (finish : σ → Fin d → σ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ d))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.State

  33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.divModFromTapesWithFinish line 466
  34. inductive OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape line 503
  35. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape.enumList line 510
  36. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape.enumList_getElem?_ctorIdx_eq line 514
  37. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape.enumList_nodup line 518
  38. instance OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.(instance at line 520) line 520
  39. inductive OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Label line 524
  40. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Ambient line 542
  41. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.State line 543
  42. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.divisionStates line 548

    Source documentation

    The residue and the emitter's unit field are just permuted; no tape is read or written by this static change of finite state coordinates.

    def divisionStates (ρ : Type) (d : Nat) :
    MachineFixedDivMod.State (Ambient ρ d × Unit) (degree d) ≃ State ρ d where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Ambient, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.State

  43. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.firstFinish line 555
  44. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.secondFinish line 559
  45. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.affinePlan line 563
  46. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.firstPlan line 568
  47. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.secondPlan line 572
  48. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.outputPlan line 576
  49. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupTape line 580
  50. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.dirtyTape line 587
  51. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.statement line 599

    Source documentation

    Every branch is a concrete finite TM2 statement. The fixed table H is evaluated only on finite control values, never on an unbounded tape value.

    def statement {d : Nat} (positive : 0 < d) (H : Table (cloudSize d) d)
    (ports : Tape → K) (labels : Label d → Λ) (exit : Option Λ) :
    Label d → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d)
  | .initialize =>
    .push (ports .quotientFirst) (fun _ => false)
      (.push (ports .quotientSecond) (fun _ => false)
        (.push (ports .remainderFirst) (fun _ => false)
          (.push (ports .remainderSecond) (fun _ => false)
            (.load (fun s => (s.1, none))
              (.goto fun _ => labels (.firstEmit (PCP.AlphabetTable.Emitter.labelAt 3 _ 0 .entry)))))))
  | .firstEmit l =>
    PCP.AlphabetTable.Emitter.statement (firstPlan ρ d) (fun _ => ports .inputVertex)
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.State, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.labelAt, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.statement, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.firstPlan

  52. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.program line 664
  53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.controlStatement_inverse_inline_MachineExpanderRowDivision line 682
  54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.transportedDivision_inline_MachineExpanderRowDivision line 691

    Source documentation

    Pull the actual target program into division-state coordinates, derive its trace from its concrete statements, then transport every actual transition back.

    private theorem transportedDivision_inline_MachineExpanderRowDivision {K Λ σ τ : Type} [DecidableEq K] [Fintype σ]
    (q : Nat) (positive : 0 < q) (source quotient remainder : K)
    (sourceQuotient : source ≠ quotient) (sourceRemainder : source ≠ remainder)
    (quotientRemainder : quotient ≠ remainder)
    (states : MachineFixedDivMod.State σ q ≃ τ)
    (scanLabel : Λ) (emitterLabel : Fin q → Λ) (exit : Option Λ)
    (finish : σ → Fin q → σ)
    (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ τ)
    (atScan : target scanLabel = MachineControl.statement id states
      (MachineFixedDivMod.scanLoop q positive source quotient scanLabel emitterLabel))
    (atEmitter : ∀ r, target (emitterLabel r) = MachineControl.statement id states
      (MachineFixedDivMod.emitterWithFinish q positive remainder exit finish r))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.State, OAI.MaxCutGames.Foundations.Complexity.MachineControl.statement, OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.scanLoop, OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.emitterWithFinish

  55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.divisionStates_apply line 750
  56. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.divisionState line 755

    Source documentation

    The common row state at a division boundary, with its local residue reset.

    def divisionState {d : Nat} (positive : 0 < d) (ambient : ρ) (control : Control d)
    (register : Option Bool) : State ρ d :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.State

  57. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.divisionOutput line 760
  58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.firstDivisionTrace line 767

    Source documentation

    Exact first lookup-result division, including the receiveFirst control update.

    theorem firstDivisionTrace {d : Nat} (positive : 0 < d) (H : Table (cloudSize d) d)
    (ports : Tape → K) (portsInjective : Function.Injective ports)
    (labels : Label d → Λ) (exit : Option Λ)
    (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d))
    (atProgram : ∀ label, target (labels label) = statement positive H ports labels exit label)
    (base : K → List Bool) (n : Nat)
    (sourceSuffix quotientSuffix remainderSuffix : List Bool)
    (sourceInput : base (ports .lookupOutput) = encodeWord n ++ sourceSuffix)
    (quotientInput : base (ports .quotientFirst) = encodeWord 0 ++ quotientSuffix)
    (remainderInput : base (ports .remainderFirst) = encodeWord 0 ++ remainderSuffix)
    (ambient : ρ) (control : Control d) (register : Option Bool) :
    (MachineComposition.advance (TM2.step target))^[n + 2]
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.statement, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance

  59. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.secondDivisionTrace line 809

    Source documentation

    Exact second division, including receiveSecond and the actual output-emitter entry label.

    theorem secondDivisionTrace {d : Nat} (positive : 0 < d) (H : Table (cloudSize d) d)
    (ports : Tape → K) (portsInjective : Function.Injective ports)
    (labels : Label d → Λ) (exit : Option Λ)
    (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d))
    (atProgram : ∀ label, target (labels label) = statement positive H ports labels exit label)
    (base : K → List Bool) (n : Nat)
    (sourceSuffix quotientSuffix remainderSuffix : List Bool)
    (sourceInput : base (ports .lookupOutput) = encodeWord n ++ sourceSuffix)
    (quotientInput : base (ports .quotientSecond) = encodeWord 0 ++ quotientSuffix)
    (remainderInput : base (ports .remainderSecond) = encodeWord 0 ++ remainderSuffix)
    (ambient : ρ) (control : Control d) (register : Option Bool) :
    (MachineComposition.advance (TM2.step target))^[n + 2]
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.statement, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance

  60. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_source line 853
  61. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_quotient line 865
  62. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_remainder line 874
  63. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_other line 881
  64. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.firstDivisionInTime line 891
  65. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.secondDivisionInTime line 915