PoweringMachineGlobal.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

The fixed global powering machine

For fixed degree d and radius parameter n, this is one concrete finite machine: initialization, unary vertex guard, the fixed vertex-row producer, and output-header/cleanup instructions are connected by explicit labels. Its definition takes no input graph, vertex count, or program callback.

The code equations below expose each actual branch for the separate runtime proof. The variable-size input graph and counters reside on physical tapes.

abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.Tape line 23
abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.State line 26
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.placement line 29
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.inputTape line 33
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.outputTape line 36
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.headerVertices line 39
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.headerDarts line 40
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.enumeration line 42
abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.FinishLabel line 46
abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.Label line 48
instance OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.labelFintype line 51
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.initLabels line 55
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.guardLabel line 56
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.bridgeLabel line 57
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.vertexLabels line 59
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.finishLabels line 62
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.finishEntry line 66
Source documentation
Finish first copies the dart-count field, then the vertex-count field.
```
def finishEntry (d n : Nat) : Label d n := finishLabels d n (.inl .seed)
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.Label, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.finishLabels
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.main line 69
Source documentation
Initialization first clones the input's live vertex-count field.
```
def main (d n : Nat) : Label d n := initLabels d n (.inr .seed)
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.Label, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.initLabels
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.program line 72
Source documentation
The complete program, fixed solely by the reduction parameters.
```
def program (d n : Nat) :
    Label d n → TM2.Stmt (fun _ : Tape n => Bool) (Label d n) (State d n)
  | .inl label => PoweringMachineInitialize.instruction
      (PoweringMachineRowBody.capacity n) (PoweringMachineRowBody.bufferSize d n)
      (PCP.PoweringTableLayout.blockSize d n) (initLabels d n) (some (guardLabel d n)) label
  | .inr (.inl false) => MachineUnaryCounter.guard
      (placement n (PoweringMachineTapes.start (PoweringMachineRowBody.capacity n)))
      (bridgeLabel d n) (finishEntry d n)
  | .inr (.inl true) => PoweringMachineOuterLoop.bridge d n (vertexLabels d n) (guardLabel d n)
  | .inr (.inr (.inl label)) => PoweringMachineVertex.instruction n (placement n) (outputTape n)
      (vertexLabels d n) (some (guardLabel d n)) label
  | .inr (.inr (.inr label)) => PoweringMachineFinish.instruction (enumeration n)
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.Label, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.Tape, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.State, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.instruction, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.capacity, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.bufferSize, OAI.MaxCutGames.Foundations.PCP.PoweringTableLayout.blockSize, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.initLabels, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.guardLabel, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.guard, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.placement, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.start, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.bridgeLabel, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.finishEntry, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.bridge, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.vertexLabels, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.instruction, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.outputTape, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.instruction, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.enumeration
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.atInit line 88
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.atGuard line 93
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.atBridge line 98
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.atVertex line 102
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.atFinish line 106
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.machine line 114
Source documentation
All state and control spaces are explicit finite types; only the tapes hold variable-size data.
```
def machine (d n : Nat) : FinTM2 where
…
```
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.machine_code line 125
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.machine_main line 128
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.machine_initialState line 130
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.input_ne_output line 133