PoweringOpinionTables.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Bounded first-address tables for actual powering constraints

For a graph with numbered vertices and ports, each stored local-opinion index is the first address in allAddresses that reaches the requested vertex. The search traverses bounded port words, never the ambient vertex set.

The walk table stores one base dart and two address indices per traversed edge. Looking up the endpoint labels at those indices gives exactly the existing finitePortSelector decoders, including when addresses collide. The resulting finite table predicate equals the actual powering predicate.

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.match_in_tail line 28
def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.firstIndex line 35
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.get_firstIndex line 44
Source documentation
The stored index selects the very same first address as scanWitness, not just an address with the same endpoint.
```
theorem get_firstIndex (p : X → Prop) [DecidablePred p] :
    ∀ (xs : List X) (h : ∃ a ∈ xs, p a),
      xs.get (firstIndex p xs h) = (scanWitness p xs h).val := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.firstIndex
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.firstIndex_matches line 57
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.firstIndex_is_first line 63
Source documentation
Every earlier stored address fails the matching predicate.
```
theorem firstIndex_is_first (p : X → Prop) [DecidablePred p] :
    ∀ (xs : List X) (h : ∃ a ∈ xs, p a) (j : Fin xs.length),
      j.val < (firstIndex p xs h).val → ¬p (xs.get j) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.firstIndex
abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.AddressIndex line 80
Source documentation
A local label slot is an index into the explicit bounded address list.
```
abbrev AddressIndex (d t : Nat) := Fin (allAddresses d t).length
…
```
def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.addressIndex line 84
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.addressIndex_get line 91
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.addressIndex_matches line 100
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.addressIndex_is_first line 106
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.addressIndex_lt line 113
Source documentation
The address bound depends on degree and radius, not the vertex count.
```
theorem addressIndex_lt (G : PortGraph (Fin vertices) (Fin d)) (t : Nat)
    (center : Fin vertices) (u : Ball G t center) :
    (addressIndex G t center u).val < ∑ n : Fin (t + 1), d ^ n.val := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.addressIndex
abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.LabelTable line 119
def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.labelTable line 122
Source documentation
Materialize a padded label in the common address order.
```
def labelTable {t : Nat} (a : PaddedLabel (Fin d) t A) : LabelTable d t A :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.LabelTable
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.labelTable_get line 125
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.labelTable_addressIndex line 132
Source documentation
Exact evaluation bridge for every local target, with no consistency assumption on labels at distinct addresses that reach the same vertex.
```
theorem labelTable_addressIndex (G : PortGraph (Fin vertices) (Fin d)) (t : Nat)
    (center : Fin vertices) (u : Ball G t center) (a : PaddedLabel (Fin d) t A) :
    (labelTable a)[addressIndex G t center u] =
      decode (finitePortSelector G t center) a u := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.labelTable, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.addressIndex
structure OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.WalkOpinionRow line 140
Source documentation
One finite row for each constraint checked along a recorded walk.
```
structure WalkOpinionRow (vertices d t : Nat) where
…
```
abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.WalkRows line 145
def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.walkRows line 148
Source documentation
The only target vertices inspected are the actual edge endpoints.
```
def walkRows (G : PortGraph (Fin vertices) (Fin d)) (n : Nat)
    (w : Walk (Fin vertices) (Fin d) (n + 1)) : WalkRows vertices d n :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.WalkRows
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.walkRows_edge line 155
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.walkRows_tail_value line 160
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.walkRows_head_value line 168
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.walkRows_length line 176
def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.rowsAccepts line 183
Source documentation
Evaluate an already stored row vector by finite label lookups. The only quantified type is the bounded set of walk positions.
```
def rowsAccepts {n : Nat} (accepts : Edge (Fin vertices) (Fin d) → A → A → Bool)
    (rows : WalkRows vertices d n) (a b : LabelTable d (n + 1) A) : Bool :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.WalkRows, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.LabelTable
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.rowsAccepts_walkRows line 189
Source documentation
The stored finite lookup predicate implements the actual powering test.
```
theorem rowsAccepts_walkRows (G : PortGraph (Fin vertices) (Fin d))
    (accepts : Edge (Fin vertices) (Fin d) → A → A → Bool) (n : Nat)
    (w : Walk (Fin vertices) (Fin d) (n + 1))
    (a b : PaddedLabel (Fin d) (n + 1) A) :
    rowsAccepts accepts (walkRows G n w) (labelTable a) (labelTable b) =
      PoweringTest.pathAccepts G accepts n (finitePortSelector G (n + 1)) w a b := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.rowsAccepts, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.walkRows, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinionTables.labelTable, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.pathAccepts