Documentation

MIPRE.Background.AnswerReduction.PcpPresentation

The PCP sampler of answer reduction, over F_q #

Piece AR-3a of planning/answer-reduction.md: the typed PCP sampler Ŝ^pcp of the paper's sec:ar-verifier (ld_compiler.tex, eq:V-pcp), as CL presentations over F_q.

The ambient space is V^pcp = ⊕_{i≤5} (V_{i,pt} ⊕ V_{i,coord} ⊕ V_{i,dir}) ⊕ V_{aux,pt} ⊕ V_{6,coord} ⊕ V_{aux,dir}, with coordinates Coord P (10m + 2s + 16 of them, card_coord). There are six copies of the seeded low-degree test on it (regs, regs6):

The overlap is the point of the construction: the i-th block of the sixth copy's point, in the block order SAT.PcpParams.block of the PCP, is the i-th copy's point (block_ptOf_regs6). That is what the answer-reduced decider's consistency subtests compare.

The types are Fin 6 × LIDT.CL.Ty, eighteen of them, each presented in three levels (pres), exactly on the whole space (pres_exactlyOn), with full evaluation the seeded question of its copy (question_eval).

The coordinates #

source
inductive MIPRE.AnswerReduction.Pcp.Coord (P : SAT.PcpParams) :
Type

The coordinates of V^pcp.

Instances For
    source
    def MIPRE.AnswerReduction.Pcp.instDecidableEqCoord.decEq {P✝ : SAT.PcpParams} (x✝ x✝¹ : Coord P✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance MIPRE.AnswerReduction.Pcp.instDecidableEqCoord {P✝ : SAT.PcpParams} :
      DecidableEq (Coord P✝)
      Equations
      source
      def MIPRE.AnswerReduction.Pcp.Coord.equivSum (P : SAT.PcpParams) :
      Coord P ≃ Fin 5 × Fin P.m ⊕ Fin 5 × Fin P.m ⊕ Fin 6 ⊕ Fin (5 + P.s) ⊕ Fin (5 + P.s)

      The coordinates as a sum.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[instance_reducible]
        instance MIPRE.AnswerReduction.Pcp.Coord.instFintype (P : SAT.PcpParams) :
        Fintype (Coord P)
        Equations
        source
        theorem MIPRE.AnswerReduction.Pcp.Coord.card_coord (P : SAT.PcpParams) :
        Fintype.card (Coord P) = 10 * P.m + 2 * P.s + 16

        The six copies #

        source
        def MIPRE.AnswerReduction.Pcp.regs (P : SAT.PcpParams) (i : Fin 5) :
        LIDT.CL.Regs (Coord P) P.m

        The registers of copy i ≤ 5.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def MIPRE.AnswerReduction.Pcp.pt6 (P : SAT.PcpParams) (k : Fin P.m') :
          Coord P

          The k-th coordinate of the concatenated point register V_{6,pt}: the (k mod m)-th coordinate of V_{⌊k/m⌋,pt} for k < 5m, and of V_{aux,pt} beyond.

          Equations
          Instances For
            source
            def MIPRE.AnswerReduction.Pcp.dir6 (P : SAT.PcpParams) (k : Fin P.m') :
            Coord P

            The k-th coordinate of the concatenated direction register V_{6,dir}.

            Equations
            Instances For
              source
              theorem MIPRE.AnswerReduction.Pcp.pt6_injective (P : SAT.PcpParams) :
              Function.Injective (pt6 P)
              source
              theorem MIPRE.AnswerReduction.Pcp.dir6_injective (P : SAT.PcpParams) :
              Function.Injective (dir6 P)
              source
              def MIPRE.AnswerReduction.Pcp.regs6 (P : SAT.PcpParams) :
              LIDT.CL.Regs (Coord P) P.m'

              The registers of copy 6.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem MIPRE.AnswerReduction.Pcp.pt6_block (P : SAT.PcpParams) (i : Fin 5) (j : Fin P.m) :
                pt6 P ⟨↑i * P.m + ↑j, ⋯⟩ = Coord.pt i j

                The j-th coordinate of the i-th block of V_{6,pt} is the j-th coordinate of V_{i,pt}.

                source
                theorem MIPRE.AnswerReduction.Pcp.block_ptOf_regs6 (P : SAT.PcpParams) {F : Type u_1} [Field F] (i : Fin 5) (x : Coord P → F) :
                P.block i ((regs6 P).ptOf x) = (regs P i).ptOf x

                The overlap: the i-th block of the sixth copy's point, in the PCP's block order, is the i-th copy's point.

                The eighteen types #

                source
                @[reducible, inline]
                abbrev MIPRE.AnswerReduction.Pcp.PcpTy :
                Type

                The PCP types: a copy and a low-degree test type.

                Equations
                Instances For
                  source
                  instance MIPRE.AnswerReduction.Pcp.instNeZeroNatM' (P : SAT.PcpParams) :
                  NeZero P.m'
                  source
                  noncomputable def MIPRE.AnswerReduction.Pcp.pres (P : SAT.PcpParams) {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [NeZero P.m] {hm : P.m ∣ Fintype.card F} {hm' : P.m' ∣ Fintype.card F} (S : LIDT.CL.Sel F P.m hm) (S' : LIDT.CL.Sel F P.m' hm') (t : PcpTy) :
                  CL.CLFun F (Coord P) 3

                  The three-level presentation of the PCP type t.

                  Equations
                  Instances For
                    source
                    theorem MIPRE.AnswerReduction.Pcp.pres_exactlyOn (P : SAT.PcpParams) {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [NeZero P.m] {hm : P.m ∣ Fintype.card F} {hm' : P.m' ∣ Fintype.card F} (S : LIDT.CL.Sel F P.m hm) (S' : LIDT.CL.Sel F P.m' hm') (t : PcpTy) :
                    (pres P S S' t).ExactlyOn Finset.univ
                    source
                    def MIPRE.AnswerReduction.Pcp.questionOf (P : SAT.PcpParams) {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [NeZero P.m] {hm : P.m ∣ Fintype.card F} {hm' : P.m' ∣ Fintype.card F} (S : LIDT.CL.Sel F P.m hm) (S' : LIDT.CL.Sel F P.m' hm') (t : PcpTy) (x : Coord P → F) :
                    LIDT.CL.Question F P.m ⊕ LIDT.CL.Question F P.m'

                    The question of a PCP type, read off a vector: a question of the m-variable test for the first five copies, of the m'-variable test for the sixth.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      theorem MIPRE.AnswerReduction.Pcp.question_eval (P : SAT.PcpParams) {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [NeZero P.m] {hm : P.m ∣ Fintype.card F} {hm' : P.m' ∣ Fintype.card F} (S : LIDT.CL.Sel F P.m hm) (S' : LIDT.CL.Sel F P.m' hm') (t : PcpTy) (x : Coord P → F) :
                      questionOf P S S' t ((pres P S S' t).eval x) = if h : ↑t.1 < 5 then Sum.inl (LIDT.CL.Sample.question hm ((regs P ⟨↑t.1, h⟩).sampleOf S t.2 x) t.2) else Sum.inr (LIDT.CL.Sample.question hm' ((regs6 P).sampleOf S' t.2 x) t.2)

                      The presentation computes the seeded question of its copy.