GapCVP proof, part 01

def «tacticCompactMachineStepTac[_,,]» : Lean.ParserDescr

Executes the compactMachineStepTac machine-step simplifier.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.TraceGolf.oneStep {α : Type u_1} {step : α → Option α} (source target : α) (transition : step source = some target) : StateTransition.EvalsToInTime step source (some target) 1

GapCVP reduction support.

Equations

• GapCVP.TraceGolf.oneStep source target transition = { steps := 1, evals_in_steps := transition, steps_le_m := GapCVP.TraceGolf.oneStep._proof_1 }

def GapCVP.TraceGolf.sweepTrace {α : Type u_1} {β : Type u_2} (step : α → Option α) (configuration : List β → α) (transition : (symbol : β) → (remaining : List β) → StateTransition.EvalsToInTime step (configuration (symbol :: remaining)) (some (configuration remaining)) 1) (symbols : List β) : StateTransition.EvalsToInTime step (configuration symbols) (some (configuration [])) symbols.length

Repeatedly composes supplied one-step traces while consuming a list.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.TraceGolf.sweep {α : Type u_1} {β : Type u_2} (step : α → Option α) (configuration : List β → α) (transition : ∀ (symbol : β) (remaining : List β), step (configuration (symbol :: remaining)) = some (configuration remaining)) (symbols : List β) : StateTransition.EvalsToInTime step (configuration symbols) (some (configuration [])) symbols.length

Repeatedly applies a one-step transition while consuming a list.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.TraceGolf.sweepThen {α : Type u_1} {β : Type u_2} (step : α → Option α) (configuration : List β → α) (transition : ∀ (symbol : β) (remaining : List β), step (configuration (symbol :: remaining)) = some (configuration remaining)) (symbols : List β) {target : α} (finish : step (configuration []) = some target) : StateTransition.EvalsToInTime step (configuration symbols) (some target) (symbols.length + 1)

Consumes a list and then applies one final transition.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.TraceGolf.rebound {α : Type u_1} {step : α → Option α} {source : α} {target : Option α} {oldBudget newBudget : ℕ} (trace : StateTransition.EvalsToInTime step source target oldBudget) (budget : oldBudget ≤ newBudget) : StateTransition.EvalsToInTime step source target newBudget

GapCVP reduction support.

Equations

• GapCVP.TraceGolf.rebound trace budget = { toEvalsTo := trace.toEvalsTo, steps_le_m := ⋯ }

theorem GapCVP.Core.odd_integer_distance_gt_half (z : ℤ) : 1 / 2 < |1 - 2 * ↑z|

structure GapCVP.Core.GapCVPInstance : Type

GapCVP reduction support.

• dimension : ℕ

  GapCVP reduction support.

• dimension_pos : 0 < self.dimension
• basis : Matrix (Fin self.dimension) (Fin self.dimension) ℤ

  GapCVP reduction support.

• basis_nonsingular : self.basis.det ≠ 0
• target : Fin self.dimension → ℚ

  GapCVP reduction support.

• radius : ℚ

  GapCVP reduction support.

• radius_pos : 0 < self.radius

noncomputable def GapCVP.Core.GapCVPInstance.latticePoint (I : GapCVPInstance) (z : Fin I.dimension → ℤ) : EuclideanSpace ℝ (Fin I.dimension)

GapCVP reduction support.

Equations

• I.latticePoint z = WithLp.toLp 2 fun (i : Fin I.dimension) => ↑(∑ j : Fin I.dimension, I.basis i j * z j)

noncomputable def GapCVP.Core.GapCVPInstance.targetPoint (I : GapCVPInstance) : EuclideanSpace ℝ (Fin I.dimension)

GapCVP reduction support.

Equations

• I.targetPoint = WithLp.toLp 2 fun (i : Fin I.dimension) => ↑(I.target i)

noncomputable def GapCVP.Core.GapCVPInstance.latticeDistance (I : GapCVPInstance) : ℝ

GapCVP reduction support.

Equations

• I.latticeDistance = Metric.infDist I.targetPoint (Set.range I.latticePoint)

noncomputable def GapCVP.Core.GapCVPInstance.IsYes (I : GapCVPInstance) : Bool

GapCVP reduction support.

Equations

• I.IsYes = decide (I.latticeDistance ≤ ↑I.radius)

noncomputable def GapCVP.Core.GapCVPInstance.IsNo (c : ℝ) (I : GapCVPInstance) : Bool

GapCVP reduction support.

Equations

• GapCVP.Core.GapCVPInstance.IsNo c I = decide (↑I.dimension ^ c * ↑I.radius < I.latticeDistance)

def GapCVP.Core.squaredDistance (I : GapCVPInstance) (z : Fin I.dimension → ℤ) : ℝ

GapCVP reduction support.

Equations

• GapCVP.Core.squaredDistance I z = ∑ i : Fin I.dimension, (↑(I.target i) - ∑ j : Fin I.dimension, ↑(I.basis i j) * ↑(z j)) ^ 2

noncomputable def GapCVP.Core.SquaredYes (I : GapCVPInstance) : Bool

GapCVP reduction support.

Equations

• GapCVP.Core.SquaredYes I = decide (∃ (z : Fin I.dimension → ℤ), GapCVP.Core.squaredDistance I z ≤ ↑I.radius ^ 2)

noncomputable def GapCVP.Core.SquaredNoAt (c : ℝ) (I : GapCVPInstance) : Bool

GapCVP reduction support.

Equations

• GapCVP.Core.SquaredNoAt c I = decide (∀ (z : Fin I.dimension → ℤ), (↑I.dimension ^ c * ↑I.radius) ^ 2 < GapCVP.Core.squaredDistance I z)

theorem GapCVP.Core.squaredDistance_eq_dist_sq (I : GapCVPInstance) (z : Fin I.dimension → ℤ) : squaredDistance I z = dist I.targetPoint (I.latticePoint z) ^ 2

theorem GapCVP.Core.exists_latticePoint_eq_latticeDistance (I : GapCVPInstance) : ∃ (z : Fin I.dimension → ℤ), I.latticeDistance = dist I.targetPoint (I.latticePoint z)

theorem GapCVP.Core.yes_of_squaredYes (I : GapCVPInstance) : SquaredYes I = true → I.IsYes = true

theorem GapCVP.Core.no_of_squaredNoAt (c : ℝ) (I : GapCVPInstance) : SquaredNoAt c I = true → GapCVPInstance.IsNo c I = true

theorem GapCVP.Core.squaredNoAt_of_metricNo (c : ℝ) (I : GapCVPInstance) (hno : GapCVPInstance.IsNo c I = true) : SquaredNoAt c I = true

theorem GapCVP.Core.squaredNoAt_iff_metricNo (c : ℝ) (I : GapCVPInstance) : SquaredNoAt c I = true ↔ GapCVPInstance.IsNo c I = true

@[reducible, inline]

abbrev GapCVP.Core.canonicalNoInstance : GapCVPInstance

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GapCVP.Literal : Type

GapCVP reduction support.

Equations

• GapCVP.Literal = (ℕ × Bool)

@[reducible, inline]

abbrev GapCVP.ThreeClause : Type

GapCVP reduction support.

Equations

• GapCVP.ThreeClause = (Fin 3 → GapCVP.Literal)

@[reducible, inline]

abbrev GapCVP.ThreeCNF : Type

GapCVP reduction support.

Equations

• GapCVP.ThreeCNF = List GapCVP.ThreeClause

noncomputable def GapCVP.clauseHasDistinctVariables (c : ThreeClause) : Bool

GapCVP reduction support.

Equations

• GapCVP.clauseHasDistinctVariables c = decide (Function.Injective fun (i : Fin 3) => (c i).1)

noncomputable def GapCVP.literalSatisfied (assignment : ℕ → Bool) (l : Literal) : Bool

GapCVP reduction support.

Equations

• GapCVP.literalSatisfied assignment l = decide (assignment l.1 = l.2)

noncomputable def GapCVP.clauseSatisfied (assignment : ℕ → Bool) (c : ThreeClause) : Bool

GapCVP reduction support.

Equations

• GapCVP.clauseSatisfied assignment c = decide (∃ (i : Fin 3), GapCVP.literalSatisfied assignment (c i) = true)

noncomputable def GapCVP.threeCNFSatisfiable (φ : ThreeCNF) : Bool

GapCVP reduction support.

Equations

• GapCVP.threeCNFSatisfiable φ = decide ((∀ c ∈ φ, GapCVP.clauseHasDistinctVariables c = true) ∧ ∃ (assignment : ℕ → Bool), ∀ c ∈ φ, GapCVP.clauseSatisfied assignment c = true)

structure GapCVP.GapCVPInstance : Type

GapCVP reduction support.

• dimension : ℕ

  GapCVP reduction support.

• basis : Matrix (Fin self.dimension) (Fin self.dimension) ℤ

  GapCVP reduction support.

• target : Fin self.dimension → ℚ

  GapCVP reduction support.

• radius : ℚ

  GapCVP reduction support.

noncomputable def GapCVP.gapCVPWellFormed (I : GapCVPInstance) : Bool

GapCVP reduction support.

Equations

• GapCVP.gapCVPWellFormed I = decide (0 < I.dimension ∧ I.basis.det ≠ 0 ∧ 0 < I.radius)

noncomputable def GapCVP.distanceSquared (I : GapCVPInstance) (z : Fin I.dimension → ℤ) : ℝ

GapCVP reduction support.

Equations

• GapCVP.distanceSquared I z = ∑ i : Fin I.dimension, (∑ j : Fin I.dimension, ↑(I.basis i j) * ↑(z j) - ↑(I.target i)) ^ 2

class GapCVP.BinaryBitCodec (α : Type u_1) : Type u_1

GapCVP reduction support.

• encode : α → List Bool

  GapCVP reduction support.

• decode : List Bool → Option α

  GapCVP reduction support.

• decode_encode (a : α) : decode (encode a) = some a

