Model.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.UniqueGamesTheorem.Foundations.Target.PermutationTable line 9
Source documentation
Finite forward and inverse tables make totality and invertibility explicit. An eventual external encoding only needs to serialize the forward table.
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:9 (same declaration text).
```
structure PermutationTable (alphabet : Nat) where
…
```
structure OAI.UniqueGamesTheorem.Foundations.Target.Constraint line 15
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:15 (same declaration text).
def OAI.UniqueGamesTheorem.Foundations.Target.Constraint.satisfied line 20
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:20 (same declaration text).
structure OAI.UniqueGamesTheorem.Foundations.Target.Instance line 26
Source documentation
Constraint occurrences are list entries, so repeated parallel edges retain their multiplicity. No weights are hidden in this representation.
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:26 (same declaration text).
```
structure Instance (alphabet : Nat) where
…
```
def OAI.UniqueGamesTheorem.Foundations.Target.countSatisfied line 31
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:31 (same declaration text).
structure OAI.UniqueGamesTheorem.BinaryFormula.Literal line 43
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:43 (same declaration text).
def OAI.UniqueGamesTheorem.BinaryFormula.Literal.eval line 48
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:48 (same declaration text).
abbrev OAI.UniqueGamesTheorem.BinaryFormula.Clause line 51
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:51 (same declaration text).
def OAI.UniqueGamesTheorem.BinaryFormula.Clause.eval line 53
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:53 (same declaration text).
structure OAI.UniqueGamesTheorem.BinaryFormula.Formula line 58
Source documentation
An ordinary conjunction of three-slot clauses with sparse variable names. Repeated names and repeated literals are permitted in every clause.
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:58 (same declaration text).
```
structure Formula where
…
```
def OAI.UniqueGamesTheorem.BinaryFormula.Formula.Satisfiable line 61
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:61 (same declaration text).
def OAI.UniqueGamesTheorem.BinaryEncoding.bitsValue line 70
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:70 (same declaration text).
def OAI.UniqueGamesTheorem.BinaryEncoding.parseFrame line 74
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:74 (same declaration text).
def OAI.UniqueGamesTheorem.BinaryEncoding.parseName line 82
Source documentation
Equality with the canonical digits rejects alternate padded encodings.
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:82 (same declaration text).
```
def parseName (input : List Bool) : Option (Nat × List Bool) := do
…
```
def OAI.UniqueGamesTheorem.BinaryEncoding.parseLiteral line 87
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:87 (same declaration text).
def OAI.UniqueGamesTheorem.BinaryEncoding.parseClause line 93
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:93 (same declaration text).

def OAI.UniqueGamesTheorem.BinaryEncoding.parseClauses line 100

Source documentation

Fuel bounds the number of clause iterations, not the size of any name.

Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:100 (same declaration text).

def parseClauses : Nat → List Bool → Option (List Clause × List Bool)
  | 0, _ => none
  | _ + 1, false :: rest => some ([], rest)
  | fuel + 1, true :: input => do
      let (clause, input) ← parseClause input
      let (clauses, rest) ← parseClauses fuel input
      return (clause :: clauses, rest)
  | _ + 1, [] => none

Mentions: OAI.UniqueGamesTheorem.BinaryEncoding.parseClause

def OAI.UniqueGamesTheorem.BinaryEncoding.decodeFormula line 109
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:109 (same declaration text).
def OAI.UniqueGamesTheorem.BinaryLanguage.language line 119
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:119 (same declaration text).
abbrev OAI.UniqueGamesTheorem.Integration.BinaryLinear.F2 line 126
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:126 (same declaration text).
abbrev OAI.UniqueGamesTheorem.Integration.BinaryLinear.Vector line 128
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:128 (same declaration text).
def OAI.UniqueGamesTheorem.Integration.TranslationTarget.IsTranslationInstance line 137
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:137 (same declaration text).
def OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord line 147
Also declared: ComparatorChallenges/PerfectCompleteness.lean:7 (same declaration text), ComparatorChallenges/UniqueGamesTheorem.lean:147 (same declaration text).
def OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords line 149
Also declared: ComparatorChallenges/PerfectCompleteness.lean:9 (same declaration text), ComparatorChallenges/UniqueGamesTheorem.lean:149 (same declaration text).
def OAI.UniqueGamesTheorem.Foundations.Complexity.tableWords line 159
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:159 (same declaration text).
def OAI.UniqueGamesTheorem.Foundations.Complexity.constraintWords line 162
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:162 (same declaration text).
def OAI.UniqueGamesTheorem.Foundations.Complexity.gameWords line 165
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:165 (same declaration text).
def OAI.UniqueGamesTheorem.Foundations.Complexity.gameBits line 168
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:168 (same declaration text).
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet line 178
Source documentation
Every physical tape has a finite alphabet. Together with M.kFin, this also makes the disjoint union of all physical tape alphabets finite.
Also declared: ComparatorChallenges/PerfectCompleteness.lean:19 (same declaration text), ComparatorChallenges/UniqueGamesTheorem.lean:178 (same declaration text).
```
def FiniteAlphabet (M : FinTM2) : Prop := ∀ k, Finite (M.Γ k)
…
```
structure OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite line 191
Source documentation
A canonical orientation from the false side to the true side. Injectivity is on occurrence indices, so two distinct list entries cannot be parallel even when their constraint tables are different.
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:191 (same declaration text).
```
structure SimpleBipartite {q : Nat} (game : Instance q) where
…
```
structure OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.BinaryGapReduction line 203
Source documentation
Every parameter, coordinate identification, program, and polynomial is fixed before the input quantifier. The identity input encoding measures runtime in the original raw bit length, including sparse binary variable names.
Also declared: ComparatorChallenges/UniqueGamesTheorem.lean:203 (same declaration text).
```
structure BinaryGapReduction (ε δ : ℝ) where
…
```