MachineExpanderRowDivision.lean`

13 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.

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.controlStatement_inverse line 19

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.transportedDivision line 28

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 {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.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineControl.statement, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.scanLoop, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.emitterWithFinish

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.divisionStates_apply line 87
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.divisionState line 92
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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.State
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.divisionOutput line 97

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.firstDivisionTrace line 104

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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.statement, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.advance

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.secondDivisionTrace line 146

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]
…

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.divisionOutput_source line 190
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.divisionOutput_quotient line 202
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.divisionOutput_remainder line 211
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.divisionOutput_other line 218
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.firstDivisionInTime line 228
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.secondDivisionInTime line 252