Documentation

Complexitylib.Classes.PCP.Internal.Compose

Dinur's composition: alphabet reduction #

The powering step leaves a constraint graph over an enormous (though constant) alphabet. Composition brings the alphabet back down to a fixed one, at the cost of a constant factor in the unsatisfiability value that does not depend on the alphabet being reduced. That independence is what lets the powering step's gain win.

The construction: every vertex of the outer graph gets a block of positions holding the Hadamard encoding of its label; every dart gets a proof for the assembled tester of TesterCore, whose input tables are the encodings at its two ends and whose constraint is the dart's relation, spelled out on encoded pairs. The tester's reads make a MultiTest, and LocalTest turns it into a binary constraint graph over the fixed alphabet Alpha ReadIdx.

Soundness decodes an assignment of the composed graph to one of the outer graph by nearest codeword at every vertex. Whenever the decoded assignment violates a dart, that dart's tester rejects on a 1/32 fraction of its random strings — otherwise the tester's own soundness would produce a satisfying pair whose encodings are close to both blocks, and closeness to a codeword pins the decoded labels down. Each rejecting string costs one of the 22 edges it owns.

Main definitions #

Main results #

The reads #

source
inductive Complexity.ReadIdx :
Type

The tester's reads, by check: linearity of F (three), linearity of G (three), consistency (six), the constraint (four), and the two input tables (three each: the input coordinate and two self-correction reads).

