The actual strong advice-correlation-breaker law

Run both concrete advice programs on the original factored sources. The honest output is compared with uniform while retaining the original transcript, the entire original right state, and the tampered output. Thus this law retains both right inputs even when they are correlated.

The program is Chattopadhyay--Goyal--Li Algorithm 2 followed by the final left-source extraction specified in Advice.Defs. The finite error budget uses conservative amplification of the checked per-bit error; it does not claim the sharper error parameters of the original construction.

noncomputable def Algebraic.Cutwidth.Extractor.adviceCorrelationBreakerWeight (n m L e : ℕ) {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 (matchedBlockSeedBits L) → Bool)) × (Fin (matchedBlockSeedBits L) → Bool) → ℝ

Both actual advice programs, retaining the entire original right state and tampered output.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.adviceCorrelationBreakerError (m L e a : ℕ) (α : ℝ) : ℝ

A finite error budget for advice length a and original left-envelope total α.

Equations

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