def GapCVP.BinaryEncoding.lengthPrefixedWord (word : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryEncoding.lengthPrefixedWord word = List.replicate word.length true ++ false :: word

@[simp]

theorem GapCVP.BinaryEncoding.lengthPrefixedWord_length (word : List Bool) : (lengthPrefixedWord word).length = 2 * word.length + 1

def GapCVP.BinaryEncoding.readUnaryPrefix : List Bool → Option (ℕ × List Bool)

GapCVP reduction support.

Equations

• GapCVP.BinaryEncoding.readUnaryPrefix [] = none
• GapCVP.BinaryEncoding.readUnaryPrefix (false :: rest) = some (0, rest)
• GapCVP.BinaryEncoding.readUnaryPrefix (true :: rest) = match GapCVP.BinaryEncoding.readUnaryPrefix rest with | none => none | some (n, tail) => some (n + 1, tail)

@[simp]

theorem GapCVP.BinaryEncoding.readUnaryPrefix_replicate (n : ℕ) (tail : List Bool) : readUnaryPrefix (List.replicate n true ++ false :: tail) = some (n, tail)

def GapCVP.BinaryEncoding.readLengthPrefixedWord (bits : List Bool) : Option (List Bool × List Bool)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GapCVP.BinaryEncoding.readLengthPrefixedWord_append (word suffix : List Bool) : readLengthPrefixedWord (lengthPrefixedWord word ++ suffix) = some (word, suffix)

def GapCVP.BinaryEncoding.encodeLiteral (literal : Literal) : List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryEncoding.encodeLiteral literal = GapCVP.BinaryEncoding.lengthPrefixedWord (Computability.encodeNat literal.1) ++ [literal.2]

def GapCVP.BinaryEncoding.readLiteral (bits : List Bool) : Option (Literal × List Bool)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GapCVP.BinaryEncoding.readLiteral_append (literal : Literal) (suffix : List Bool) : readLiteral (encodeLiteral literal ++ suffix) = some (literal, suffix)

def GapCVP.BinaryEncoding.encodeThreeClause (clause : ThreeClause) : List Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.BinaryEncoding.encodeThreeCNF (clauses : ThreeCNF) : List Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.BinaryEncoding.decodeThreeCNF (bits : List Bool) : Option ThreeCNF

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GapCVP.BinaryEncoding.decodeThreeCNF_encode (clauses : ThreeCNF) : decodeThreeCNF (encodeThreeCNF clauses) = some clauses

@[instance_reducible, instance 2000]

noncomputable instance GapCVP.instBinaryBitCodecThreeCNF : BinaryBitCodec ThreeCNF

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.BinaryEncoding.encodeAtomic {α : Type u_1} [Encodable α] (a : α) : List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryEncoding.encodeAtomic a = GapCVP.BinaryEncoding.lengthPrefixedWord (Computability.encodeNat (Encodable.encode a))

def GapCVP.BinaryEncoding.readAtomic {α : Type u_1} [Encodable α] (bits : List Bool) : Option (α × List Bool)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GapCVP.BinaryEncoding.readAtomic_append {α : Type u_1} [Encodable α] (a : α) (suffix : List Bool) : readAtomic (encodeAtomic a ++ suffix) = some (a, suffix)

def GapCVP.BinaryEncoding.encodeFinValues {α : Type u_1} [Encodable α] (n : ℕ) : (Fin n → α) → List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryEncoding.encodeFinValues 0 x_2 = []
• GapCVP.BinaryEncoding.encodeFinValues n.succ values = GapCVP.BinaryEncoding.encodeAtomic (values 0) ++ GapCVP.BinaryEncoding.encodeFinValues n fun (i : Fin n) => values i.succ

def GapCVP.BinaryEncoding.readFinValues {α : Type u_1} [Encodable α] (n : ℕ) : List Bool → Option ((Fin n → α) × List Bool)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.BinaryEncoding.readFinValues 0 x✝ = some (Fin.elim0, x✝)

@[simp]

theorem GapCVP.BinaryEncoding.readFinValues_append {α : Type u_1} [Encodable α] {n : ℕ} (values : Fin n → α) (suffix : List Bool) : readFinValues n (encodeFinValues n values ++ suffix) = some (values, suffix)

def GapCVP.BinaryEncoding.encodeMatrixRows (m n : ℕ) : (Fin m → Fin n → ℤ) → List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryEncoding.encodeMatrixRows 0 x✝¹ x✝ = []
• GapCVP.BinaryEncoding.encodeMatrixRows m.succ x✝¹ x✝ = GapCVP.BinaryEncoding.encodeFinValues x✝¹ (x✝ 0) ++ GapCVP.BinaryEncoding.encodeMatrixRows m x✝¹ fun (i : Fin m) => x✝ i.succ

def GapCVP.BinaryEncoding.readMatrixRows (m n : ℕ) : List Bool → Option ((Fin m → Fin n → ℤ) × List Bool)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.BinaryEncoding.readMatrixRows 0 x✝¹ x✝ = some (Fin.elim0, x✝)

@[simp]

theorem GapCVP.BinaryEncoding.readMatrixRows_append {m n : ℕ} (matrix : Fin m → Fin n → ℤ) (suffix : List Bool) : readMatrixRows m n (encodeMatrixRows m n matrix ++ suffix) = some (matrix, suffix)

def GapCVP.BinaryEncoding.encodeGapCVPInstance (I : GapCVPInstance) : List Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible, instance 2000]

noncomputable instance GapCVP.instBinaryBitCodecGapCVPInstance : BinaryBitCodec GapCVPInstance

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.binaryFinEncoding (α : Type u_1) [BinaryBitCodec α] : Computability.Encoding α Bool

GapCVP reduction support.

Equations

• GapCVP.binaryFinEncoding α = { encode := GapCVP.BinaryBitCodec.encode, decode := GapCVP.BinaryBitCodec.decode, decode_encode := ⋯ }

@[reducible, inline]

abbrev GapCVP.BitLanguage : Type

GapCVP reduction support.

Equations

• GapCVP.BitLanguage = (List Bool → Bool)

@[reducible, inline]

abbrev GapCVP.bitEncoding : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.bitEncoding = id

def GapCVP.pairBitEncoding : List Bool × List Bool → List (Bool ⊕ Bool)

GapCVP reduction support.

Equations

• GapCVP.pairBitEncoding = (Computability.encodingProd (Computability.encodingList Bool) (Computability.encodingList Bool)).encode

@[reducible, inline]

abbrev GapCVP.BitTM (f : List Bool → List Bool) : Type 1

GapCVP reduction support.

Equations

• GapCVP.BitTM f = Turing.TM2ComputableInPolyTime GapCVP.bitEncoding GapCVP.bitEncoding f

@[reducible, inline]

abbrev GapCVP.VerifierTM (verifier : List Bool × List Bool → Bool) : Type 1

GapCVP reduction support.

Equations

• GapCVP.VerifierTM verifier = Turing.TM2ComputableInPolyTime GapCVP.pairBitEncoding Computability.encodeBool verifier

noncomputable def GapCVP.IsNP (L : BitLanguage) : Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

structure GapCVP.PolynomialReduction (A B : BitLanguage) : Type

GapCVP reduction support.

• map : List Bool → List Bool

  GapCVP reduction support.

• polynomial_time : Nonempty (BitTM self.map)
• correct (x : List Bool) : A x = true ↔ B (self.map x) = true

noncomputable def GapCVP.PolynomialTimeClosedUnderComposition : Bool

Polynomial-time binary-string functions remain polynomial-time under composition.

Equations

• GapCVP.PolynomialTimeClosedUnderComposition = decide (∀ (f g : List Bool → List Bool), Nonempty (GapCVP.BitTM f) → Nonempty (GapCVP.BitTM g) → Nonempty (GapCVP.BitTM (g ∘ f)))

noncomputable def GapCVP.NPHard (L : BitLanguage) : Bool

GapCVP reduction support.

Equations

• GapCVP.NPHard L = decide (∀ (A : GapCVP.BitLanguage), GapCVP.IsNP A = true → Nonempty (GapCVP.PolynomialReduction A L))

noncomputable def GapCVP.threeSATLanguage : BitLanguage

GapCVP reduction support.

Equations

• GapCVP.threeSATLanguage bits = decide (∃ (φ : GapCVP.ThreeCNF), (GapCVP.binaryFinEncoding GapCVP.ThreeCNF).encode φ = bits ∧ GapCVP.threeCNFSatisfiable φ = true)

structure GapCVP.PromiseProblem : Type

GapCVP reduction support.

• yes : BitLanguage

  GapCVP reduction support.

• no : BitLanguage

  GapCVP reduction support.

• disjoint (x : List Bool) : self.yes x = true → self.no x = true → False

structure GapCVP.PromiseReduction (A : BitLanguage) (P : PromiseProblem) : Type

GapCVP reduction support.

• map : List Bool → List Bool

  GapCVP reduction support.

• polynomial_time : Nonempty (BitTM self.map)
• completeness (x : List Bool) : A x = true → P.yes (self.map x) = true
• soundness (x : List Bool) : ¬A x = true → P.no (self.map x) = true

noncomputable def GapCVP.NPHardPromise (P : PromiseProblem) : Bool

GapCVP reduction support.

Equations

• GapCVP.NPHardPromise P = decide (∀ (A : GapCVP.BitLanguage), GapCVP.IsNP A = true → Nonempty (GapCVP.PromiseReduction A P))

noncomputable def GapCVP.gapYES (I : GapCVPInstance) : Bool

GapCVP reduction support.

Equations

• GapCVP.gapYES I = decide (GapCVP.gapCVPWellFormed I = true ∧ ∃ (z : Fin I.dimension → ℤ), GapCVP.distanceSquared I z ≤ ↑I.radius ^ 2)

@[reducible, inline]

abbrev GapCVP.TMComposition.alphabet (first second : Turing.FinTM2) : GapCVP.TMComposition.Stack✝ first second → Type

GapCVP reduction support.

Equations

• GapCVP.TMComposition.alphabet first second (Sum.inl k) = first.Γ k
• GapCVP.TMComposition.alphabet first second (Sum.inr k) = second.Γ ↑k

noncomputable def GapCVP.TMComposition.maxPushPerStep (tm : Turing.FinTM2) : ℕ

GapCVP reduction support.

Equations

• GapCVP.TMComposition.maxPushPerStep tm = Finset.univ.sup fun (label : tm.Λ) => GapCVP.TMComposition.statementPushCount✝ (tm.m label)

