GapReduction.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

Encodings and reductions for uniform sparsest cut

These definitions express the polynomial-time reduction and approximation search problem in Constant-factor hardness of uniform sparsest cut by OpenAI. The last semantic implication uses rational threshold comparison.

abbrev OAI.UniformSparsestCut.BitString line 19
def OAI.UniformSparsestCut.block line 22
Source documentation
A self-delimiting binary block: unary length, terminator, then the bits.
```
def block (s : BitString) : BitString := List.replicate s.length true ++ false :: s
```
Mentions: OAI.UniformSparsestCut.BitString
def OAI.UniformSparsestCut.encodeNat line 25
Source documentation
Binary, not unary, representation of a natural number, with a length prefix.
```
def encodeNat (n : ℕ) : BitString := block (Computability.encodeNat n)
```
Mentions: OAI.UniformSparsestCut.BitString, OAI.UniformSparsestCut.block
def OAI.UniformSparsestCut.encodeRat line 28
Source documentation
Signed numerator and positive denominator, both in binary.
```
def encodeRat (q : ℚ) : BitString :=
…
```
Mentions: OAI.UniformSparsestCut.BitString
def OAI.UniformSparsestCut.encodePair line 31
def OAI.UniformSparsestCut.encodeBool line 33
def OAI.UniformSparsestCut.Polytime line 41
Source documentation
A finite-stack, finite-alphabet Turing machine with a polynomial step bound.
Mathlib's FinTM2 only supplies alphabet finiteness for the input stack. The extra condition here requires every stack alphabet to be finite. Thus one cannot store an arbitrary natural number or a function in a single stack symbol.
```
def Polytime {α β : Type} (ea : α → BitString) (eb : β → BitString)
    (f : α → β) : Prop :=
…
```
Mentions: OAI.UniformSparsestCut.BitString
structure OAI.UniformSparsestCut.Literal line 47
structure OAI.UniformSparsestCut.Clause line 52
abbrev OAI.UniformSparsestCut.Formula line 59
Source documentation
Exactly three literals per clause; repetitions are permitted.
```
abbrev Formula := List Clause
```
Mentions: OAI.UniformSparsestCut.Clause
def OAI.UniformSparsestCut.Literal.eval line 61
def OAI.UniformSparsestCut.Clause.eval line 64
def OAI.UniformSparsestCut.Satisfiable line 67
def OAI.UniformSparsestCut.Literal.encode line 70
def OAI.UniformSparsestCut.Clause.encode line 72
def OAI.UniformSparsestCut.encodeFormula line 75
def OAI.UniformSparsestCut.formulaSize line 78
def OAI.UniformSparsestCut.encodeGraph line 80
structure OAI.UniformSparsestCut.Instance line 85
Source documentation
The rational threshold is additional to the graph.
```
structure Instance where
…
```
def OAI.UniformSparsestCut.encodeInstance line 90
def OAI.UniformSparsestCut.OutputBound line 95
Source documentation
This records graph size, every numeric bit length, and total output length. The polynomial is quantified inside the choice of the fixed factor.
```
def OutputBound (R : Formula → Instance) (p : Polynomial ℕ) : Prop :=
…
```
Mentions: OAI.UniformSparsestCut.Formula, OAI.UniformSparsestCut.Instance
def OAI.UniformSparsestCut.HasGapReduction line 103
Source documentation
Polynomial-time gap reduction for the specific objective above.
```
def HasGapReduction (C : ℝ) : Prop :=
…
```
def OAI.UniformSparsestCut.cutOfBits line 113
Source documentation
A cut is returned as one bit per vertex, in vertex order.
```
def cutOfBits (G : Graph) (s : BitString) : Finset (Fin G.n) :=
…
```
Mentions: OAI.UniformSparsestCut.Graph, OAI.UniformSparsestCut.BitString
def OAI.UniformSparsestCut.ApproxAnswer line 117
Source documentation
The approximation algorithm must return a feasible cut, not just an estimated value.
```
def ApproxAnswer (C : ℝ) (G : Graph) (s : BitString) : Prop :=
…
```
Mentions: OAI.UniformSparsestCut.Graph, OAI.UniformSparsestCut.BitString
abbrev OAI.UniformSparsestCut.Language line 121
def OAI.UniformSparsestCut.InNP line 124
Source documentation
NP via a deterministic polynomial-time verifier and a polynomial-length certificate.
```
def InNP (L : Language) : Prop :=
…
```
Mentions: OAI.UniformSparsestCut.Language
def OAI.UniformSparsestCut.ApproximationNPHard line 132
Source documentation
NP-hardness of the factor-C search problem, under one-call polynomial-time oracle reductions. The postprocessor must work for every valid approximate answer, not just for a helpful choice of answer.
```
def ApproximationNPHard (C : ℝ) : Prop :=
…
```
def OAI.UniformSparsestCut.bitsOfCut line 139
theorem OAI.UniformSparsestCut.bitsOfCut_length line 142
theorem OAI.UniformSparsestCut.cutOfBits_bitsOfCut line 145
theorem OAI.UniformSparsestCut.exists_approximation_answer line 151
Source documentation
Every graph has a factor-C approximation when C ≥ 1.
```
theorem exists_approximation_answer (G : Graph) {C : ℝ} (hC : 1 ≤ C) :
    ∃ s, ApproxAnswer C G s := by
…
```
Mentions: OAI.UniformSparsestCut.Graph, OAI.UniformSparsestCut.ApproxAnswer
def OAI.UniformSparsestCut.decideGap line 162
Source documentation
Rational comparison of the returned cut with a fixed rational factor B. No real-number oracle is used by this predicate.
```
def decideGap (B : ℚ) (I : Instance) (s : BitString) : Bool :=
…
```
Mentions: OAI.UniformSparsestCut.Instance, OAI.UniformSparsestCut.BitString
theorem OAI.UniformSparsestCut.gap_decision_correct line 167
Source documentation
A gap for a larger rational factor decides satisfiability from every valid approximation at the target real factor.
```
theorem gap_decision_correct {F : Formula} {I : Instance} {C : ℝ} {B : ℚ}
    (hC : 0 ≤ C) (hCB : C ≤ (B : ℝ))
    (hyes : Satisfiable F → I.graph.phi ≤ I.threshold)
    (hno : ¬ Satisfiable F → (B : ℝ) * I.threshold < I.graph.phi)
    {s : BitString} (hs : ApproxAnswer C I.graph s) :
    decideGap B I s = true ↔ Satisfiable F := by
…
```
Mentions: OAI.UniformSparsestCut.Formula, OAI.UniformSparsestCut.Instance, OAI.UniformSparsestCut.Satisfiable, OAI.UniformSparsestCut.BitString, OAI.UniformSparsestCut.ApproxAnswer, OAI.UniformSparsestCut.decideGap