Embedding a small test into the fixed tampering slots

The honest call is removed from the Cartesian product of the tested coordinates with all candidates. At most 4 * C - 1 calls remain. An embedding places these calls in the fixed slot type; a partial inverse fills every unused slot with a caller-supplied padding value.

def Algebraic.Cutwidth.Extractor.Internal.affineTestDummyAdvice : List Bool → List Bool

Change the first advice bit, preserving every remaining bit.

Equations

• Algebraic.Cutwidth.Extractor.Internal.affineTestDummyAdvice [] = []
• Algebraic.Cutwidth.Extractor.Internal.affineTestDummyAdvice (b :: bs) = (!b) :: bs

theorem Algebraic.Cutwidth.Extractor.Internal.affineTestDummyAdvice_length (advice : List Bool) : (affineTestDummyAdvice advice).length = advice.length

theorem Algebraic.Cutwidth.Extractor.Internal.affineTestDummyAdvice_ne (advice : List Bool) (positive : 0 < advice.length) : advice ≠ affineTestDummyAdvice advice

def Algebraic.Cutwidth.Extractor.Internal.affineTestOtherSlots {N C : ℕ} (U : Finset (Fin N)) (j : Fin N) (z : Fin C) : Finset (Fin N × Fin C)

Real calls except for the already chosen honest coordinate and candidate.

Equations

• Algebraic.Cutwidth.Extractor.Internal.affineTestOtherSlots U j z = (U.product Finset.univ).erase (j, z)

theorem Algebraic.Cutwidth.Extractor.Internal.affineTestOtherSlots_ne {N C : ℕ} (U : Finset (Fin N)) (j : Fin N) (z : Fin C) (v : ↥(affineTestOtherSlots U j z)) : ↑v ≠ (j, z)

theorem Algebraic.Cutwidth.Extractor.Internal.affineTestOtherSlots_card {N C : ℕ} (U : Finset (Fin N)) (small : U.card ≤ 4) (j : Fin N) (member : j ∈ U) (z : Fin C) : Fintype.card ↥(affineTestOtherSlots U j z) ≤ Fintype.card (Fin (4 * C - 1))

theorem Algebraic.Cutwidth.Extractor.Internal.affineTestOtherSlots_prod {N C : ℕ} (U : Finset (Fin N)) (j : Fin N) (member : j ∈ U) (z : Fin C) (f : Fin N × Fin C → ℝ) : f (j, z) * ∏ v : ↥(affineTestOtherSlots U j z), f ↑v = ∏ i ∈ U, ∏ k : Fin C, f (i, k)

noncomputable def Algebraic.Cutwidth.Extractor.Internal.affineTestPadded {ι : Type u_1} {α : Type u_2} {τ : ℕ} (embedding : ι ↪ Fin τ) (real : ι → α) (padding : α) (i : Fin τ) : α

Extend the genuinely used slots by a fixed padding value.

Equations

• Algebraic.Cutwidth.Extractor.Internal.affineTestPadded embedding real padding i = (Function.partialInv (⇑embedding) i).elim padding real

theorem Algebraic.Cutwidth.Extractor.Internal.affineTestPadded_apply {ι : Type u_1} {α : Type u_2} {τ : ℕ} (embedding : ι ↪ Fin τ) (real : ι → α) (padding : α) (i : ι) : affineTestPadded embedding real padding (embedding i) = real i

theorem Algebraic.Cutwidth.Extractor.Internal.affineTestPadded_property {ι : Type u_1} {α : Type u_2} {τ : ℕ} (embedding : ι ↪ Fin τ) (real : ι → α) (padding : α) (P : α → Prop) (used : ∀ (i : ι), P (real i)) (unused : P padding) (i : Fin τ) : P (affineTestPadded embedding real padding i)