PoweringRowData.lean`

61 declarations, 0 contain sorry, 0 declared as axioms

Actual graph data consumed by the powered-row machine

The data fields are computed from the stored rotor and base relations. The endpoint masks compare actual bounded word endpoints, in allAddresses order. Their first true positions equal the already checked canonical address indices.

Reversing a row swaps the two masks and transposes each base predicate. Thus one fixed row machine handles both directions. Its label lookup depends only on the fixed degree and radius. The final identities describe the exact unary input fields and the exact serialized relation emitted for a stored output row.

These are semantic producer-to-emitter identities. A machine implementation that computes the input data from the serialized rotor is a separate frontend.

theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.firstMatch_of_first line 33

Source documentation

The row machine scans the same increasing address-index order.

theorem firstMatch_of_first {S : Nat} (mask : Fin S → Bool) (i : Fin S)
    (hi : mask i = true) (hfirst : ∀ j : Fin S, j.val < i.val → mask j = false) :
    firstMatch mask = some i := by
…

theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.firstMatch_firstIndex line 43
def OAI.MaxCutGames.Foundations.PCP.PoweringRowData.endpointMask line 53
Source documentation
An actual endpoint comparison; it has no reachability oracle input.
```
def endpointMask (G : PortGraph (Fin vertices) (Fin d)) (t : Nat)
    (center target : Fin vertices) (i : AddressIndex d t) : Bool :=
…
```
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.firstMatch_endpointMask line 57
def OAI.MaxCutGames.Foundations.PCP.PoweringRowData.slotCount line 67
abbrev OAI.MaxCutGames.Foundations.PCP.PoweringRowData.RowBuffer line 69
def OAI.MaxCutGames.Foundations.PCP.PoweringRowData.fixedLabelAt line 72
Source documentation
This lookup is fixed by the reduction parameters, not the input graph.
```
def fixedLabelAt (d n : Nat) (a : Fin (PoweringTables.labelCount d n))
    (i : Fin (slotCount d n)) : GraphTables.Label :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringTables.labelCount, OAI.MaxCutGames.Foundations.PCP.PoweringRowData.slotCount, OAI.MaxCutGames.Foundations.PCP.GraphTables.Label
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.fixedLabelAt_addressIndex line 76

def OAI.MaxCutGames.Foundations.PCP.PoweringRowData.walkData line 86

Source documentation

For each actual path edge, store its complete base relation, then the start-to-tail mask, then the end-to-head mask. Every bit is computed.

def walkData (input : PortTables.Table vertices d) (n : Nat)
    (w : Walk (Fin vertices) (Fin d) (n + 1))
    (k : Fin (n + 1)) : Field (slotCount d n) → Bool
  | .inl (a, b) => PortTables.accepts input (edgeAt (PortTables.portGraph input) n w k) a b
  | .inr (.inl i) => endpointMask (PortTables.portGraph input) (n + 1) w.1
      (edgeAt (PortTables.portGraph input) n w k).1 i
  | .inr (.inr i) => endpointMask (PortTables.portGraph input) (n + 1)
      (endpoint (PortTables.portGraph input) w)
      ((PortTables.portGraph input).rot (edgeAt (PortTables.portGraph input) n w k)).1 i

Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringRowData.slotCount, OAI.MaxCutGames.Foundations.PCP.PortTables.accepts, OAI.MaxCutGames.Foundations.PCP.PortTables.portGraph, OAI.MaxCutGames.Foundations.PCP.PoweringRowData.endpointMask