Instances For
    source
    @[instance_reducible]
    instance Complexity.instDecidableEqReadIdx :
    DecidableEq ReadIdx
    Equations
    source
    @[instance_reducible]
    instance Complexity.instFintypeReadIdx :
    Fintype ReadIdx

    All twenty-two reads, in declaration order.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem Complexity.card_readIdx :
    Fintype.card ReadIdx = 22
    source
    instance Complexity.instNonemptyReadIdx :
    Nonempty ReadIdx
    source
    @[instance_reducible]
    noncomputable instance Complexity.instNumEncReadIdx :
    NumEnc ReadIdx

    The reads are numbered by their own enumeration: there are twenty-two of them, so this is a lookup on a bounded key.

    Equations

    Signs and bits #

    source
    theorem Complexity.chi_eq_chi_iff (u v : ZMod 2) :
    BooleanAnalysis.chi u = BooleanAnalysis.chi v ↔ u = v
    source
    theorem Complexity.signBit_signOf_mul {m : ℕ} (F : BooleanAnalysis.Cube m → ZMod 2) (u v : BooleanAnalysis.Cube m) :
    signBit (signOf F u * signOf F v) = F u + F v
    source
    theorem Complexity.signOf_mul_eq_iff {m : ℕ} (F : BooleanAnalysis.Cube m → ZMod 2) (u v w : BooleanAnalysis.Cube m) :
    signOf F u * signOf F v = signOf F w ↔ F u + F v = F w

    The checks as a formula on the bits read #

    source
    noncomputable def Complexity.Tester.bitFormula {B : ℕ} (S : Finset (BooleanAnalysis.Cube (kOf B))) (z : BooleanAnalysis.Cube (ROf B)) (rd : ReadIdx → ZMod 2) :
    Prop

    The tester's verdict as a formula on the bits it read.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      noncomputable instance Complexity.Tester.instDecidableBitFormula {B : ℕ} (S : Finset (BooleanAnalysis.Cube (kOf B))) (z : BooleanAnalysis.Cube (ROf B)) (rd : ReadIdx → ZMod 2) :
      Decidable (bitFormula S z rd)
      Equations
      source
      noncomputable def Complexity.Tester.readsOf {B : ℕ} (Tt Th : BooleanAnalysis.Cube B → ZMod 2) (F : BooleanAnalysis.Cube (nOf B) → ZMod 2) (G : BooleanAnalysis.Cube (nOf B * nOf B) → ZMod 2) (S : Finset (BooleanAnalysis.Cube (kOf B))) (z : BooleanAnalysis.Cube (ROf B)) :
      ReadIdx → ZMod 2

      The bits the tester reads from the four tables.

      Equations
      Instances For
        source
        theorem Complexity.Tester.allChecks_iff {B : ℕ} (S : Finset (BooleanAnalysis.Cube (kOf B))) (Tt Th : BooleanAnalysis.Cube B → ZMod 2) (F : BooleanAnalysis.Cube (nOf B) → ZMod 2) (G : BooleanAnalysis.Cube (nOf B * nOf B) → ZMod 2) (z : BooleanAnalysis.Cube (ROf B)) :
        AllChecks S Tt Th F G z ↔ bitFormula S z (readsOf Tt Th F G S z)

        The verdict is the formula on the reads.

        The composition #

        source
        noncomputable def Complexity.RegCSP.vecOf {B : ℕ} (t : BooleanAnalysis.Cube B → ZMod 2) :
        BooleanAnalysis.Cube (2 ^ B)

        A bit table on Cube B, as a vector indexed by Fin (2 ^ B).

        Equations
        Instances For
          source
          noncomputable def Complexity.RegCSP.inputVec {β : Type} {B : ℕ} (enc : β → BooleanAnalysis.Cube B) (σ τ : β) :
          BooleanAnalysis.Cube (Tester.kOf B)

          The tester's input variables for a pair of labels: the two encodings.

          Equations
          Instances For
            source
            theorem Complexity.RegCSP.tailPart_of_leftBlock {β : Type} {B : ℕ} (enc : β → BooleanAnalysis.Cube B) (σ τ : β) (a : BooleanAnalysis.Cube (Tester.nOf B)) (h : leftBlock a = inputVec enc σ τ) :
            Tester.tailPart a = hadamard (enc σ)
            source
            theorem Complexity.RegCSP.headPart_of_leftBlock {β : Type} {B : ℕ} (enc : β → BooleanAnalysis.Cube B) (σ τ : β) (a : BooleanAnalysis.Cube (Tester.nOf B)) (h : leftBlock a = inputVec enc σ τ) :
            Tester.headPart a = hadamard (enc τ)
            source
            noncomputable def Complexity.RegCSP.satSet {β : Type} {B : ℕ} (enc : β → BooleanAnalysis.Cube B) [Fintype β] (R : RegCSP β) (p : R.Dart) :
            Finset (BooleanAnalysis.Cube (Tester.kOf B))

            The satisfying set of a dart: the encoded pairs its relation accepts.

            Equations
            Instances For
              source
              theorem Complexity.RegCSP.mem_satSet_iff {β : Type} {B : ℕ} (enc : β → BooleanAnalysis.Cube B) [Fintype β] (R : RegCSP β) (p : R.Dart) (w : BooleanAnalysis.Cube (Tester.kOf B)) :
              w ∈ satSet enc R p ↔ ∃ (σ : β) (τ : β), R.rel p.1 p.2 σ τ = true ∧ inputVec enc σ τ = w
              source
              @[reducible, inline]
              abbrev Complexity.RegCSP.Pos {β : Type} {B : ℕ} (R : RegCSP β) :
              Type

              The positions of the composed proof: an encoding block per vertex, and a linear and a quadratic table per dart.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def Complexity.RegCSP.compose {β : Type} {B : ℕ} (enc : β → BooleanAnalysis.Cube B) [Fintype β] (R : RegCSP β) :
                MultiTest R.Pos R.Dart ReadIdx

                The composed test: for each dart, the assembled tester on the encodings at its ends and its own proof tables.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def Complexity.RegCSP.tailTable {β : Type} {B : ℕ} (R : RegCSP β) (T : MultiTest.Table R.Pos) (p : R.Dart) :
                  BooleanAnalysis.Cube B → ZMod 2

                  The encoding block at a dart's tail, as the tester's first input table.

                  Equations
                  Instances For
                    source
                    noncomputable def Complexity.RegCSP.headTable {β : Type} {B : ℕ} (R : RegCSP β) (T : MultiTest.Table R.Pos) (p : R.Dart) :
                    BooleanAnalysis.Cube B → ZMod 2

                    The encoding block at a dart's head, as the tester's second input table.

                    Equations
                    Instances For
                      source
                      noncomputable def Complexity.RegCSP.linTable {β : Type} {B : ℕ} (R : RegCSP β) (T : MultiTest.Table R.Pos) (p : R.Dart) :
                      BooleanAnalysis.Cube (Tester.nOf B) → ZMod 2

                      A dart's linear proof table.

                      Equations
                      Instances For
                        source
                        noncomputable def Complexity.RegCSP.quadTable {β : Type} {B : ℕ} (R : RegCSP β) (T : MultiTest.Table R.Pos) (p : R.Dart) :
                        BooleanAnalysis.Cube (Tester.nOf B * Tester.nOf B) → ZMod 2

                        A dart's quadratic proof table.

                        Equations
                        Instances For
                          source
                          theorem Complexity.RegCSP.accepts_compose_iff {β : Type} {B : ℕ} (enc : β → BooleanAnalysis.Cube B) [Fintype β] (R : RegCSP β) (T : MultiTest.Table R.Pos) (p : R.Dart) (z : BooleanAnalysis.Cube (Tester.ROf B)) :
                          (compose enc R).accepts T p z = true ↔ Tester.AllChecks (satSet enc R p) (R.tailTable T p) (R.headTable T p) (R.linTable T p) (R.quadTable T p) z

                          The composed test runs the tester.

                          Soundness #

                          source
                          noncomputable def Complexity.RegCSP.decodeAssign {β : Type} {B : ℕ} (enc : β → BooleanAnalysis.Cube B) [Fintype β] [Nonempty β] (R : RegCSP β) [NumEnc R.graph.V] [NumEnc R.graph.D] (A : (compose enc R).toGraph.Assignment) :
                          R.Assignment

                          Decoding an assignment of the composed graph: nearest codeword at each vertex.

                          Equations
                          Instances For
                            source
                            theorem Complexity.RegCSP.card_rejects_ge {β : Type} {B : ℕ} (enc : β → BooleanAnalysis.Cube B) [Fintype β] [Nonempty β] (R : RegCSP β) [NumEnc R.graph.V] [NumEnc R.graph.D] (henc : Function.Injective enc) (A : (compose enc R).toGraph.Assignment) (p : R.Dart) (hp : ¬R.Satisfies (decodeAssign enc R A) p) :
                            2 ^ Tester.ROf B ≤ 32 * ((compose enc R).rejects ((compose enc R).tableOf A) p).card

                            A violated dart rejects a 1/32 fraction of its random strings.

                            source
                            theorem Complexity.RegCSP.unsatFrac_compose_ge {β : Type} {B : ℕ} (enc : β → BooleanAnalysis.Cube B) [Fintype β] [Nonempty β] (R : RegCSP β) [NumEnc R.graph.V] [NumEnc R.graph.D] (henc : Function.Injective enc) (A : (compose enc R).toGraph.Assignment) :
                            R.unsatFrac (decodeAssign enc R A) / 704 ≤ (compose enc R).toGraph.unsatFrac A

                            Soundness of composition, per assignment: the composed graph's violated fraction is at least the decoded assignment's, divided by 704 = 32 · 22.

                            source
                            theorem Complexity.RegCSP.le_unsatVal_compose {β : Type} {B : ℕ} (enc : β → BooleanAnalysis.Cube B) [Fintype β] [Nonempty β] (R : RegCSP β) [NumEnc R.graph.V] [NumEnc R.graph.D] (henc : Function.Injective enc) :
                            R.unsatVal / 704 ≤ (compose enc R).toGraph.unsatVal

                            Soundness of composition.

                            Completeness #

                            source
                            noncomputable def Complexity.RegCSP.honestTable {β : Type} {B : ℕ} (enc : β → BooleanAnalysis.Cube B) (R : RegCSP β) (σ : R.Assignment) :
                            MultiTest.Table R.Pos

                            The honest proof of a satisfying assignment: encodings at the vertices, and for each dart the Hadamard tables of the one-hot extension of its encoded pair.

                            Equations
                            Instances For
                              source
                              theorem Complexity.RegCSP.satisfiable_compose {β : Type} {B : ℕ} (enc : β → BooleanAnalysis.Cube B) [Fintype β] (R : RegCSP β) [NumEnc R.graph.V] [NumEnc R.graph.D] (h : R.Satisfiable) :
                              (compose enc R).toGraph.Satisfiable

                              Completeness of composition.