Polynomial-time evaluation of powered constraints

The walk length, killing rate and finite edge-label type are fixed. The graph, starting vertex, and both endpoint opinion tables are runtime data; their encodings are charged in full. This is not a certificate uniform in varying walk lengths, killing rates or alphabet encodings.

Main results

• Cslib.PCP.RegularConstraintGraph.isPolyTime_powerRelationWithInput: joint evaluation cost.

References

• I. Dinur, The PCP theorem by gap amplification

noncomputable def Cslib.PCP.RegularConstraintGraph.powerInputEncoding {P W D α : Type} [Fintype D] (input : P ↪ List Bool) (vertex : W ↪ List Bool) (label : D ↪ List Bool) (alphabet : α ↪ List Bool) (T q : ℕ) (signal : Fin q ↪ List Bool) : PowerInput P W D α T q ↪ List Bool

The runtime graph, vertex, complete walk and both opinion tables are all stored explicitly.

theorem Cslib.PCP.RegularConstraintGraph.isPolyTime_powerRelationWithInput {P W D α : Type} {input : P ↪ List Bool} {vertex : W ↪ List Bool} {label : D ↪ List Bool} {alphabet : α ↪ List Bool} {rotate : P × W × D → W × D} {rel : P × (W × D) × α × α → Bool} [Fintype D] (hrotate : Turing.MultiTapeTM.ComputableInPolyTime rotate (Turing.MultiTapeTM.encPair input (Turing.MultiTapeTM.encPair vertex label)) (Turing.MultiTapeTM.encPair vertex label)) (hrel : Turing.MultiTapeTM.ComputableInPolyTime rel (Turing.MultiTapeTM.encPair input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair vertex label) (Turing.MultiTapeTM.encPair alphabet alphabet))) Turing.MultiTapeTM.encBool) (T q : ℕ) [NeZero q] (signal : Fin q ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime (powerRelationWithInput rotate rel T q) (powerInputEncoding input vertex label alphabet T q signal) Turing.MultiTapeTM.encBool

Every original relation call, intermediate walk vertex, reverse-label table and opinion lookup is charged. The finite dispatch depends only on the fixed walk parameters.