Model.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.MaxCutGames.BinaryFormula.Literal line 7
Also declared: ComparatorChallenges/OptimalMaxCut.lean:7 (same declaration text).
def OAI.MaxCutGames.BinaryFormula.Literal.eval line 12
Also declared: ComparatorChallenges/OptimalMaxCut.lean:12 (same declaration text).
abbrev OAI.MaxCutGames.BinaryFormula.Clause line 15
Also declared: ComparatorChallenges/OptimalMaxCut.lean:15 (same declaration text).
def OAI.MaxCutGames.BinaryFormula.Clause.eval line 17
Also declared: ComparatorChallenges/OptimalMaxCut.lean:17 (same declaration text).
structure OAI.MaxCutGames.BinaryFormula.Formula line 22
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/OptimalMaxCut.lean:22 (same declaration text).
```
structure Formula where
…
```
def OAI.MaxCutGames.BinaryFormula.Formula.Satisfiable line 25
Also declared: ComparatorChallenges/OptimalMaxCut.lean:25 (same declaration text).
def OAI.MaxCutGames.BinaryEncoding.bitsValue line 34
Also declared: ComparatorChallenges/OptimalMaxCut.lean:34 (same declaration text).
def OAI.MaxCutGames.BinaryEncoding.frame line 39
Source documentation
Prefix-free framing on the two-symbol input alphabet.
Also declared: ComparatorChallenges/OptimalMaxCut.lean:39 (same declaration text).
```
def frame : List Bool → List Bool
  | [] => [false]
  | b :: bits => true :: b :: frame bits
```
def OAI.MaxCutGames.BinaryEncoding.parseFrame line 43
Also declared: ComparatorChallenges/OptimalMaxCut.lean:43 (same declaration text).
def OAI.MaxCutGames.BinaryEncoding.nameBits line 50
Also declared: ComparatorChallenges/OptimalMaxCut.lean:50 (same declaration text).
def OAI.MaxCutGames.BinaryEncoding.parseName line 53
Source documentation
Equality with the canonical digits rejects alternate padded encodings.
Also declared: ComparatorChallenges/OptimalMaxCut.lean:53 (same declaration text).
```
def parseName (input : List Bool) : Option (Nat × List Bool) := do
…
```
def OAI.MaxCutGames.BinaryEncoding.parseLiteral line 58
Also declared: ComparatorChallenges/OptimalMaxCut.lean:58 (same declaration text).
def OAI.MaxCutGames.BinaryEncoding.parseClause line 64
Also declared: ComparatorChallenges/OptimalMaxCut.lean:64 (same declaration text).

def OAI.MaxCutGames.BinaryEncoding.parseClauses line 71

Source documentation

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

Also declared: ComparatorChallenges/OptimalMaxCut.lean:71 (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.MaxCutGames.BinaryEncoding.parseClause

def OAI.MaxCutGames.BinaryEncoding.decodeFormula line 80
Also declared: ComparatorChallenges/OptimalMaxCut.lean:80 (same declaration text).
def OAI.OptimalMaxCut.alphaGW line 91
Source documentation
The exact Goemans–Williamson ratio, as an infimum over -1 ≤ ρ < 1.
Also declared: ComparatorChallenges/OptimalMaxCut.lean:91 (same declaration text).
```
noncomputable def alphaGW : ℝ :=
…
```
def OAI.OptimalMaxCut.binary3SAT line 96
Source documentation
The ordinary binary 3SAT language, including rejection of malformed words.
Also declared: ComparatorChallenges/OptimalMaxCut.lean:96 (same declaration text).
```
def binary3SAT (input : List Bool) : Prop :=
…
```
structure OAI.OptimalMaxCut.Graph line 101
Source documentation
A finite simple unweighted graph with its full Boolean adjacency table.
Also declared: ComparatorChallenges/OptimalMaxCut.lean:101 (same declaration text).
```
structure Graph where
…
```
def OAI.OptimalMaxCut.Graph.cutSize line 108
Source documentation
Each unordered distinct edge crossing the cut is counted exactly once.
Also declared: ComparatorChallenges/OptimalMaxCut.lean:108 (same declaration text).
```
def Graph.cutSize (G : Graph) (cut : Fin G.vertices → Bool) : ℕ :=
…
```
Mentions: OAI.OptimalMaxCut.Graph
def OAI.OptimalMaxCut.Graph.maxCut line 113
Source documentation
The maximum over all Boolean cuts of the finite vertex set.
Also declared: ComparatorChallenges/OptimalMaxCut.lean:113 (same declaration text).
```
def Graph.maxCut (G : Graph) : ℕ :=
…
```
Mentions: OAI.OptimalMaxCut.Graph
structure OAI.OptimalMaxCut.ScaledGraph line 118
Source documentation
The positive integer scale Q is part of the output. It need not equal the number of graph edges.
Also declared: ComparatorChallenges/OptimalMaxCut.lean:118 (same declaration text).
```
structure ScaledGraph where
…
```
def OAI.OptimalMaxCut.ScaledGraph.bits line 125
Source documentation
Canonical delimited binary vertex count and scale, followed by the full adjacency table in lexicographic order.
Also declared: ComparatorChallenges/OptimalMaxCut.lean:125 (same declaration text).
```
def ScaledGraph.bits (G : ScaledGraph) : List Bool :=
…
```
Mentions: OAI.OptimalMaxCut.ScaledGraph
structure OAI.OptimalMaxCut.GapReduction line 133
Source documentation
The rational gap bounds and the finite machine are fixed before the input. The bounds compare the maximum cut divided by the positive output scale.
Also declared: ComparatorChallenges/OptimalMaxCut.lean:133 (same declaration text).
```
structure GapReduction (α : ℝ) where
…
```
def OAI.OptimalMaxCut.MainStatement line 148
Also declared: ComparatorChallenges/OptimalMaxCut.lean:148 (same declaration text).