Total output truncation for the actual advice program

The requested output consists of its first coordinates, with false bits beyond the actual output width. Both honest and tampered programs use this same total map. The retained law keeps the original shared tag and entire right state, together with the truncated tampered output.

def Algebraic.Cutwidth.Extractor.adviceOutputPrefix (out : ℕ) {d : ℕ} (bits : Fin d → Bool) : Fin out → Bool

Keep the first requested bits, completing positions beyond the input width by false.

Equations

• Algebraic.Cutwidth.Extractor.adviceOutputPrefix out bits i = (List.ofFn bits)[↑i]?.getD false

def Algebraic.Cutwidth.Extractor.adviceTruncatedCorrelationBreaker (n m L e out : ℕ) (x : Fin n → Bool) (y : Fin m → Bool) (advice : List Bool) : Fin out → Bool

The actual advice correlation breaker at a requested total output width.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.adviceTruncatedCorrelationBreakerWeight (n m L e out : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → Fin n → Bool) (y y' : Z → B → Fin m → Bool) (advice advice' : List Bool) : ((Z × B) × (Fin out → Bool)) × (Fin out → Bool) → ℝ

Both truncated programs, retaining the original right state and truncated tampered output.

Equations

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