def GapCVP.TMComposition.evalsToInTimeMapOfStep {α β : Type} (stepA : α → Option α) (stepB : β → Option β) (translate : α → β) (hstep : ∀ (a a' : α), stepA a = some a' → stepB (translate a) = some (translate a')) {a a' : α} {budget : ℕ} (h : StateTransition.EvalsToInTime stepA a (some a') budget) : StateTransition.EvalsToInTime stepB (translate a) (some (translate a')) budget

GapCVP reduction support.

Equations

• GapCVP.TMComposition.evalsToInTimeMapOfStep stepA stepB translate hstep h = { steps := h.steps, evals_in_steps := ⋯, steps_le_m := ⋯ }

theorem GapCVP.TMComposition.natPolynomial_eval_monotone (p : Polynomial ℕ) : Monotone fun (x : ℕ) => Polynomial.eval x p

noncomputable def GapCVP.TMComposition.outputLengthPolynomial {f : List Bool → List Bool} (first : BitTM f) : Polynomial ℕ

GapCVP reduction support.

Equations

• GapCVP.TMComposition.outputLengthPolynomial first = Polynomial.X + Polynomial.C (GapCVP.TMComposition.maxPushPerStep first.tm) * first.time

theorem GapCVP.TMComposition.outputLengthPolynomial_bounds {f : List Bool → List Bool} (first : BitTM f) (x : List Bool) : (f x).length ≤ Polynomial.eval x.length (outputLengthPolynomial first)

noncomputable def GapCVP.TMComposition.machine {f g : List Bool → List Bool} (first : BitTM f) (second : BitTM g) : Turing.FinTM2

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.TMComposition.auxiliary {f g : List Bool → List Bool} (first : BitTM f) (second : BitTM g) : Turing.TM2ComputableAux Bool Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GapCVP.TMComposition.haltList_stk_self (tm : Turing.FinTM2) (xs : List (tm.Γ tm.k₁)) : (Turing.haltList tm xs).stk tm.k₁ = xs

noncomputable def GapCVP.TMComposition.computableInPolyTime {f g : List Bool → List Bool} (first : BitTM f) (second : BitTM g) : BitTM (g ∘ f)

GapCVP reduction support.

Equations

• GapCVP.TMComposition.computableInPolyTime first second = GapCVP.TMComposition.computableInPolyTimeOfSeam✝ first second

theorem GapCVP.polynomialTimeClosedUnderComposition : PolynomialTimeClosedUnderComposition = true

def GapCVP.PromiseReduction.comp {A B : BitLanguage} {P : PromiseProblem} (first : PolynomialReduction A B) (second : PromiseReduction B P) (closed : PolynomialTimeClosedUnderComposition = true) : PromiseReduction A P

GapCVP reduction support.

Equations

• GapCVP.PromiseReduction.comp first second closed = GapCVP.PromiseReduction.compWithCertificate✝ first second ⋯

theorem GapCVP.nphardPromise_of_nphard_of_promiseReduction {A : BitLanguage} {P : PromiseProblem} (hard : NPHard A = true) (reduction : PromiseReduction A P) (closed : PolynomialTimeClosedUnderComposition = true) : NPHardPromise P = true

@[reducible, inline]

abbrev GapCVP.CL.Time (T : ℕ) : Type

GapCVP reduction support.

Equations

• GapCVP.CL.Time T = Fin (T + 1)

@[reducible, inline]

abbrev GapCVP.CL.Position (T : ℕ) : Type

GapCVP reduction support.

Equations

• GapCVP.CL.Position T = Fin (T + 1)

@[reducible, inline]

abbrev GapCVP.CL.Symbol (S : ℕ) : Type

GapCVP reduction support.

Equations

• GapCVP.CL.Symbol S = Fin (S + 1)

@[reducible, inline]

abbrev GapCVP.CL.Variable (T S : ℕ) : Type

GapCVP reduction support.

Equations

• GapCVP.CL.Variable T S = (GapCVP.CL.Time T × GapCVP.CL.Position T × GapCVP.CL.Symbol S)

@[reducible, inline]

abbrev GapCVP.CL.SignedLiteral (T S : ℕ) : Type

GapCVP reduction support.

Equations

• GapCVP.CL.SignedLiteral T S = (GapCVP.CL.Variable T S × Bool)

@[reducible, inline]

abbrev GapCVP.CL.Clause (T S : ℕ) : Type

GapCVP reduction support.

Equations

• GapCVP.CL.Clause T S = Finset (GapCVP.CL.SignedLiteral T S)

@[reducible, inline]

abbrev GapCVP.CL.Formula (T S : ℕ) : Type

GapCVP reduction support.

Equations

• GapCVP.CL.Formula T S = Finset (GapCVP.CL.Clause T S)

def GapCVP.CL.positive {T S : ℕ} (v : Variable T S) : SignedLiteral T S

GapCVP reduction support.

Equations

• GapCVP.CL.positive v = (v, true)

def GapCVP.CL.negative {T S : ℕ} (v : Variable T S) : SignedLiteral T S

GapCVP reduction support.

Equations

• GapCVP.CL.negative v = (v, false)

def GapCVP.CL.atLeastOneClause {T S : ℕ} (t : Time T) (i : Position T) : Clause T S

GapCVP reduction support.

Equations

• GapCVP.CL.atLeastOneClause t i = Finset.image (fun (s : GapCVP.CL.Symbol S) => GapCVP.CL.positive (t, i, s)) Finset.univ

def GapCVP.CL.atMostOneClause {T S : ℕ} (t : Time T) (i : Position T) (a b : Symbol S) : Clause T S

GapCVP reduction support.

Equations

• GapCVP.CL.atMostOneClause t i a b = {GapCVP.CL.negative (t, i, a), GapCVP.CL.negative (t, i, b)}

def GapCVP.CL.initialClause {T S : ℕ} (input : Position T → Symbol S) (i : Position T) : Clause T S

GapCVP reduction support.

Equations

• GapCVP.CL.initialClause input i = {GapCVP.CL.positive (0, i, input i)}

def GapCVP.CL.acceptanceClause {T S : ℕ} (accept : Symbol S) : Clause T S

GapCVP reduction support.

Equations

• GapCVP.CL.acceptanceClause accept = Finset.image (fun (i : GapCVP.CL.Position T) => GapCVP.CL.positive (Fin.last T, i, accept)) Finset.univ

@[reducible, inline]

abbrev GapCVP.CL.Window (T : ℕ) : Type

GapCVP reduction support.

Equations

• GapCVP.CL.Window T = { ti : GapCVP.CL.Time T × GapCVP.CL.Position T // ↑ti.1 + 1 < T + 1 }

def GapCVP.CL.nextTime {T : ℕ} (w : Window T) : Time T

GapCVP reduction support.

Equations

• GapCVP.CL.nextTime w = ⟨↑(↑w).1 + 1, ⋯⟩

def GapCVP.CL.leftPosition {T : ℕ} (w : Window T) : Position T

GapCVP reduction support.

Equations

• GapCVP.CL.leftPosition w = ⟨↑(↑w).2 - 1, ⋯⟩

def GapCVP.CL.rightPosition {T : ℕ} (w : Window T) : Position T

GapCVP reduction support.

Equations

• GapCVP.CL.rightPosition w = ⟨min (↑(↑w).2 + 1) T, ⋯⟩

def GapCVP.CL.windowAt {T : ℕ} (t : Fin T) (i : Position T) : Window T

GapCVP reduction support.

Equations

• GapCVP.CL.windowAt t i = ⟨(⟨↑t, ⋯⟩, i), ⋯⟩

@[reducible, inline]

abbrev GapCVP.CL.WindowSymbols (S : ℕ) : Type

GapCVP reduction support.

Equations

• GapCVP.CL.WindowSymbols S = (GapCVP.CL.Symbol S × GapCVP.CL.Symbol S × GapCVP.CL.Symbol S × GapCVP.CL.Symbol S)

def GapCVP.CL.transitionClause {T S : ℕ} (w : Window T) (symbols : WindowSymbols S) : Clause T S

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

structure GapCVP.CL.Specification (T S : ℕ) : Type

GapCVP reduction support.

• input : Position T → Symbol S

  GapCVP reduction support.

• accept : Symbol S

  GapCVP reduction support.

• allowed : WindowSymbols S → Bool

  GapCVP reduction support.

def GapCVP.CL.structuralClauses (T S : ℕ) : Formula T S

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.CL.initialClauses {T S : ℕ} (spec : Specification T S) : Formula T S

GapCVP reduction support.

Equations

• GapCVP.CL.initialClauses spec = Finset.image (fun (i : GapCVP.CL.Position T) => GapCVP.CL.initialClause spec.input i) Finset.univ

def GapCVP.CL.transitionClauses {T S : ℕ} (spec : Specification T S) : Formula T S

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.CL.tableauFormula {T S : ℕ} (spec : Specification T S) : Formula T S

GapCVP reduction support.

Equations

• GapCVP.CL.tableauFormula spec = GapCVP.CL.structuralClauses T S ∪ GapCVP.CL.initialClauses spec ∪ {GapCVP.CL.acceptanceClause spec.accept} ∪ GapCVP.CL.transitionClauses spec

noncomputable def GapCVP.CL.ValidTrace {T S : ℕ} (spec : Specification T S) (trace : Time T → Position T → Symbol S) : Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CL.atLeastOneClause_mem_tableauFormula {T S : ℕ} (spec : Specification T S) (t : Time T) (i : Position T) : atLeastOneClause t i ∈ tableauFormula spec

theorem GapCVP.CL.atMostOneClause_mem_tableauFormula {T S : ℕ} (spec : Specification T S) (t : Time T) (i : Position T) (a b : Symbol S) (hab : a < b) : atMostOneClause t i a b ∈ tableauFormula spec

theorem GapCVP.CL.initialClause_mem_tableauFormula {T S : ℕ} (spec : Specification T S) (i : Position T) : initialClause spec.input i ∈ tableauFormula spec

theorem GapCVP.CL.acceptanceClause_mem_tableauFormula {T S : ℕ} (spec : Specification T S) : acceptanceClause spec.accept ∈ tableauFormula spec

theorem GapCVP.CL.transitionClause_mem_tableauFormula {T S : ℕ} (spec : Specification T S) (w : Window T) (symbols : WindowSymbols S) (hforbidden : spec.allowed symbols = false) : transitionClause w symbols ∈ tableauFormula spec

def GapCVP.ThreeCNFReduction.sortedElements {α : Type} [Encodable α] (s : Finset α) : List α

GapCVP reduction support.

Equations

• GapCVP.ThreeCNFReduction.sortedElements s = s.sort fun (a b : α) => Encodable.encode a ≤ Encodable.encode b

@[simp]

theorem GapCVP.ThreeCNFReduction.mem_sortedElements {α : Type} [Encodable α] (s : Finset α) (a : α) : a ∈ sortedElements s ↔ a ∈ s

@[simp]

theorem GapCVP.ThreeCNFReduction.sortedElements_length {α : Type} [Encodable α] (s : Finset α) : (sortedElements s).length = s.card

noncomputable def GapCVP.ThreeCNFReduction.allDistinct (formula : ThreeCNF) : Bool

GapCVP reduction support.

Equations

• GapCVP.ThreeCNFReduction.allDistinct formula = decide (∀ clause ∈ formula, GapCVP.clauseHasDistinctVariables clause = true)

def GapCVP.ThreeCNFReduction.sourceVariable {T S : ℕ} (v : CL.Variable T S) : ℕ

GapCVP reduction support.

Equations

• GapCVP.ThreeCNFReduction.sourceVariable v = 4 * Encodable.encode v

def GapCVP.ThreeCNFReduction.accumulatorVariable (clauseIndex prefixIndex : ℕ) : ℕ

GapCVP reduction support.

Equations

• GapCVP.ThreeCNFReduction.accumulatorVariable clauseIndex prefixIndex = 4 * Encodable.encode (clauseIndex, prefixIndex) + 1

def GapCVP.ThreeCNFReduction.triple (a b c : Literal) : ThreeClause

GapCVP reduction support.

Equations

• GapCVP.ThreeCNFReduction.triple a b c = ![a, b, c]

def GapCVP.ThreeCNFReduction.paddedBinary (a b : Literal) : ThreeCNF

GapCVP reduction support.

Equations

• GapCVP.ThreeCNFReduction.paddedBinary a b = [GapCVP.ThreeCNFReduction.triple a b (2, true), GapCVP.ThreeCNFReduction.triple a b (2, false)]

def GapCVP.ThreeCNFReduction.paddedUnary (a : Literal) : ThreeCNF

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.ThreeCNFReduction.negate (a : Literal) : Literal

GapCVP reduction support.

Equations

• GapCVP.ThreeCNFReduction.negate a = (a.1, !a.2)

def GapCVP.ThreeCNFReduction.orGate (a b output : Literal) : ThreeCNF

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GapCVP.ThreeCNFReduction.paddedUnary_length (a : Literal) : List.length (paddedUnary a) = 4

@[simp]

theorem GapCVP.ThreeCNFReduction.orGate_length (a b output : Literal) : List.length (orGate a b output) = 5

def GapCVP.ThreeCNFReduction.sourceLiteral {T S : ℕ} (literal : CL.SignedLiteral T S) : Literal

GapCVP reduction support.

Equations

• GapCVP.ThreeCNFReduction.sourceLiteral literal = (GapCVP.ThreeCNFReduction.sourceVariable literal.1, literal.2)

def GapCVP.ThreeCNFReduction.accumulatorLiteral (clauseIndex prefixIndex : ℕ) (value : Bool) : Literal

GapCVP reduction support.

Equations

• GapCVP.ThreeCNFReduction.accumulatorLiteral clauseIndex prefixIndex value = (GapCVP.ThreeCNFReduction.accumulatorVariable clauseIndex prefixIndex, value)

def GapCVP.ThreeCNFReduction.gateList {T S : ℕ} (clauseIndex : ℕ) : ℕ → List (CL.SignedLiteral T S) → ThreeCNF

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.ThreeCNFReduction.gateList clauseIndex x✝ [] = []

def GapCVP.ThreeCNFReduction.encodeClause {T S : ℕ} (clauseIndex : ℕ) (clause : CL.Clause T S) : ThreeCNF

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.ThreeCNFReduction.encodeFormulaFrom {T S : ℕ} : ℕ → List (CL.Clause T S) → ThreeCNF

GapCVP reduction support.

Equations

• GapCVP.ThreeCNFReduction.encodeFormulaFrom x✝ [] = []
• GapCVP.ThreeCNFReduction.encodeFormulaFrom x✝ (clause :: remaining) = GapCVP.ThreeCNFReduction.encodeClause x✝ clause ++ GapCVP.ThreeCNFReduction.encodeFormulaFrom (x✝ + 1) remaining

theorem GapCVP.ThreeCNFReduction.encodeFormula_allDistinct {T S : ℕ} (formula : CL.Formula T S) : allDistinct (GapCVP.ThreeCNFReduction.encodeFormula✝ formula) = true

theorem GapCVP.ThreeCNFReduction.signedLiteral_card (T S : ℕ) : Fintype.card (CL.SignedLiteral T S) = 2 * ((T + 1) ^ 2 * (S + 1))

def GapCVP.ThreeCNFReduction.restrictAssignment {T S : ℕ} (assignment : ℕ → Bool) : CL.Variable T S → Bool

GapCVP reduction support.

Equations

• GapCVP.ThreeCNFReduction.restrictAssignment assignment v = assignment (GapCVP.ThreeCNFReduction.sourceVariable v)

def GapCVP.ThreeCNFReduction.encodeTableau {T S : ℕ} (spec : CL.Specification T S) : ThreeCNF

GapCVP reduction support.

Equations

• GapCVP.ThreeCNFReduction.encodeTableau spec = GapCVP.ThreeCNFReduction.encodeFormula✝ (GapCVP.CL.tableauFormula spec)

@[simp]

theorem GapCVP.CLVerifier.pairBitEncoding_apply (x certificate : List Bool) : pairBitEncoding (x, certificate) = List.map Sum.inl x ++ List.map Sum.inr certificate

theorem GapCVP.CLVerifier.pairBitEncoding_length (x certificate : List Bool) : (pairBitEncoding (x, certificate)).length = x.length + certificate.length

theorem GapCVP.CLVerifier.encodeNat_length_eq_size (n : ℕ) : (Computability.encodeNat n).length = n.size

def GapCVP.CLVerifier.verifierInput {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x certificate : List Bool) : List (machine.tm.Γ machine.tm.k₀)

GapCVP reduction support.

Equations

• GapCVP.CLVerifier.verifierInput machine x certificate = List.map machine.inputAlphabet.invFun (GapCVP.pairBitEncoding (x, certificate))

def GapCVP.CLVerifier.verifierOutput {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (value : Bool) : List (machine.tm.Γ machine.tm.k₁)

GapCVP reduction support.

Equations

• GapCVP.CLVerifier.verifierOutput machine value = List.map machine.outputAlphabet.invFun (Computability.encodeBool value)

@[simp]

theorem GapCVP.CLVerifier.verifierInput_length {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x certificate : List Bool) : (verifierInput machine x certificate).length = x.length + certificate.length

@[simp]

theorem GapCVP.CLVerifier.verifierOutput_length {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (value : Bool) : (verifierOutput machine value).length = 1

theorem GapCVP.CLVerifier.verifierOutput_injective {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : Function.Injective (verifierOutput machine)

noncomputable def GapCVP.CLVerifier.witnessTimePolynomial (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : Polynomial ℕ

GapCVP reduction support.

Equations

• GapCVP.CLVerifier.witnessTimePolynomial bound machine = machine.time.comp (Polynomial.X + bound)

def GapCVP.CLVerifier.boundedVerifierRun (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x certificate : List Bool) (hcertificate : certificate.length ≤ Polynomial.eval x.length bound) : Turing.TM2OutputsInTime machine.tm (verifierInput machine x certificate) (some (verifierOutput machine (verifier (x, certificate)))) (Polynomial.eval x.length (witnessTimePolynomial bound machine))

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

structure GapCVP.CLVerifier.ConfigurationTrace (tm : Turing.FinTM2) (input : List (tm.Γ tm.k₀)) (output : List (tm.Γ tm.k₁)) (steps : ℕ) : Type

GapCVP reduction support.

• configuration : Fin (steps + 1) → tm.Cfg

  GapCVP reduction support.

• initial : self.configuration 0 = Turing.initList tm input
• final : self.configuration (Fin.last steps) = Turing.haltList tm output
• transition (i : Fin steps) : tm.step (self.configuration i.castSucc) = some (self.configuration i.succ)

theorem GapCVP.CLVerifier.ConfigurationTrace.iterate_configuration {tm : Turing.FinTM2} {input : List (tm.Γ tm.k₀)} {output : List (tm.Γ tm.k₁)} {steps : ℕ} (trace : ConfigurationTrace tm input output steps) (i : Fin (steps + 1)) : (flip bind tm.step)^[↑i] (some (Turing.initList tm input)) = some (trace.configuration i)

def GapCVP.CLVerifier.ConfigurationTrace.evalsToAt {tm : Turing.FinTM2} {input : List (tm.Γ tm.k₀)} {output : List (tm.Γ tm.k₁)} {steps : ℕ} (trace : ConfigurationTrace tm input output steps) (i : Fin (steps + 1)) : StateTransition.EvalsTo tm.step (Turing.initList tm input) (some (trace.configuration i))

GapCVP reduction support.

Equations

• trace.evalsToAt i = { steps := ↑i, evals_in_steps := ⋯ }

def GapCVP.CLVerifier.ConfigurationTrace.evalsTo {tm : Turing.FinTM2} {input : List (tm.Γ tm.k₀)} {output : List (tm.Γ tm.k₁)} {steps : ℕ} (trace : ConfigurationTrace tm input output steps) : StateTransition.EvalsTo tm.step (Turing.initList tm input) (some (Turing.haltList tm output))

GapCVP reduction support.

Equations

• trace.evalsTo = { steps := steps, evals_in_steps := ⋯ }

theorem GapCVP.CLVerifier.ConfigurationTrace.stack_length_le {tm : Turing.FinTM2} {input : List (tm.Γ tm.k₀)} {output : List (tm.Γ tm.k₁)} {steps : ℕ} (trace : ConfigurationTrace tm input output steps) (i : Fin (steps + 1)) (stack : tm.K) : ((trace.configuration i).stk stack).length ≤ input.length + ↑i * TMComposition.maxPushPerStep tm

theorem GapCVP.CLVerifier.haltList_step (tm : Turing.FinTM2) (output : List (tm.Γ tm.k₁)) : tm.step (Turing.haltList tm output) = none

theorem GapCVP.CLVerifier.evalsTo_terminal_unique_of_steps_le {α : Type} (step : α → Option α) (initial a b : α) (ha : StateTransition.EvalsTo step initial (some a)) (hb : StateTransition.EvalsTo step initial (some b)) (hterminal : step a = none) (hle : ha.steps ≤ hb.steps) : a = b

structure GapCVP.CLVerifier.AcceptedExecution (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : Type

GapCVP reduction support.

• certificate : List Bool

  GapCVP reduction support.

• certificate_le : self.certificate.length ≤ Polynomial.eval x.length bound
• steps : ℕ

  GapCVP reduction support.

• steps_le : self.steps ≤ Polynomial.eval x.length (witnessTimePolynomial bound machine)
• trace : ConfigurationTrace machine.tm (verifierInput machine x self.certificate) (verifierOutput machine true) self.steps

  GapCVP reduction support.

structure GapCVP.CLVerifier.TableauSimulation (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : Type

GapCVP reduction support.

• time : Polynomial ℕ

  GapCVP reduction support.

• symbols : ℕ

  GapCVP reduction support.

• specification (x : List Bool) : CL.Specification (Polynomial.eval x.length self.time) self.symbols

  GapCVP reduction support.

• correct (x : List Bool) : (∃ (trace : CL.Time (Polynomial.eval x.length self.time) → CL.Position (Polynomial.eval x.length self.time) → CL.Symbol self.symbols), CL.ValidTrace (self.specification x) trace = true) ↔ Nonempty (AcceptedExecution bound machine x)

noncomputable def GapCVP.CLVerifier.encodedTableau {bound : Polynomial ℕ} {verifier : List Bool × List Bool → Bool} {machine : VerifierTM verifier} (simulation : TableauSimulation bound machine) (x : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CLVerifier.encodedTableau simulation x = (GapCVP.binaryFinEncoding GapCVP.ThreeCNF).encode (GapCVP.ThreeCNFReduction.encodeTableau (simulation.specification x))

theorem GapCVP.CLVerifier.threeSATLanguage_encode_iff (formula : ThreeCNF) : threeSATLanguage ((binaryFinEncoding ThreeCNF).encode formula) = true ↔ threeCNFSatisfiable formula = true

inductive GapCVP.CLNondeterminism.FiniteRun {α : Type} (transition : α → α → Type) : α → α → ℕ → Type

GapCVP reduction support.

• refl {α : Type} {transition : α → α → Type} (state : α) : FiniteRun transition state state 0
• tail {α : Type} {transition : α → α → Type} {first middle last : α} {steps : ℕ} : FiniteRun transition first middle steps → transition middle last → FiniteRun transition first last (steps + 1)

noncomputable def GapCVP.CLNondeterminism.FiniteRun.single {α : Type} {transition : α → α → Type} {first last : α} (h : transition first last) : FiniteRun transition first last 1

GapCVP reduction support.

Equations

• GapCVP.CLNondeterminism.FiniteRun.single h = (GapCVP.CLNondeterminism.FiniteRun.refl first).tail h

noncomputable def GapCVP.CLNondeterminism.FiniteRun.trans {α : Type} {transition : α → α → Type} {first middle last : α} {leftSteps rightSteps : ℕ} (left : FiniteRun transition first middle leftSteps) (right : FiniteRun transition middle last rightSteps) : FiniteRun transition first last (leftSteps + rightSteps)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

inductive GapCVP.CLNondeterminism.GuessState (tm : Turing.FinTM2) : Type

GapCVP reduction support.

• guessing {tm : Turing.FinTM2} (certificate : List Bool) : GuessState tm
• verifying {tm : Turing.FinTM2} (certificate : List Bool) (configuration : tm.Cfg) : GuessState tm

inductive GapCVP.CLNondeterminism.GuessStep (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : GuessState machine.tm → GuessState machine.tm → Type

GapCVP reduction support.

• guess {bound : Polynomial ℕ} {verifier : List Bool × List Bool → Bool} {machine : VerifierTM verifier} {x : List Bool} (certificate : List Bool) (bit : Bool) (hbound : certificate.length < Polynomial.eval x.length bound) : GuessStep bound machine x (GuessState.guessing certificate) (GuessState.guessing (certificate ++ [bit]))
• begin {bound : Polynomial ℕ} {verifier : List Bool × List Bool → Bool} {machine : VerifierTM verifier} {x : List Bool} (certificate : List Bool) (hbound : certificate.length ≤ Polynomial.eval x.length bound) : GuessStep bound machine x (GuessState.guessing certificate) (GuessState.verifying certificate (Turing.initList machine.tm (CLVerifier.verifierInput machine x certificate)))
• execute {bound : Polynomial ℕ} {verifier : List Bool × List Bool → Bool} {machine : VerifierTM verifier} {x : List Bool} (certificate : List Bool) (configuration next : machine.tm.Cfg) (hstep : machine.tm.step configuration = some next) : GuessStep bound machine x (GuessState.verifying certificate configuration) (GuessState.verifying certificate next)

def GapCVP.CLNondeterminism.oneStepEvalsTo (tm : Turing.FinTM2) (configuration next : tm.Cfg) (hstep : tm.step configuration = some next) : StateTransition.EvalsTo tm.step configuration (some next)

GapCVP reduction support.

Equations

• GapCVP.CLNondeterminism.oneStepEvalsTo tm configuration next hstep = { steps := 1, evals_in_steps := ⋯ }

noncomputable def GapCVP.CLNondeterminism.guessTimePolynomial (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : Polynomial ℕ

GapCVP reduction support.

Equations

• GapCVP.CLNondeterminism.guessTimePolynomial bound machine = bound + 1 + GapCVP.CLVerifier.witnessTimePolynomial bound machine

noncomputable def GapCVP.CLNondeterminism.nondeterministicTableauDimensionPolynomial (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : Polynomial ℕ

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CLNondeterminism.verifying_stack_length_le (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x certificate : List Bool) (configuration : machine.tm.Cfg) {elapsed : ℕ} (run : FiniteRun (GuessStep bound machine x) (GuessState.guessing []) (GuessState.verifying certificate configuration) elapsed) (hruntime : elapsed ≤ Polynomial.eval x.length (guessTimePolynomial bound machine)) (stack : machine.tm.K) : (configuration.stk stack).length ≤ Polynomial.eval x.length (nondeterministicTableauDimensionPolynomial bound machine)

structure GapCVP.CLNondeterminism.GuessingExecution (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : Type

GapCVP reduction support.

• certificate : List Bool

  GapCVP reduction support.

• steps : ℕ

  GapCVP reduction support.

• steps_le : self.steps ≤ Polynomial.eval x.length (guessTimePolynomial bound machine)
• run : FiniteRun (GuessStep bound machine x) (GuessState.guessing []) (GuessState.verifying self.certificate (Turing.haltList machine.tm (CLVerifier.verifierOutput machine true))) self.steps

  GapCVP reduction support.

theorem GapCVP.CLNondeterminism.guessingExecution_accepted (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) {x : List Bool} (execution : GuessingExecution bound machine x) : Nonempty (CLVerifier.AcceptedExecution bound machine x)

structure GapCVP.CLNondeterminism.LocalTableauCompiler (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : Type

GapCVP reduction support.

• symbols : ℕ

  GapCVP reduction support.

• specification (x : List Bool) : CL.Specification (Polynomial.eval x.length (nondeterministicTableauDimensionPolynomial bound machine)) self.symbols

  GapCVP reduction support.

• encode (x : List Bool) : ∀ (a : GuessingExecution bound machine x), ∃ (trace : CL.Time (Polynomial.eval x.length (nondeterministicTableauDimensionPolynomial bound machine)) → CL.Position (Polynomial.eval x.length (nondeterministicTableauDimensionPolynomial bound machine)) → CL.Symbol self.symbols), CL.ValidTrace (self.specification x) trace = true
• decode (x : List Bool) (trace : CL.Time (Polynomial.eval x.length (nondeterministicTableauDimensionPolynomial bound machine)) → CL.Position (Polynomial.eval x.length (nondeterministicTableauDimensionPolynomial bound machine)) → CL.Symbol self.symbols) : CL.ValidTrace (self.specification x) trace = true → GuessingExecution bound machine x

  GapCVP reduction support.

noncomputable def GapCVP.CLNondeterminism.tableauSimulationOfLocalCompiler (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (compiler : LocalTableauCompiler bound machine) : CLVerifier.TableauSimulation bound machine

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CLNondeterminism.compiledTableau_iff_verifier (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (compiler : LocalTableauCompiler bound machine) (x : List Bool) : threeSATLanguage (CLVerifier.encodedTableau (tableauSimulationOfLocalCompiler bound machine compiler) x) = true ↔ ∃ (certificate : List Bool), certificate.length ≤ Polynomial.eval x.length bound ∧ verifier (x, certificate) = true

@[instance_reducible]

noncomputable instance GapCVP.CLBoundedStates.instFintypePushSlot (tm : Turing.FinTM2) : Fintype (GapCVP.CLBoundedStates.PushSlot✝ tm)

Equations

• GapCVP.CLBoundedStates.instFintypePushSlot tm = inferInstance

@[reducible, inline]

abbrev GapCVP.CLBoundedStates.PushTag (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• GapCVP.CLBoundedStates.PushTag tm = (GapCVP.CLBoundedStates.PushSlot✝ tm × tm.σ)

@[instance_reducible]

noncomputable instance GapCVP.CLBoundedStates.instFintypePushTag (tm : Turing.FinTM2) : Fintype (PushTag tm)

Equations

• GapCVP.CLBoundedStates.instFintypePushTag tm = inferInstance

@[reducible, inline]

abbrev GapCVP.CLBoundedStates.CellAtom (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• GapCVP.CLBoundedStates.CellAtom tm = Option ((Bool ⊕ Bool) ⊕ GapCVP.CLBoundedStates.PushTag tm)

@[instance_reducible]

noncomputable instance GapCVP.CLBoundedStates.instFintypeCellAtom (tm : Turing.FinTM2) : Fintype (CellAtom tm)

Equations

• GapCVP.CLBoundedStates.instFintypeCellAtom tm = inferInstance

inductive GapCVP.CLBoundedStates.PhaseTag : Type

GapCVP reduction support.

• guessing : PhaseTag
• verifying : PhaseTag
• accepting : PhaseTag

@[instance_reducible]

instance GapCVP.CLBoundedStates.instDecidableEqPhaseTag : DecidableEq PhaseTag

Equations

• GapCVP.CLBoundedStates.instDecidableEqPhaseTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

noncomputable instance GapCVP.CLBoundedStates.instFintypePhaseTag : Fintype PhaseTag

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GapCVP.CLBoundedStates.LocalCellSymbol (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• GapCVP.CLBoundedStates.LocalCellSymbol tm = (GapCVP.CLBoundedStates.PhaseTag × Option (tm.Λ × tm.σ) × (tm.K → GapCVP.CLBoundedStates.CellAtom tm) × Bool)

@[instance_reducible]

noncomputable instance GapCVP.CLBoundedStates.instFintypeLocalCellSymbol (tm : Turing.FinTM2) : Fintype (LocalCellSymbol tm)

Equations

• GapCVP.CLBoundedStates.instFintypeLocalCellSymbol tm = inferInstance

def GapCVP.CLPushAlphabet.cellAtomValue {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (stack : machine.tm.K) : CLBoundedStates.CellAtom machine.tm → Option (machine.tm.Γ stack)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.CLPushAlphabet.cellAtomValue machine stack none = none
• GapCVP.CLPushAlphabet.cellAtomValue machine stack (some (Sum.inl bit)) = if h : stack = machine.tm.k₀ then some (⋯ ▸ machine.inputAlphabet.invFun bit) else none

@[simp]

theorem GapCVP.CLPushAlphabet.cellAtomValue_blank {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (stack : machine.tm.K) : cellAtomValue machine stack none = none

@[simp]

theorem GapCVP.CLPushAlphabet.cellAtomValue_input {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (bit : Bool ⊕ Bool) : cellAtomValue machine machine.tm.k₀ (some (Sum.inl bit)) = some (machine.inputAlphabet.invFun bit)

noncomputable def GapCVP.CLPushAlphabet.StackAtomSupported {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (configuration : machine.tm.Cfg) : Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CLPushAlphabet.initialConfiguration_stackAtomSupported {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x certificate : List Bool) : StackAtomSupported machine (Turing.initList machine.tm (CLVerifier.verifierInput machine x certificate)) = true

def GapCVP.CLCellRows.paddedAtom {tm : Turing.FinTM2} (atoms : List (CLBoundedStates.CellAtom tm)) (index : ℕ) : CLBoundedStates.CellAtom tm

GapCVP reduction support.

Equations

• GapCVP.CLCellRows.paddedAtom atoms index = atoms[index]?.getD none

theorem GapCVP.CLCellRows.paddedAtom_decode {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (stack : machine.tm.K) {atoms : List (CLBoundedStates.CellAtom machine.tm)} {values : List (machine.tm.Γ stack)} (h : List.Forall₂ (fun (atom : CLBoundedStates.CellAtom machine.tm) (value : machine.tm.Γ stack) => CLPushAlphabet.cellAtomValue machine stack atom = some value) atoms values) (index : ℕ) : CLPushAlphabet.cellAtomValue machine stack (paddedAtom atoms index) = values[index]?

def GapCVP.CLCellRows.certificatePhase (certificate : List Bool) (index : ℕ) : CLBoundedStates.PhaseTag

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CLCellRows.certificatePhase_accepting_iff (certificate : List Bool) (index : ℕ) : certificatePhase certificate index = CLBoundedStates.PhaseTag.accepting ↔ index = certificate.length

def GapCVP.CLCellRows.guessingRow (tm : Turing.FinTM2) (width : ℕ) (certificate : List Bool) : GapCVP.CLCellRows.CellRow✝ tm width

GapCVP reduction support.

Equations

• GapCVP.CLCellRows.guessingRow tm width certificate index = (GapCVP.CLCellRows.certificatePhase certificate ↑index, none, fun (x : tm.K) => none, false)

def GapCVP.CLCellRows.configurationControl (tm : Turing.FinTM2) (configuration : tm.Cfg) : tm.Λ × tm.σ

GapCVP reduction support.

Equations

• GapCVP.CLCellRows.configurationControl tm configuration = (configuration.l.getD tm.main, configuration.var)

@[reducible, inline]

noncomputable abbrev GapCVP.CLCellRowBounds.rowWidth (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : ℕ

GapCVP reduction support.

Equations

• GapCVP.CLCellRowBounds.rowWidth bound machine x = Polynomial.eval x.length (GapCVP.CLNondeterminism.nondeterministicTableauDimensionPolynomial bound machine)

theorem GapCVP.CLCellRowBounds.certificateBound_le_rowWidth (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : Polynomial.eval x.length bound ≤ rowWidth bound machine x

def GapCVP.CLLocalWindows.statementStackActions {K : Type} {Γ : K → Type} {Λ σ : Type} : Turing.TM2.Stmt Γ Λ σ → ℕ

GapCVP reduction support.

Equations

• GapCVP.CLLocalWindows.statementStackActions (Turing.TM2.Stmt.push k a q) = GapCVP.CLLocalWindows.statementStackActions q + 1
• GapCVP.CLLocalWindows.statementStackActions (Turing.TM2.Stmt.peek k a q) = GapCVP.CLLocalWindows.statementStackActions q
• GapCVP.CLLocalWindows.statementStackActions (Turing.TM2.Stmt.pop k a q) = GapCVP.CLLocalWindows.statementStackActions q + 1
• GapCVP.CLLocalWindows.statementStackActions (Turing.TM2.Stmt.load a q) = GapCVP.CLLocalWindows.statementStackActions q
• GapCVP.CLLocalWindows.statementStackActions (Turing.TM2.Stmt.branch a yes no) = max (GapCVP.CLLocalWindows.statementStackActions yes) (GapCVP.CLLocalWindows.statementStackActions no)
• GapCVP.CLLocalWindows.statementStackActions (Turing.TM2.Stmt.goto a) = 0
• GapCVP.CLLocalWindows.statementStackActions Turing.TM2.Stmt.halt = 0

def GapCVP.CLLocalWindows.blockSize (tm : Turing.FinTM2) : ℕ

GapCVP reduction support.

Equations

• GapCVP.CLLocalWindows.blockSize tm = GapCVP.CLLocalWindows.maxStackEditsPerStep✝ tm + 1

theorem GapCVP.CLLocalWindows.blockSize_pos (tm : Turing.FinTM2) : 0 < blockSize tm

@[reducible, inline]

abbrev GapCVP.CLLocalWindows.BlockCell (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• GapCVP.CLLocalWindows.BlockCell tm = (Fin (GapCVP.CLLocalWindows.blockSize tm) → GapCVP.CLBoundedStates.LocalCellSymbol tm)

@[instance_reducible]

noncomputable instance GapCVP.CLLocalWindows.instFintypeBlockCell (tm : Turing.FinTM2) : Fintype (BlockCell tm)

Equations

• GapCVP.CLLocalWindows.instFintypeBlockCell tm = inferInstance

def GapCVP.CLLocalWindows.blankCell (tm : Turing.FinTM2) : CLBoundedStates.LocalCellSymbol tm

GapCVP reduction support.

Equations

• GapCVP.CLLocalWindows.blankCell tm = (GapCVP.CLBoundedStates.PhaseTag.guessing, none, fun (x : tm.K) => none, false)

def GapCVP.CLLocalWindows.packRow (tm : Turing.FinTM2) (width : ℕ) (row : GapCVP.CLCellRows.CellRow✝ tm width) : GapCVP.CLLocalWindows.BlockRow✝ tm width

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.CLLocalWindows.coordinateBlock (tm : Turing.FinTM2) (width : ℕ) (index : Fin (width + 1)) : Fin (width + 1)

GapCVP reduction support.

Equations

• GapCVP.CLLocalWindows.coordinateBlock tm width index = ⟨↑index / GapCVP.CLLocalWindows.blockSize tm, ⋯⟩

def GapCVP.CLLocalWindows.coordinateOffset (tm : Turing.FinTM2) (width : ℕ) (index : Fin (width + 1)) : Fin (blockSize tm)

GapCVP reduction support.

Equations

• GapCVP.CLLocalWindows.coordinateOffset tm width index = ⟨↑index % GapCVP.CLLocalWindows.blockSize tm, ⋯⟩

theorem GapCVP.CLLocalWindows.packRow_cell (tm : Turing.FinTM2) (width : ℕ) (row : GapCVP.CLCellRows.CellRow✝ tm width) (index : Fin (width + 1)) : packRow tm width row (coordinateBlock tm width index) (coordinateOffset tm width index) = row index

def GapCVP.CLLocalWindows.leftBlock (width : ℕ) (index : Fin (width + 1)) : Fin (width + 1)

GapCVP reduction support.

Equations

• GapCVP.CLLocalWindows.leftBlock width index = ⟨↑index - 1, ⋯⟩

def GapCVP.CLLocalWindows.rightBlock (width : ℕ) (index : Fin (width + 1)) : Fin (width + 1)

GapCVP reduction support.

Equations

• GapCVP.CLLocalWindows.rightBlock width index = ⟨min (↑index + 1) width, ⋯⟩

@[simp]

theorem GapCVP.CLLocalWindows.leftBlock_zero (width : ℕ) : leftBlock width 0 = 0

@[reducible, inline]

abbrev GapCVP.CLLocalRules.SummaryBlockCell (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• GapCVP.CLLocalRules.SummaryBlockCell tm = (GapCVP.CLLocalWindows.BlockCell tm × GapCVP.CLLocalWindows.BlockCell tm)

@[instance_reducible]

noncomputable instance GapCVP.CLLocalRules.instFintypeSummaryBlockCell (tm : Turing.FinTM2) : Fintype (SummaryBlockCell tm)

Equations

• GapCVP.CLLocalRules.instFintypeSummaryBlockCell tm = inferInstance

theorem GapCVP.CLTableauStitching.leftBlock_succ (width : ℕ) (index : Fin width) : CLLocalWindows.leftBlock width index.succ = index.castSucc

@[reducible, inline]

abbrev GapCVP.CLExactLocalRules.GuessPhaseWindow : Type

GapCVP reduction support.

Equations

• GapCVP.CLExactLocalRules.GuessPhaseWindow = (GapCVP.CLBoundedStates.PhaseTag × GapCVP.CLBoundedStates.PhaseTag × GapCVP.CLBoundedStates.PhaseTag × GapCVP.CLBoundedStates.PhaseTag)

noncomputable def GapCVP.CLExactLocalRules.GuessPhaseAllowed (window : GuessPhaseWindow) : Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.CLExactLocalRules.guessPhaseWindowAt (width : ℕ) (first next : List Bool) (index : Fin (width + 1)) : GuessPhaseWindow

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CLExactLocalRules.certificatePhase_append_before (certificate : List Bool) (bit : Bool) (index : ℕ) (hindex : index < certificate.length) : CLCellRows.certificatePhase (certificate ++ [bit]) index = CLCellRows.certificatePhase certificate index

theorem GapCVP.CLExactLocalRules.certificatePhase_append_old_marker (certificate : List Bool) (bit : Bool) : CLCellRows.certificatePhase (certificate ++ [bit]) certificate.length = if bit = true then CLBoundedStates.PhaseTag.verifying else CLBoundedStates.PhaseTag.guessing

theorem GapCVP.CLExactLocalRules.certificatePhase_append_new_marker (certificate : List Bool) (bit : Bool) : CLCellRows.certificatePhase (certificate ++ [bit]) (certificate.length + 1) = CLBoundedStates.PhaseTag.accepting

theorem GapCVP.CLExactLocalRules.certificatePhase_after (certificate : List Bool) (index : ℕ) (hindex : certificate.length < index) : CLCellRows.certificatePhase certificate index = CLBoundedStates.PhaseTag.guessing

theorem GapCVP.CLExactLocalRules.certificatePhase_append_after (certificate : List Bool) (bit : Bool) (index : ℕ) (hindex : certificate.length + 1 < index) : CLCellRows.certificatePhase (certificate ++ [bit]) index = CLCellRows.certificatePhase certificate index

theorem GapCVP.CLExactLocalRules.guessPhaseWindow_of_append (width : ℕ) (certificate : List Bool) (bit : Bool) (hspace : certificate.length < width) (index : Fin (width + 1)) : GuessPhaseAllowed (guessPhaseWindowAt width certificate (certificate ++ [bit]) index) = true

noncomputable def GapCVP.CLExactStackRules.SupportedStackValue {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (stack : machine.tm.K) (value : machine.tm.Γ stack) : Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CLExactStackRules.stackAtomSupported_supportedValues {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (configuration : machine.tm.Cfg) (supported : CLPushAlphabet.StackAtomSupported machine configuration = true) (stack : machine.tm.K) (value : machine.tm.Γ stack) : value ∈ configuration.stk stack → SupportedStackValue machine stack value = true

noncomputable def GapCVP.CLExactStackRules.canonicalCellAtom {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (stack : machine.tm.K) (value : machine.tm.Γ stack) (hsupported : SupportedStackValue machine stack value = true) : CLBoundedStates.CellAtom machine.tm

GapCVP reduction support.

Equations

• GapCVP.CLExactStackRules.canonicalCellAtom machine stack value hsupported = Classical.choose ⋯

theorem GapCVP.CLExactStackRules.canonicalCellAtom_decode {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (stack : machine.tm.K) (value : machine.tm.Γ stack) (hsupported : SupportedStackValue machine stack value = true) : CLPushAlphabet.cellAtomValue machine stack (canonicalCellAtom machine stack value hsupported) = some value

noncomputable def GapCVP.CLExactStackRules.canonicalStackAtoms {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (stack : machine.tm.K) (values : List (machine.tm.Γ stack)) (hsupported : ∀ value ∈ values, SupportedStackValue machine stack value = true) : List (CLBoundedStates.CellAtom machine.tm)

GapCVP reduction support.

Equations

• GapCVP.CLExactStackRules.canonicalStackAtoms machine stack values hsupported = List.pmap (GapCVP.CLExactStackRules.canonicalCellAtom machine stack) values hsupported

theorem GapCVP.CLExactStackRules.canonicalStackAtoms_length {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (stack : machine.tm.K) (values : List (machine.tm.Γ stack)) (hsupported : ∀ value ∈ values, SupportedStackValue machine stack value = true) : (canonicalStackAtoms machine stack values hsupported).length = values.length

theorem GapCVP.CLExactStackRules.canonicalStackAtoms_forall₂ {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (stack : machine.tm.K) (values : List (machine.tm.Γ stack)) (hsupported : ∀ value ∈ values, SupportedStackValue machine stack value = true) : List.Forall₂ (fun (atom : CLBoundedStates.CellAtom machine.tm) (value : machine.tm.Γ stack) => CLPushAlphabet.cellAtomValue machine stack atom = some value) (canonicalStackAtoms machine stack values hsupported) values

noncomputable def GapCVP.CLExactVerifierRules.StackPrefixAgreement {K : Type} {Γ : K → Type} (radius : ℕ) (first next : (stack : K) → List (Γ stack)) : Bool

GapCVP reduction support.

Equations

• GapCVP.CLExactVerifierRules.StackPrefixAgreement radius first next = decide (∀ (stack : K), List.take radius (first stack) = List.take radius (next stack))

theorem GapCVP.CLExactVerifierRules.stackPrefixAgreement_mono {K : Type} {Γ : K → Type} {small large : ℕ} {first next : (stack : K) → List (Γ stack)} (hbound : small ≤ large) (hagreement : StackPrefixAgreement large first next = true) : StackPrefixAgreement small first next = true

theorem GapCVP.CLExactVerifierRules.statementLookahead_le_blockSize (tm : Turing.FinTM2) (label : tm.Λ) : CLLocalWindows.statementStackActions (tm.m label) + 1 ≤ CLLocalWindows.blockSize tm

@[reducible, inline]

abbrev GapCVP.CLCompleteLocalCompiler.AtomBlock (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• GapCVP.CLCompleteLocalCompiler.AtomBlock tm = (Fin (GapCVP.CLLocalWindows.blockSize tm) → GapCVP.CLBoundedStates.CellAtom tm)

@[instance_reducible]

noncomputable instance GapCVP.CLCompleteLocalCompiler.instFintypeAtomBlock (tm : Turing.FinTM2) : Fintype (AtomBlock tm)

Equations

• GapCVP.CLCompleteLocalCompiler.instFintypeAtomBlock tm = inferInstance

@[reducible, inline]

abbrev GapCVP.CLCompleteLocalCompiler.SingleStackHint (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• GapCVP.CLCompleteLocalCompiler.SingleStackHint tm = (Fin (GapCVP.CLLocalWindows.blockSize tm) × Fin (GapCVP.CLLocalWindows.blockSize tm) × GapCVP.CLCompleteLocalCompiler.AtomBlock tm)

@[instance_reducible]

noncomputable instance GapCVP.CLCompleteLocalCompiler.instFintypeSingleStackHint (tm : Turing.FinTM2) : Fintype (SingleStackHint tm)

Equations

• GapCVP.CLCompleteLocalCompiler.instFintypeSingleStackHint tm = inferInstance

def GapCVP.CLCompleteLocalCompiler.atomBlockAt (tm : Turing.FinTM2) (atoms : List (CLBoundedStates.CellAtom tm)) (index : ℕ) : AtomBlock tm

GapCVP reduction support.

Equations

• GapCVP.CLCompleteLocalCompiler.atomBlockAt tm atoms index offset = GapCVP.CLCellRows.paddedAtom atoms (index * GapCVP.CLLocalWindows.blockSize tm + ↑offset)

@[reducible, inline]

abbrev GapCVP.CLCompleteLocalCompiler.StackShiftWindow (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.CLCompleteLocalCompiler.stackShiftWindowAt (tm : Turing.FinTM2) (width : ℕ) (first next : List (CLBoundedStates.CellAtom tm)) (index : Fin (width + 1)) : StackShiftWindow tm

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.CLCompleteLocalCompiler.shiftedWindowAtom (tm : Turing.FinTM2) (hint : SingleStackHint tm) (window : StackShiftWindow tm) (offset : Fin (CLLocalWindows.blockSize tm)) : CLBoundedStates.CellAtom tm

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.CLCompleteLocalCompiler.StackShiftAllowed (tm : Turing.FinTM2) (hint : SingleStackHint tm) (window : StackShiftWindow tm) : Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.CLCompleteLocalCompiler.stackShiftAllowed (tm : Turing.FinTM2) (hint : SingleStackHint tm) (window : StackShiftWindow tm) : Bool

GapCVP reduction support.

Equations

• GapCVP.CLCompleteLocalCompiler.stackShiftAllowed tm hint window = decide (GapCVP.CLCompleteLocalCompiler.StackShiftAllowed tm hint window = true)

theorem GapCVP.CLCompleteLocalCompiler.stackShiftAllowed_iff (tm : Turing.FinTM2) (hint : SingleStackHint tm) (window : StackShiftWindow tm) : stackShiftAllowed tm hint window = true ↔ StackShiftAllowed tm hint window = true

noncomputable def GapCVP.CLStackShiftSoundness2.NoBlankAtoms (tm : Turing.FinTM2) (atoms : List (CLBoundedStates.CellAtom tm)) : Bool

GapCVP reduction support.

Equations

• GapCVP.CLStackShiftSoundness2.NoBlankAtoms tm atoms = decide (∀ atom ∈ atoms, atom ≠ none)

theorem GapCVP.CLStackShiftSoundness2.atomSuffix_iff_paddedShift (tm : Turing.FinTM2) (first next : List (CLBoundedStates.CellAtom tm)) (hfirst : NoBlankAtoms tm first = true) (hnext : NoBlankAtoms tm next = true) (firstDrop nextDrop : ℕ) : List.drop firstDrop first = List.drop nextDrop next ↔ ∀ (index : ℕ), CLCellRows.paddedAtom first (firstDrop + index) = CLCellRows.paddedAtom next (nextDrop + index)

theorem GapCVP.CLFiniteShiftWindows.paddedAtom_none_of_length_le (tm : Turing.FinTM2) (atoms : List (CLBoundedStates.CellAtom tm)) (index : ℕ) (hindex : atoms.length ≤ index) : CLCellRows.paddedAtom atoms index = none

noncomputable def GapCVP.CLFiniteShiftWindows.AllStackShiftWindows (tm : Turing.FinTM2) (width : ℕ) (hint : CLCompleteLocalCompiler.SingleStackHint tm) (first next : List (CLBoundedStates.CellAtom tm)) : Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.CLFiniteShiftWindows.PrefixHintCorrect (tm : Turing.FinTM2) (hint : CLCompleteLocalCompiler.SingleStackHint tm) (next : List (CLBoundedStates.CellAtom tm)) : Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CLFiniteShiftWindows.width_le_block_capacity (tm : Turing.FinTM2) (width : ℕ) : width ≤ width * CLLocalWindows.blockSize tm

theorem GapCVP.CLFiniteShiftWindows.shiftedWindowAtom_eq_old (tm : Turing.FinTM2) (width : ℕ) (first next : List (CLBoundedStates.CellAtom tm)) (hfirstLength : first.length ≤ width) (hint : CLCompleteLocalCompiler.SingleStackHint tm) (index : Fin (width + 1)) (offset : Fin (CLLocalWindows.blockSize tm)) (hnotPrefix : ¬(↑index = 0 ∧ ↑offset < ↑hint.2.1)) : CLCompleteLocalCompiler.shiftedWindowAtom tm hint (CLCompleteLocalCompiler.stackShiftWindowAt tm width first next index) offset = CLCellRows.paddedAtom first (↑index * CLLocalWindows.blockSize tm + ↑offset - ↑hint.2.1 + ↑hint.1)

@[reducible, inline]

abbrev GapCVP.CLExactVerifierTransition.FiniteVerifierHint (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• GapCVP.CLExactVerifierTransition.FiniteVerifierHint tm = (tm.K → GapCVP.CLCompleteLocalCompiler.SingleStackHint tm)

@[instance_reducible]

noncomputable instance GapCVP.CLExactVerifierTransition.instFintypeFiniteVerifierHint (tm : Turing.FinTM2) : Fintype (FiniteVerifierHint tm)

Equations

• GapCVP.CLExactVerifierTransition.instFintypeFiniteVerifierHint tm = inferInstance

noncomputable def GapCVP.CLExactVerifierTransition.AllVerifierStackWindows {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (width : ℕ) (first next : machine.tm.Cfg) (hfirst : CLPushAlphabet.StackAtomSupported machine first = true) (hnext : CLPushAlphabet.StackAtomSupported machine next = true) (hint : FiniteVerifierHint machine.tm) : Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.CLEmittedCNFTM.boundedLookupOutput (limit : ℕ) (table : List Bool → Bool) (input : List Bool) : Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.CLEmittedCNFTM.boundedLookupComputable (limit : ℕ) (table : List Bool → Bool) : BitTM fun (input : List Bool) => [boundedLookupOutput limit table input]

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CLWindowTruthTable.boundedLookupOutput_of_length_le (limit : ℕ) (table : List Bool → Bool) (input : List Bool) (hinput : input.length ≤ limit) : CLEmittedCNFTM.boundedLookupOutput limit table input = table input

theorem GapCVP.CLLocalTableauCompiler.filterMap_ofFn_getElem {α : Type} (values : List α) (width : ℕ) : List.filterMap id (List.ofFn fun (index : Fin width) => values[↑index]?) = List.take width values

def GapCVP.CLLocalTableauCompiler.decodedAtomBlock {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (stack : machine.tm.K) (block : CLCompleteLocalCompiler.AtomBlock machine.tm) : List (machine.tm.Γ stack)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CLLocalTableauCompiler.decodedAtomBlock_canonical {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (stack : machine.tm.K) (values : List (machine.tm.Γ stack)) (hsupported : ∀ value ∈ values, CLExactStackRules.SupportedStackValue machine stack value = true) : decodedAtomBlock machine stack (CLCompleteLocalCompiler.atomBlockAt machine.tm (CLExactStackRules.canonicalStackAtoms machine stack values hsupported) 0) = List.take (CLLocalWindows.blockSize machine.tm) values

@[reducible, inline]

abbrev GapCVP.CLLocalTableauCompiler.FiniteVerifierHeadQuery (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• GapCVP.CLLocalTableauCompiler.FiniteVerifierHeadQuery tm = ((Option tm.Λ × tm.σ) × (tm.K → GapCVP.CLCompleteLocalCompiler.AtomBlock tm) × Option tm.Λ × tm.σ)

def GapCVP.CLLocalTableauCompiler.finiteHeadConfiguration {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (control : Option machine.tm.Λ × machine.tm.σ) (heads : machine.tm.K → CLCompleteLocalCompiler.AtomBlock machine.tm) : machine.tm.Cfg

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CLVerifierTableauEmission.prefixHintCorrect_of_allStackShiftWindows (tm : Turing.FinTM2) (width : ℕ) (first next : List (CLBoundedStates.CellAtom tm)) (hint : CLCompleteLocalCompiler.SingleStackHint tm) (hwindows : CLFiniteShiftWindows.AllStackShiftWindows tm width hint first next = true) : CLFiniteShiftWindows.PrefixHintCorrect tm hint next = true

structure GapCVP.CLUnconditionalTableau.PrefixScript {K : Type} (Γ : K → Type) : Type

GapCVP reduction support.

• dropped : K → ℕ

  GapCVP reduction support.

• pushed (stack : K) : List (Γ stack)

  GapCVP reduction support.

def GapCVP.CLUnconditionalTableau.scriptStacks {K : Type} {Γ : K → Type} (original : (stack : K) → List (Γ stack)) (script : PrefixScript Γ) (stack : K) : List (Γ stack)

GapCVP reduction support.

Equations

• GapCVP.CLUnconditionalTableau.scriptStacks original script stack = script.pushed stack ++ List.drop (script.dropped stack) (original stack)

def GapCVP.CLUnconditionalTableau.emptyPrefixScript {K : Type} (Γ : K → Type) : PrefixScript Γ

GapCVP reduction support.

Equations

• GapCVP.CLUnconditionalTableau.emptyPrefixScript Γ = { dropped := fun (x : K) => 0, pushed := fun (x : K) => [] }

@[simp]

theorem GapCVP.CLUnconditionalTableau.scriptStacks_empty {K : Type} {Γ : K → Type} (original : (stack : K) → List (Γ stack)) : scriptStacks original (emptyPrefixScript Γ) = original

def GapCVP.CLUnconditionalTableau.executePrefixScript {K : Type} {Γ : K → Type} {Λ σ : Type} [DecidableEq K] : Turing.TM2.Stmt Γ Λ σ → σ → ((stack : K) → List (Γ stack)) → PrefixScript Γ → Option Λ × σ × PrefixScript Γ

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.CLUnconditionalTableau.executePrefixScript (Turing.TM2.Stmt.load update continuation) x✝² x✝¹ x✝ = GapCVP.CLUnconditionalTableau.executePrefixScript continuation (update x✝²) x✝¹ x✝
• GapCVP.CLUnconditionalTableau.executePrefixScript (Turing.TM2.Stmt.goto update) x✝² x✝¹ x✝ = (some (update x✝²), x✝², x✝)
• GapCVP.CLUnconditionalTableau.executePrefixScript Turing.TM2.Stmt.halt x✝² x✝¹ x✝ = (none, x✝², x✝)

theorem GapCVP.CLUnconditionalTableau.executePrefixScript_correct {K : Type} {Γ : K → Type} {Λ σ : Type} [DecidableEq K] (statement : Turing.TM2.Stmt Γ Λ σ) (state : σ) (original : (stack : K) → List (Γ stack)) (script : PrefixScript Γ) : Turing.TM2.stepAux statement state (scriptStacks original script) = { l := (executePrefixScript statement state original script).1, var := (executePrefixScript statement state original script).2.1, stk := scriptStacks original (executePrefixScript statement state original script).2.2 }

theorem GapCVP.CLUnconditionalTableau.executePrefixScript_of_prefix {K : Type} {Γ : K → Type} {Λ σ : Type} [DecidableEq K] (statement : Turing.TM2.Stmt Γ Λ σ) (state : σ) (first second : (stack : K) → List (Γ stack)) (script : PrefixScript Γ) (hagreement : CLExactVerifierRules.StackPrefixAgreement (CLLocalWindows.statementStackActions statement + 1) (scriptStacks first script) (scriptStacks second script) = true) : executePrefixScript statement state first script = executePrefixScript statement state second script

def GapCVP.CLGlobalTableauSimulation.finiteHeadScriptRun {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (label : machine.tm.Λ) (state : machine.tm.σ) (heads : machine.tm.K → CLCompleteLocalCompiler.AtomBlock machine.tm) : Option machine.tm.Λ × machine.tm.σ × CLUnconditionalTableau.PrefixScript machine.tm.Γ

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GapCVP.CLGlobalTableauSimulation.ScriptVerifierQuery (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.CLGlobalTableauSimulation.scriptVerifierAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (query : ScriptVerifierQuery machine.tm) : Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CLGlobalTableauSimulation.scriptVerifierAllowed_iff {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (query : ScriptVerifierQuery machine.tm) : scriptVerifierAllowed machine query = true ↔ ∃ (label : machine.tm.Λ), query.1.1.1 = some label ∧ have run := finiteHeadScriptRun machine label query.1.1.2 query.1.2.1; run.1 = query.1.2.2.1 ∧ run.2.1 = query.1.2.2.2 ∧ ∀ (stack : machine.tm.K), ↑(query.2.2 stack).1 = run.2.2.dropped stack ∧ ↑(query.2.2 stack).2.1 = (run.2.2.pushed stack).length ∧ List.take (run.2.2.pushed stack).length (CLLocalTableauCompiler.decodedAtomBlock machine stack (query.2.1 stack)) = run.2.2.pushed stack

noncomputable def GapCVP.CLGlobalTableauSimulation.scriptVerifierQueryOf {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (first next : machine.tm.Cfg) (hfirst : CLPushAlphabet.StackAtomSupported machine first = true) (hnext : CLPushAlphabet.StackAtomSupported machine next = true) (hint : CLExactVerifierTransition.FiniteVerifierHint machine.tm) : ScriptVerifierQuery machine.tm

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CLGlobalTableauSimulation.configuration_eq_of_components (tm : Turing.FinTM2) (first next : tm.Cfg) (hlabel : first.l = next.l) (hstate : first.var = next.var) (hstacks : first.stk = next.stk) : first = next

theorem GapCVP.CLGlobalTableauSimulation.actualStep_of_stepAux (tm : Turing.FinTM2) (first next : tm.Cfg) (label : tm.Λ) (hlabel : first.l = some label) (haux : Turing.TM2.stepAux (tm.m label) first.var first.stk = next) : tm.step first = some next

theorem GapCVP.CLGlobalTableauSimulation.actualStep_iff_finite_script_and_windows {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (width : ℕ) (first next : machine.tm.Cfg) (hfirst : CLPushAlphabet.StackAtomSupported machine first = true) (hnext : CLPushAlphabet.StackAtomSupported machine next = true) (hfirstLength : ∀ (stack : machine.tm.K), (first.stk stack).length ≤ width) (hnextLength : ∀ (stack : machine.tm.K), (next.stk stack).length ≤ width) : machine.tm.step first = some next ↔ ∃ (hint : CLExactVerifierTransition.FiniteVerifierHint machine.tm), scriptVerifierAllowed machine (scriptVerifierQueryOf machine first next hfirst hnext hint) = true ∧ CLExactVerifierTransition.AllVerifierStackWindows machine width first next hfirst hnext hint = true

def GapCVP.CLTableauSimulationCert.stackAtomsOfBlock (tm : Turing.FinTM2) (block : CLLocalWindows.BlockCell tm) (stack : tm.K) : CLCompleteLocalCompiler.AtomBlock tm

GapCVP reduction support.

Equations

• GapCVP.CLTableauSimulationCert.stackAtomsOfBlock tm block stack offset = (block offset).2.2.1 stack

def GapCVP.CLTableauSimulationCert.machineControlOfBlock (tm : Turing.FinTM2) (block : CLLocalWindows.BlockCell tm) : Option (Option tm.Λ × tm.σ)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GapCVP.CLTableauSimulationCert.ScriptBlockCell (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• GapCVP.CLTableauSimulationCert.ScriptBlockCell tm = (GapCVP.CLLocalRules.SummaryBlockCell tm × GapCVP.CLExactVerifierTransition.FiniteVerifierHint tm × Bool)

@[instance_reducible]

noncomputable instance GapCVP.CLTableauSimulationCert.instFintypeScriptBlockCell (tm : Turing.FinTM2) : Fintype (ScriptBlockCell tm)

Equations

• GapCVP.CLTableauSimulationCert.instFintypeScriptBlockCell tm = inferInstance

@[reducible, inline]

abbrev GapCVP.CLTableauSimulationCert.ScriptBlockRow (tm : Turing.FinTM2) (width : ℕ) : Type

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.CLTableauSimulationCert.ScriptBlockRow tm width = (Fin (width + 1) → GapCVP.CLTableauSimulationCert.ScriptBlockCell tm)

@[reducible, inline]

abbrev GapCVP.CLTableauSimulationCert.ScriptBlockWindow (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.CLTableauSimulationCert.scriptBlockWindowAt (tm : Turing.FinTM2) (width : ℕ) (first next : ScriptBlockRow tm width) (index : Fin (width + 1)) : ScriptBlockWindow tm

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.CLTableauSimulationCert.canonicalVerifyingRow {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (width : ℕ) (certificate : List Bool) (configuration : machine.tm.Cfg) (hsupported : CLPushAlphabet.StackAtomSupported machine configuration = true) : GapCVP.CLCellRows.CellRow✝ machine.tm width

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CLTableauSimulationCert.stackAtomsOfBlock_pack_canonical {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (width : ℕ) (certificate : List Bool) (configuration : machine.tm.Cfg) (hsupported : CLPushAlphabet.StackAtomSupported machine configuration = true) (hstackLength : ∀ (stack : machine.tm.K), (configuration.stk stack).length ≤ width) (index : Fin (width + 1)) (stack : machine.tm.K) : stackAtomsOfBlock machine.tm (CLLocalWindows.packRow machine.tm width (canonicalVerifyingRow machine width certificate configuration hsupported) index) stack = CLCompleteLocalCompiler.atomBlockAt machine.tm (CLExactStackRules.canonicalStackAtoms machine stack (configuration.stk stack) ⋯) ↑index

noncomputable def GapCVP.CLTableauSimulationCert.canonicalScriptBlockRow {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (width : ℕ) (certificate : List Bool) (configuration : machine.tm.Cfg) (hsupported : CLPushAlphabet.StackAtomSupported machine configuration = true) (hint : CLExactVerifierTransition.FiniteVerifierHint machine.tm) : ScriptBlockRow machine.tm width

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CLTableauSimulationCert.machineControlOfBlock_pack_canonical {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (width : ℕ) (certificate : List Bool) (configuration : machine.tm.Cfg) (hsupported : CLPushAlphabet.StackAtomSupported machine configuration = true) : machineControlOfBlock machine.tm (CLLocalWindows.packRow machine.tm width (canonicalVerifyingRow machine width certificate configuration hsupported) 0) = some (configuration.l, configuration.var)

def GapCVP.CLTableauSimulationCert.scriptQueryOfBlockWindow {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : ScriptBlockWindow machine.tm) : Option (CLGlobalTableauSimulation.ScriptVerifierQuery machine.tm)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.CLTableauSimulationCert.stackWindowOfScriptBlock (tm : Turing.FinTM2) (window : ScriptBlockWindow tm) (stack : tm.K) : CLCompleteLocalCompiler.StackShiftWindow tm

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.CLTableauSimulationCert.ScriptBlockCoherent (tm : Turing.FinTM2) (window : ScriptBlockWindow tm) : Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.CLTableauSimulationCert.scriptBlockAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : ScriptBlockWindow machine.tm) : Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CLTableauSimulationCert.scriptBlockAllowed_iff {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : ScriptBlockWindow machine.tm) : scriptBlockAllowed machine window = true ↔ ScriptBlockCoherent machine.tm window = true ∧ ∃ (query : CLGlobalTableauSimulation.ScriptVerifierQuery machine.tm), scriptQueryOfBlockWindow machine window = some query ∧ CLGlobalTableauSimulation.scriptVerifierAllowed machine query = true ∧ ∀ (stack : machine.tm.K), CLCompleteLocalCompiler.stackShiftAllowed machine.tm (window.2.1.2.1 stack) (stackWindowOfScriptBlock machine.tm window stack) = true

theorem GapCVP.CLTableauSimulationCert.canonicalScriptBlockWindows_iff {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (width : ℕ) (certificate : List Bool) (first next : machine.tm.Cfg) (hfirst : CLPushAlphabet.StackAtomSupported machine first = true) (hnext : CLPushAlphabet.StackAtomSupported machine next = true) (hfirstLength : ∀ (stack : machine.tm.K), (first.stk stack).length ≤ width) (hnextLength : ∀ (stack : machine.tm.K), (next.stk stack).length ≤ width) (firstHint nextHint : CLExactVerifierTransition.FiniteVerifierHint machine.tm) : (∀ (index : Fin (width + 1)), scriptBlockAllowed machine (scriptBlockWindowAt machine.tm width (canonicalScriptBlockRow machine width certificate first hfirst firstHint) (canonicalScriptBlockRow machine width certificate next hnext nextHint) index) = true) ↔ CLGlobalTableauSimulation.scriptVerifierAllowed machine (CLGlobalTableauSimulation.scriptVerifierQueryOf machine first next hfirst hnext firstHint) = true ∧ CLExactVerifierTransition.AllVerifierStackWindows machine width first next hfirst hnext firstHint = true

theorem GapCVP.CLTableauSimulationCert.actualStep_iff_canonical_block_windows {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (width : ℕ) (certificate : List Bool) (first next : machine.tm.Cfg) (hfirst : CLPushAlphabet.StackAtomSupported machine first = true) (hnext : CLPushAlphabet.StackAtomSupported machine next = true) (hfirstLength : ∀ (stack : machine.tm.K), (first.stk stack).length ≤ width) (hnextLength : ∀ (stack : machine.tm.K), (next.stk stack).length ≤ width) : machine.tm.step first = some next ↔ ∃ (firstHint : CLExactVerifierTransition.FiniteVerifierHint machine.tm) (nextHint : CLExactVerifierTransition.FiniteVerifierHint machine.tm), ∀ (index : Fin (width + 1)), scriptBlockAllowed machine (scriptBlockWindowAt machine.tm width (canonicalScriptBlockRow machine width certificate first hfirst firstHint) (canonicalScriptBlockRow machine width certificate next hnext nextHint) index) = true

def GapCVP.CLFullTableauEmitter.defaultVerifierHint (tm : Turing.FinTM2) : CLExactVerifierTransition.FiniteVerifierHint tm

GapCVP reduction support.

Equations

• GapCVP.CLFullTableauEmitter.defaultVerifierHint tm x✝ = GapCVP.CLFullTableauEmitter.defaultSingleStackHint✝ tm

def GapCVP.CLFullTableauEmitter.defaultScriptBlockCell (tm : Turing.FinTM2) : CLTableauSimulationCert.ScriptBlockCell tm

Internal support shared across GapCVP continuation modules.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CLVerifierPhaseCert.configurationTrace_stackAtomSupported {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x certificate : List Bool) {output : List (machine.tm.Γ machine.tm.k₁)} {steps : ℕ} (trace : CLVerifier.ConfigurationTrace machine.tm (CLVerifier.verifierInput machine x certificate) output steps) (time : Fin (steps + 1)) : CLPushAlphabet.StackAtomSupported machine (trace.configuration time) = true

theorem GapCVP.CLVerifierPhaseCert.acceptedExecution_stack_length_le_rowWidth (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) {x : List Bool} (execution : CLVerifier.AcceptedExecution bound machine x) (time : Fin (execution.steps + 1)) (stack : machine.tm.K) : ((execution.trace.configuration time).stk stack).length ≤ CLCellRowBounds.rowWidth bound machine x

inductive GapCVP.CLCompleteVerifierSimulation.PairedInputTag : Type

GapCVP reduction support.

• bit (value : Bool ⊕ Bool) : PairedInputTag
• marker : PairedInputTag
• blank : PairedInputTag

def GapCVP.CLCompleteVerifierSimulation.instDecidableEqPairedInputTag.decEq (x✝ x✝¹ : PairedInputTag) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance GapCVP.CLCompleteVerifierSimulation.instDecidableEqPairedInputTag : DecidableEq PairedInputTag

Equations

• GapCVP.CLCompleteVerifierSimulation.instDecidableEqPairedInputTag = GapCVP.CLCompleteVerifierSimulation.instDecidableEqPairedInputTag.decEq

@[instance_reducible]

instance GapCVP.CLCompleteVerifierSimulation.instFintypePairedInputTag : Fintype PairedInputTag

Equations

• GapCVP.CLCompleteVerifierSimulation.instFintypePairedInputTag = Fintype.ofEquiv ((Bool ⊕ Bool) ⊕ Unit ⊕ Unit) GapCVP.CLCompleteVerifierSimulation.PairedInputTag.proxyTypeEquiv

def GapCVP.CLCompleteVerifierSimulation.pairedInputTagAt (x certificate : List Bool) (index : ℕ) : PairedInputTag

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GapCVP.CLCompleteVerifierSimulation.pairedInputTagAt_marker (x certificate : List Bool) : pairedInputTagAt x certificate (x.length + certificate.length) = PairedInputTag.marker

theorem GapCVP.CLCompleteVerifierSimulation.pairBitEncoding_append_guess (x certificate : List Bool) (bit : Bool) : pairBitEncoding (x, certificate ++ [bit]) = pairBitEncoding (x, certificate) ++ [Sum.inr bit]