Documentation

Complexitylib.Classes.PCP.Internal.AlgPosNum

A composed position's number #

A read of the assembled tester lands in one of three kinds of block: the encoding block of a vertex, a dart's linear table, or a dart's quadratic table. Which kind, and which cube inside the block, depends only on the read and the random string — with two exceptions, where the cube is shifted by the arithmetization of the dart's satisfying set. Which block, on the other hand, is a vertex or a dart of the outer graph, so it is the only part that grows with the input.

This module splits a position's number along that seam.

Main definitions #

Main results #

source
def Complexity.RegCSP.readKind :
ReadIdx → ℕ

Which kind of block a read's position lies in: an encoding block (0), a dart's linear table (1), or a dart's quadratic table (2).

Equations
Instances For
    source
    noncomputable def Complexity.RegCSP.blockNum {β : Type} (R : RegCSP β) [NumEnc R.graph.V] [NumEnc R.graph.D] (p : R.Dart) :
    ReadIdx → ℕ

    The number of the vertex or dart whose block a read's position lies in.

    Equations
    Instances For
      source
      noncomputable def Complexity.RegCSP.cubeOfSet {B : ℕ} (S : Finset (BooleanAnalysis.Cube (Tester.kOf B))) (z : BooleanAnalysis.Cube (Tester.ROf B)) :
      ReadIdx → ℕ

      The cube a read names, from the satisfying set alone.

      Equations
      Instances For
        source
        noncomputable def Complexity.RegCSP.cubeNum {β : Type} [Fintype β] (R : RegCSP β) {B : ℕ} (enc : β → BooleanAnalysis.Cube B) (p : R.Dart) (z : BooleanAnalysis.Cube (Tester.ROf B)) :
        ReadIdx → ℕ

        The number of the cube a read's position names inside its block.

        Equations
        Instances For
          source
          def Complexity.RegCSP.posNum (cardV cardD cardB cardN cardNN k w c : ℕ) :
          ℕ

          The number a kind, a block and a cube make: encoding blocks first, then the linear tables, then the quadratic ones.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem Complexity.RegCSP.enc_pos_compose {β : Type} [Fintype β] (R : RegCSP β) [NumEnc R.graph.V] [NumEnc R.graph.D] {B : ℕ} (enc : β → BooleanAnalysis.Cube B) (p : R.Dart) (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx) :
            NumEnc.enc ((compose enc R).pos p z i) = posNum (NumEnc.card R.graph.V) (NumEnc.card R.graph.D) (NumEnc.card (BooleanAnalysis.Cube B)) (NumEnc.card (BooleanAnalysis.Cube (Tester.nOf B))) (NumEnc.card (BooleanAnalysis.Cube (Tester.nOf B * Tester.nOf B))) (readKind i) (R.blockNum p i) (R.cubeNum enc p z i)

            A composed position's number.

            source
            theorem Complexity.RegCSP.blockNum_i5r {β : Type} (R : RegCSP β) [NumEnc R.graph.V] [NumEnc R.graph.D] (p : R.Dart) :
            R.blockNum p ReadIdx.i5r = NumEnc.enc p / NumEnc.card R.graph.D

            The block of an input read is the dart's tail, which its number names by division.

            source
            theorem Complexity.RegCSP.blockNum_i6r {β : Type} (R : RegCSP β) [NumEnc R.graph.V] [NumEnc R.graph.D] (p : R.Dart) :
            R.blockNum p ReadIdx.i6r = NumEnc.enc (R.graph.rot p).1

            The block of the other input read is the dart's head.

            source
            theorem Complexity.RegCSP.val_head_toGraph_compose {β : Type} [Fintype β] (R : RegCSP β) [NumEnc R.graph.V] [NumEnc R.graph.D] {B : ℕ} (enc : β → BooleanAnalysis.Cube B) (k : Fin (Fintype.card (compose enc R).Edge)) :
            ↑((compose enc R).toGraph.head k) = posNum (NumEnc.card R.graph.V) (NumEnc.card R.graph.D) (NumEnc.card (BooleanAnalysis.Cube B)) (NumEnc.card (BooleanAnalysis.Cube (Tester.nOf B))) (NumEnc.card (BooleanAnalysis.Cube (Tester.nOf B * Tester.nOf B))) (readKind ((compose enc R).edgeOf k).2.2) (R.blockNum ((compose enc R).edgeOf k).1 ((compose enc R).edgeOf k).2.2) (R.cubeNum enc ((compose enc R).edgeOf k).1 ((compose enc R).edgeOf k).2.1 ((compose enc R).edgeOf k).2.2)

            The second endpoint of a composed edge.

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

            The test's verdict, from the satisfying set alone.

            Equations
            Instances For
              source
              theorem Complexity.RegCSP.cubeNum_eq_cubeOfSet {β : Type} [Fintype β] (R : RegCSP β) {B : ℕ} (enc : β → BooleanAnalysis.Cube B) (p : R.Dart) (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx) :
              R.cubeNum enc p z i = cubeOfSet (satSet enc R p) z i

              The cube depends on the satisfying set alone.

              source
              theorem Complexity.RegCSP.check_eq_checkOfSet {β : Type} [Fintype β] (R : RegCSP β) {B : ℕ} (enc : β → BooleanAnalysis.Cube B) (p : R.Dart) (z : BooleanAnalysis.Cube (Tester.ROf B)) :
              (compose enc R).check p z = checkOfSet (satSet enc R p) z

              And so does the verdict.

              source
              theorem Complexity.RegCSP.edge_facts {β : Type} [Fintype β] (R : RegCSP β) [NumEnc R.graph.V] [NumEnc R.graph.D] {B : ℕ} (enc : β → BooleanAnalysis.Cube B) (e : ℕ) (he : e < (compose enc R).toGraph.numEdges) :
              ∃ (p : R.Dart) (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx), e = ((NumEnc.enc p.1 * NumEnc.card R.graph.D + NumEnc.enc p.2) * 2 ^ Tester.ROf B + NumEnc.enc z) * 22 + NumEnc.enc i ∧ ↑((compose enc R).toGraph.tail ⟨e, he⟩) = (compose enc R).tailNum e ∧ ↑((compose enc R).toGraph.head ⟨e, he⟩) = posNum (NumEnc.card R.graph.V) (NumEnc.card R.graph.D) (NumEnc.card (BooleanAnalysis.Cube B)) (NumEnc.card (BooleanAnalysis.Cube (Tester.nOf B))) (NumEnc.card (BooleanAnalysis.Cube (Tester.nOf B * Tester.nOf B))) (readKind i) (R.blockNum p i) (R.cubeNum enc p z i) ∧ (compose enc R).toGraph.rel ⟨e, he⟩ = MultiTest.relOfCheck ((compose enc R).check p z) i

              An edge's data and all three of its numbers, in one package: a caller never has to spell the composed system out, nor match anything against it.

              Everything depends on the dart's constraint alone #

              source
              theorem Complexity.RegCSP.satSet_congr {β : Type} [Fintype β] (R : RegCSP β) {B : ℕ} (enc : β → BooleanAnalysis.Cube B) {R' : RegCSP β} (p : R.Dart) (p' : R'.Dart) (h : R.rel p.1 p.2 = R'.rel p'.1 p'.2) :
              satSet enc R p = satSet enc R' p'

              The satisfying set depends only on the dart's constraint.

              source
              theorem Complexity.RegCSP.cubeNum_congr {β : Type} [Fintype β] (R : RegCSP β) {B : ℕ} (enc : β → BooleanAnalysis.Cube B) {β' : Type} [Fintype β'] [DecidableEq β'] [Nonempty β'] {R' : RegCSP β'} [NumEnc R'.graph.V] [NumEnc R'.graph.D] {enc' : β' → BooleanAnalysis.Cube B} (p : R.Dart) (p' : R'.Dart) (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx) (h : satSet enc R p = satSet enc' R' p') :
              R.cubeNum enc p z i = R'.cubeNum enc' p' z i

              So does the cube a read names, even across two different systems.

              source
              theorem Complexity.RegCSP.check_congr {β : Type} [Fintype β] (R : RegCSP β) {B : ℕ} (enc : β → BooleanAnalysis.Cube B) {β' : Type} [Fintype β'] [DecidableEq β'] [Nonempty β'] {R' : RegCSP β'} [NumEnc R'.graph.V] [NumEnc R'.graph.D] {enc' : β' → BooleanAnalysis.Cube B} (p : R.Dart) (p' : R'.Dart) (z : BooleanAnalysis.Cube (Tester.ROf B)) (h : satSet enc R p = satSet enc' R' p') :
              (compose enc R).check p z = (compose enc' R').check p' z

              And so does the test's verdict.

              Across two graphs #

              source
              theorem Complexity.satSet_eq_of_data {α : Type} [Fintype α] [DecidableEq α] (G G' : ConstraintGraph α) (E : ExpanderFamily) {q T B : ℕ} (hq : 0 < q) (v : (G.preprocess E).graph.V) (v' : (G'.preprocess E).graph.V) (x : (Fin T → (G.preprocess E).graph.D) × (Fin T → Fin q)) (encβ : KOpinion (G.preprocess E).graph T α → BooleanAnalysis.Cube B) (hpar : (fun (i : Fin ((G.preprocess E).graph.kLen x)) => NumEnc.enc ((G.preprocess E).graph.walkAt ((G.preprocess E).graph.kLen x) v ((G.preprocess E).graph.kWalk x) ↑i) % 2) = fun (i : Fin ((G'.preprocess E).graph.kLen x)) => NumEnc.enc ((G'.preprocess E).graph.walkAt ((G'.preprocess E).graph.kLen x) v' ((G'.preprocess E).graph.kWalk x) ↑i) % 2) (hcode : (fun (i : Fin ((G.preprocess E).graph.kLen x)) => codeOfRel (G.rel ((G.preprocess E).graph.walkAt ((G.preprocess E).graph.kLen x) v ((G.preprocess E).graph.kWalk x) ↑i).1)) = fun (i : Fin ((G'.preprocess E).graph.kLen x)) => codeOfRel (G'.rel ((G'.preprocess E).graph.walkAt ((G'.preprocess E).graph.kLen x) v' ((G'.preprocess E).graph.kWalk x) ↑i).1)) (hend : (G.preprocess E).graph.endIdx ⋯ v ((G.preprocess E).graph.kWalk x) = (G'.preprocess E).graph.endIdx ⋯ v' ((G'.preprocess E).graph.kWalk x)) :
              RegCSP.satSet encβ ((G.preprocess E).killedPow q T hq) (v, x) = RegCSP.satSet encβ ((G'.preprocess E).killedPow q T hq) (v', x)

              Two graphs whose walks show the same data have the same satisfying set. Both sides live in Finset (Cube (kOf B)), a type that does not mention either graph.

              source
              theorem Complexity.cubeNum_eq_of_data {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G G' : ConstraintGraph α) (E : ExpanderFamily) {q T B : ℕ} (hq : 0 < q) (v : (G.preprocess E).graph.V) (v' : (G'.preprocess E).graph.V) (x : (Fin T → (G.preprocess E).graph.D) × (Fin T → Fin q)) (encβ : KOpinion (G.preprocess E).graph T α → BooleanAnalysis.Cube B) (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx) (h : RegCSP.satSet encβ ((G.preprocess E).killedPow q T hq) (v, x) = RegCSP.satSet encβ ((G'.preprocess E).killedPow q T hq) (v', x)) :
              ((G.preprocess E).killedPow q T hq).cubeNum encβ (v, x) z i = ((G'.preprocess E).killedPow q T hq).cubeNum encβ (v', x) z i

              The cube a read names is the same across two such graphs.

              source
              theorem Complexity.check_eq_of_data {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G G' : ConstraintGraph α) (E : ExpanderFamily) {q T B : ℕ} (hq : 0 < q) (v : (G.preprocess E).graph.V) (v' : (G'.preprocess E).graph.V) (x : (Fin T → (G.preprocess E).graph.D) × (Fin T → Fin q)) (encβ : KOpinion (G.preprocess E).graph T α → BooleanAnalysis.Cube B) (z : BooleanAnalysis.Cube (Tester.ROf B)) (h : RegCSP.satSet encβ ((G.preprocess E).killedPow q T hq) (v, x) = RegCSP.satSet encβ ((G'.preprocess E).killedPow q T hq) (v', x)) :
              (RegCSP.compose encβ ((G.preprocess E).killedPow q T hq)).check (v, x) z = (RegCSP.compose encβ ((G'.preprocess E).killedPow q T hq)).check (v', x) z

              And so is the test's verdict.