def OAI.MaxCutGames.Foundations.PCP.PoweringRowData.walkBits line 96
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.basePredicate_walkBits line 100
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.leftMatches_walkBits line 107
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.rightMatches_walkBits line 114
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.firstMatch_walkBits_left line 122
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.firstMatch_walkBits_right line 132
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.edgeAccept_walkBits line 143
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.rowAccept_walkBits line 156
def OAI.MaxCutGames.Foundations.PCP.PoweringRowData.transposeField line 168
Source documentation
Reverse orientation exchanges the two mask fields and label arguments.
```
def transposeField {S : Nat} : Field S → Field S
  | .inl (a, b) => .inl (b, a)
  | .inr (.inl i) => .inr (.inr i)
  | .inr (.inr i) => .inr (.inl i)
```
def OAI.MaxCutGames.Foundations.PCP.PoweringRowData.transposeBits line 173
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.basePredicate_transposeBits line 176
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.leftMatches_transposeBits line 181
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.rightMatches_transposeBits line 187
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.edgeAccept_transposeBits line 193
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.rowAccept_transposeBits line 202
def OAI.MaxCutGames.Foundations.PCP.PoweringRowData.rowBits line 210
Source documentation
The fully specified data block for either directed occurrence.
```
def rowBits (input : PortTables.Table vertices d) (n : Nat)
    (e : PoweringTest.Dart (Fin vertices) (Fin d) n) : RowBuffer d n :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringTest.Dart, OAI.MaxCutGames.Foundations.PCP.PoweringRowData.RowBuffer
def OAI.MaxCutGames.Foundations.PCP.PoweringRowData.rowData line 214
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.rowBits_packData line 219
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.rowBits_field line 226
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.rowAccept_rowBits line 234
Source documentation
No match-mask or base-relation premise remains in the evaluator bridge.
```
theorem rowAccept_rowBits (input : PortTables.Table vertices d) (n : Nat)
    (e : PoweringTest.Dart (Fin vertices) (Fin d) n)
    (a b : Fin (PoweringTables.labelCount d n)) :
    rowAccept (fixedLabelAt d n) (rowBits input n e) a b =
      PoweringTables.rowAccepts input n e a b := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringTest.Dart, OAI.MaxCutGames.Foundations.PCP.PoweringTables.labelCount, OAI.MaxCutGames.Foundations.PCP.PoweringRowData.fixedLabelAt, OAI.MaxCutGames.Foundations.PCP.PoweringRowData.rowBits, OAI.MaxCutGames.Foundations.PCP.PoweringTables.rowAccepts
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.rowBlock_at_rowBits line 244
def OAI.MaxCutGames.Foundations.PCP.PoweringRowData.dataWords line 254
def OAI.MaxCutGames.Foundations.PCP.PoweringRowData.dataTape line 258
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.dataTape_eq line 262
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.dataWords_length line 267
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.dataTape_length_le line 273
def OAI.MaxCutGames.Foundations.PCP.PoweringRowData.emittedRelation line 279
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.emittedRelation_eq line 284
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.rowBlock_unary line 292
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.emittedRelation_table line 305
Source documentation
The emitted bits are the relation of the actual numbered output row.
```
theorem emittedRelation_table (input : PortTables.Table vertices d) (n : Nat)
    (i : Fin (PoweringTables.dartCount vertices d n)) :
    emittedRelation input n (decodeDart vertices d n i) =
      (PoweringTables.table input n).rows[i].relation := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringTables.dartCount, OAI.MaxCutGames.Foundations.PCP.PoweringRowData.emittedRelation, OAI.MaxCutGames.Foundations.PCP.PoweringTables.table
theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowData.rowBlock_unary_table line 332
def OAI.MaxCutGames.Foundations.PCP.PoweringRowData.tableRowMachineInTime line 342
Source documentation
With the actual computed data on its input tape, the existing finite row machine emits precisely the serialized relation of the actual output table. The unread input suffix and prior output tape are preserved as specified.
```
def tableRowMachineInTime (input : PortTables.Table vertices d) (n : Nat)
    (i : Fin (PoweringTables.dartCount vertices d n)) (suffix : List Bool)
    (register : RowBuffer d n) (tapes : Bool → List Bool)
    (hinput : tapes false = dataTape input n (decodeDart vertices d n i) ++ suffix) :
    StateTransition.EvalsToInTime (PoweringMachineRow.machine (t := n + 1) (fixedLabelAt d n)).step
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringTables.dartCount, OAI.MaxCutGames.Foundations.PCP.PoweringRowData.RowBuffer, OAI.MaxCutGames.Foundations.PCP.PoweringRowData.dataTape, OAI.MaxCutGames.Foundations.PCP.PoweringRowData.fixedLabelAt

def OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.tailPorts line 375

Source documentation

The actual ports before a selected time, with no vertex-dependent choice.

def tailPorts : (n : Nat) → (Fin (n + 1) → D) → Fin (n + 1) → List D
  | 0, _, _ => []
  | n + 1, p, k => Fin.cases [] (fun j => p 0 :: tailPorts n (fun i => p i.succ) j) k

theorem OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.tailPorts_length line 379
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.walkEnd_tailPorts line 389
def OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.headPorts line 400
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.walkEnd_headPorts line 403
def OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.addressPorts line 411
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.walkEnd_addressPorts line 414
inductive OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.Instruction line 420
Source documentation
Static commands; all changing vertex identifiers remain inputs to evaluation.
```
inductive Instruction (d : Nat) where
…
```
def OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.Instruction.radius line 425
Source documentation
The number of shared trajectory tapes needed by a single instruction.
```
def Instruction.radius {d : Nat} : Instruction d → Nat
  | .relation ports _ _ _ => ports.length
  | .equal left right => max left.length right.length
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.Instruction
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.addressPorts_length_le line 429
def OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.evaluate line 434
def OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.fieldPlan line 442
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.evaluate_fieldPlan line 448
def OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.directedFieldPlan line 468
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.fieldPlan_radius line 472
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.directedFieldPlan_radius line 487
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.evaluate_directedFieldPlan line 492
def OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.rowPlan line 500
Source documentation
The exact fixed sequence of data-producing commands, in serialized order.
```
def rowPlan {d : Nat} (n : Nat) (ports : Fin (n + 1) → Fin d) (direction : Bool) :
    List (Instruction d) :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.Instruction
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.evaluate_rowPlan line 506
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFieldPlan.dataTape_eq_plan line 517