Executable constraints for killed-walk powering

The evaluator checks the original constraint at each used step against the two endpoint opinions. It carries the runtime graph through rotation and relation calls, and obtains the reverse labels from the same killed-power program used for the destination vertex. Agreement on valid encoded vertices suffices to identify the result with the existing mathematical powered constraint.

Main definitions

• Cslib.PCP.RegularConstraintGraph.powerRelationWithInput: the Boolean powered constraint.

Main results

• Cslib.PCP.RegularConstraintGraph.powerRelationWithInput_eq_true: exact interpretation.

References

• I. Dinur, The PCP theorem by gap amplification
• J. Radhakrishnan, Gap amplification in PCPs using lazy random walks

@[reducible, inline]

abbrev Cslib.PCP.RegularConstraintGraph.PowerInput (P : Type u_6) (W : Type u_7) (D : Type u_8) (α : Type u_9) (T q : ℕ) : Type (max u_6 (max u_8 u_9) u_8 u_7)

Runtime graph input, a killed walk, and its two endpoint opinions.

def Cslib.PCP.RegularConstraintGraph.powerRelationWithInput {P : Type u_1} {W : Type u_3} {D : Type u_4} {α : Type u_5} (rotate : P × W × D → W × D) (rel : P × (W × D) × α × α → Bool) (T q : ℕ) [NeZero q] (p : PowerInput P W D α T q) : Bool

Check every used step. Unused steps accept, and each endpoint opinion is read at the exact forward or reverse prefix specified by the mathematical powered constraint.

theorem Cslib.PCP.RegularConstraintGraph.powerRelationWithInput_eq_true {P : Type u_1} {V : Type u_2} {W : Type u_3} {D : Type u_4} {α : Type u_5} (rotate : P × W × D → W × D) (rel : P × (W × D) × α × α → Bool) (input : P) (R : RegularConstraintGraph V D α) (encode : V → W) (hrotate : ∀ (v : V) (d : D), rotate (input, encode v, d) = (encode (R.graph.rot (v, d)).1, (R.graph.rot (v, d)).2)) (hrel : ∀ (v : V) (d : D) (a b : α), rel (input, (encode v, d), a, b) = true ↔ R.rel (v, d) a b) (T q : ℕ) [NeZero q] (v : V) (k : Fin T → D) (c : Fin T → Fin q) (a b : WalkLabels D T → α) : powerRelationWithInput rotate rel T q (input, (encode v, k, c), a, b) = true ↔ (R.power T q).rel (v, k, c) a b

Valid encoded trajectories and original constraints give exactly the mathematical powered constraint, including the reverse opinion queried at each step.