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.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.OtherRegisters line 22
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.Master line 23
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.CompareState line 24
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.RowState line 25
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.compareEquiv line 28
Source documentation
This is definitionally the state already used by the equality-bit producer.
```
def compareEquiv (N : Nat) : Master N ≃ CompareState N :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.Master, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.CompareState
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.rowEquiv line 32
Source documentation
All four finite components are retained by this register permutation.
```
def rowEquiv (N : Nat) : Master N ≃ RowState N where
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.Master, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.RowState
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.compareEquiv_apply line 38
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.compareEquiv_symm_apply line 42
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.rowEquiv_apply line 46
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.rowEquiv_symm_apply line 50
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.withBuffer line 54
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.clean line 57
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.equalityBit_clean line 59
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.rowEquiv_withBuffer line 62
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.compareEquiv_withBuffer line 65
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.clearBuffer line 69
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.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.Master
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.clearBuffer_apply line 72
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.clearBuffer_withBuffer line 77
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.encodedBlockAt line 85
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.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.Master
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.stepAux_encodedBlockAt line 90

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.step_encodedBlockAt line 104

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.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.Master, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.encodedBlockAt, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.encodeBits, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.clearBuffer

def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.rowAt line 116
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.step_rowAt_clean line 123
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.UniqueGamesTheorem.Foundations.PCP.GraphTables.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.Master, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.inputSize, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.rowAt
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.rowInTime line 140
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.headerInTime line 163
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.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.Master, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineLoop.headerProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.OtherRegisters