Addresses.lean`

51 declarations, 0 contain sorry, 0 declared as axioms

Affine numeric fields of the alphabet-reduction table

The five unbounded unary inputs are n, m, e, tail, head, in that order. Every field uses a fixed list of natural coefficients and one bounded offset. For a fixed local event and slot, the query field's coefficient list does not depend on the input predicate. The predicate changes only its bounded offset. Evaluation uses the same Emitter.affineValue as the actual unary emitter.

abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.Terms line 24
structure OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.Field line 26
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.values line 30
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.eval line 32
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.fieldBound line 36
Source documentation
One q-only bound covers every coefficient and every finite offset.
```
def fieldBound (q : Nat) : Nat :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.fieldBound_pos line 39
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.tapeCount_lt_bound line 43
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.pairTapeCount_lt_bound line 47
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.localCount_lt_bound line 51
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.local_add_pair_lt_bound line 55
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.twelve_local_lt_bound line 59
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.zeroOffset line 63
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.eventOffset line 65
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.rawQueryOffset line 69
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.reverseOffset line 75
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.headerVertices line 85
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.headerDarts line 88
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.eventVertexField line 91
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.vertexQueryTerms line 95
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.edgeQueryTerms line 98
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms line 101
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.rawQueryField line 105
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.reverseDartField line 108
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.headerVertices_eval line 112
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.headerDarts_eval line 118
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.eventVertexField_eval line 123
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.rawQueryField_eval line 130
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.reverseDartField_eval line 146
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms line 156
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_query line 160
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.queryEventOffset line 168
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent line 173
Source documentation
The sole predicate-dependent component is a bounded finite-state offset.
```
def fieldForQueryEvent (q : Nat) (event : AlphabetGraph.LocalEvent (Fin q))
    (slot : Fin 6) (P : Fin q → Fin q → Bool) : Field (fieldBound q) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.LocalEvent, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.Field, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.fieldBound
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eq_rawQueryField line 177
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eval line 184
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eval_verifier line 193
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms line 202
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.dartTailOffset line 206
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.fieldForDartTail line 210
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.fieldForDartTail_eval line 214
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.CoefficientsBounded line 226
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.headerVertices_coefficients line 229
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.headerDarts_coefficients line 236
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.eventVertexField_coefficients line 242
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_coefficients line 249
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms_coefficients line 267
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.reverseDartField_coefficients line 271
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_length_le line 279
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms_length_le line 285
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms_coefficients line 289
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms_length_le line 296
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.offset_lt line 303