PoweringMasterState.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Explicit common-register layout for the powering machine. The header, word and affine routines use the trailing optional-bit register directly. Comparison reassociates the finite registers; row evaluation moves the fixed buffer to the final component. The row adapter below proves an actual step of the caller's mixed program, rather than requiring that the entire program be a translated copy of the row routine.

abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.OtherRegisters line 19
abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.Master line 20
abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.CompareState line 21
abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.RowState line 22
def OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.compareEquiv line 25
Source documentation
This is definitionally the state already used by the equality-bit producer.
```
def compareEquiv (N : Nat) : Master N ≃ CompareState N :=
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.Master, OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.CompareState
def OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.rowEquiv line 29
Source documentation
All four finite components are retained by this register permutation.
```
def rowEquiv (N : Nat) : Master N ≃ RowState N where
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.Master, OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.RowState
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.compareEquiv_apply line 35
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.compareEquiv_symm_apply line 39
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.rowEquiv_apply line 43
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.rowEquiv_symm_apply line 47
def OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.withBuffer line 51
def OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.clean line 54
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.equalityBit_clean line 56
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.rowEquiv_withBuffer line 59
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.compareEquiv_withBuffer line 62
def OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.clearBuffer line 66
Source documentation
The row primitive clears only its own buffer; other finite registers survive.
```
def clearBuffer {N : Nat} (state : Master N) : Master N :=
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.Master
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.clearBuffer_apply line 69
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.clearBuffer_withBuffer line 74
def OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.encodedBlockAt line 82
Source documentation
Only this instruction block is translated into the common state.
```
def encodedBlockAt (src dst : K) (F : Buffer N → Buffer M) (exit : Option Λ) :
    TM2.Stmt (fun _ : K => Bool) Λ (Master N) :=
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.Master
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.stepAux_encodedBlockAt line 87

theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.step_encodedBlockAt line 101

Source documentation

Exact caller-program step, with no hypothesis about its other labels.

theorem step_encodedBlockAt (src dst : K) (F : Buffer N → Buffer M) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (Master N))
    (label : Λ) (atLabel : program label = encodedBlockAt src dst F exit)
    (hne : src ≠ dst) (bits : Buffer N) (suffix : List Bool)
    (state : Master N) (tapes : K → List Bool)
    (hinput : tapes src = PoweringMachineRow.encodeBits (List.ofFn bits) ++ suffix) :
    TM2.step program ⟨some label, state, tapes⟩ =
      some ⟨exit, clearBuffer state,
        Function.update (Function.update tapes src suffix) dst
          (PoweringMachineRow.encodeBits (List.ofFn (F bits)) ++ tapes dst)⟩ := by
…

Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.Master, OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.encodedBlockAt, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.encodeBits, OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.clearBuffer

def OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.rowAt line 113
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.step_rowAt_clean line 120
Source documentation
The producer's clean finite controls and any previous buffer contents become the completely clean master state after one genuine row transition.
```
theorem step_rowAt_clean {t S q : Nat} (src dst : K)
    (labelAt : Fin q → Fin S → PCP.GraphTables.Label) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ
      (Master (PoweringMachineRow.inputSize t S)))
    (label : Λ) (atLabel : program label = rowAt (t := t) src dst labelAt exit)
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Label, OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.Master, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRow.inputSize, OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.rowAt
def OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.rowInTime line 137
def OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.headerInTime line 160
Source documentation
Header preparation already has the common trailing-bit register layout.
```
def headerInTime (N B n : Nat) (suffix : List Bool) (state : Master N) :
    StateTransition.EvalsToInTime
      (TM2.step (PoweringMachineLoop.headerProgram (σ := OtherRegisters N) B))
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.Master, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineLoop.headerProgram, OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.OtherRegisters