PoweringMachineRelationLemmas.lean`

102 declarations, 0 contain sorry, 0 declared as axioms

A rotor step on the live unary port-table encoding. First read the reverse dart identifier; then read that dart's tail vertex. This uses no division or runtime graph data in finite control. Both positional selections are proved from the actual serialization.

abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelation.Alphabet line 16
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelation.address line 18
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelation.value line 21
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelation.selected line 25
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelation.instruction line 37
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelation.relationTrace line 44
Source documentation
Actual predicate access, with serialization selection discharged.
```
theorem relationTrace (source : K) (tape : Fin 5 → K)
    (distinct : Function.Injective tape) (outside : ∀ i, source ≠ tape i)
    (port : Fin d) (position : Fin 4096)
    (labels : MachineAffineLookup.Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAffineLookup.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelation.Alphabet
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelation.steps_le line 64

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelation.value_eq_accepts line 75

Source documentation

The semantic two-label predicate is the field used by the row producer.

theorem value_eq_accepts (table : PortTables.Table n d) (vertex : Fin n) (port : Fin d)
    (left right : PortTables.Label) :
    value table vertex port (GraphTables.relationIndex (left, right)) =
      GraphTables.bitWord (PortTables.accepts table (vertex, port) left right) := rfl

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelation.value

def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelation.machine line 80
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.Alphabet line 99
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.reverseRole line 101
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.endpointRole line 104
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.reverseRole_injective line 107
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.endpointRole_injective line 108
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.source_outside_reverse line 109
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.reverse_outside_endpoint line 110
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.reverseTapes line 112
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.endpointTapes line 113
inductive OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.Label line 115
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.instruction line 120
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.reverseId line 129
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.reverseAddress line 132
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.endpointAddress line 135
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.reverse_selected line 138
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.endpoint_selected line 148
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.afterReverse line 154
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.finalTapes line 159
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.steps line 165
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.rotorTrace line 169
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.finalTapes_endpoint line 219
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.finalTapes_other line 230
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.steps_le line 239
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRotor.machine line 258
Source documentation
Its finite description depends on the fixed degree and selected port; the vertex count and graph table are runtime tape data.
```
def machine (degree port : Nat) : FinTM2 where
…
```
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.Alphabet line 285
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.Tape line 286
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.first line 288
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.shift line 290
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.shift_injective line 292
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.rotorRole line 296
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.rotorRole_injective line 301
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.Label line 305
instance OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.labelFintype line 309
instance OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.labelDecidableEq line 316
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.entry line 323
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.copyInstruction line 327
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.instruction line 334
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.steps line 347
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.finalTapes line 353
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.finalTapes_other line 362
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.wordTrace line 383
Source documentation
Actual execution together with its endpoint word. No trace or running-time hypothesis is needed: the recursive proof composes the concrete instructions.
```
theorem wordTrace (table : PortTables.Table n d) (t : Nat)
    (placement : Tape t → K) (distinct : Function.Injective placement)
    (vertex : Fin n) (ports : Fin t → Fin d)
    (labels : Label t → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.Alphabet
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.steps_le line 458
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.machine line 472
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.Tape line 491
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.table line 493
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.start line 494
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.query line 495
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.scan line 496
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.reverse line 497
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.scratch line 498
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.leftEndpoint line 499
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.rightEndpoint line 500
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.leftCopy line 501
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.rightCopy line 502
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.rowOutput line 503
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.endpoint line 505
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.endpoint_false line 508
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.endpoint_true line 509
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordSharedRole line 512
Source documentation
Table, query, scan, reverse identifier, scratch, selected endpoint.
```
def wordSharedRole (target : Bool) (i : Fin 6) : Fin 11 :=
…
```
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.trajectoryPlacement line 518
Source documentation
Position zero is the caller's starting vertex; later positions are the separate physical trajectory tapes.
```
def trajectoryPlacement {t max : Nat} (h : t ≤ max) : Fin (t + 1) → Tape max :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.Tape
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordPlacement line 521
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_zero line 526
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_one line 528
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_two line 530
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_three line 532
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_four line 534
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_five line 536
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordPlacement_first line 538
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordPlacement_succ line 540
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.relationPlacement line 543
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.relationPlacement_zero line 547
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.relationPlacement_one line 548
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.relationPlacement_two line 549
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.relationPlacement_three line 550
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.relationPlacement_four line 551
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.relationPlacement_five line 552
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.equalityPlacement line 554
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_zero line 558
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_one line 559
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_two line 560
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_three line 561
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_four line 562
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_five line 563
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_injective line 565
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_ne_start line 568
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_ne_rowOutput line 572
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.trajectoryPlacement_injective line 576
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordShared_ne_trajectory line 597
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordPlacement_injective line 611
Source documentation
Every tape used by a bounded word is placed on its own physical tape.
```
theorem wordPlacement_injective {t max : Nat} (ht : t ≤ max) (target : Bool) :
    Function.Injective (wordPlacement ht target) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordPlacement
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.relationPlacement_injective line 628
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_injective line 632
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordPlacement_ne_rowOutput line 637
Source documentation
Word subroutines cannot use the row-output tape, even temporarily.
```
theorem wordPlacement_ne_rowOutput {t max : Nat} (ht : t ≤ max) (target : Bool)
    (i : PoweringMachineWord.Tape t) : wordPlacement ht target i ≠ rowOutput max := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordPlacement, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.rowOutput
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.shared_ne_wordPlacement_succ line 655
Source documentation
A shared role is disjoint from every trajectory tape. This supplies the position-frame premise of PoweringMachineWord.finalTapes_other.
```
theorem shared_ne_wordPlacement_succ {t max : Nat} (ht : t ≤ max) (target : Bool)
    (role : Fin 11) (i : Fin t) :
    (Sum.inl role : Tape max) ≠ wordPlacement ht target (.inr i.succ) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.wordPlacement