Extraction by the complete actual advice program #
The original factored inputs construct the initial invariant. Paired advice is processed by the actual fold, and unequal advice supplies separation at its end. Final extraction retains the original right state and the actual tampered output. Thus only original-source hypotheses occur in the result; no intermediate extractor certificate or transcript witness is assumed.
This implements the CGL Algorithm 2 advice-chain argument with the extra final extraction from the original left source. The finite bound uses the conservative checked recurrence, rather than the sharper published error.
theorem
Algebraic.Cutwidth.Extractor.Internal.adviceCorrelationBreaker_chain_dist_le
(n m L e : ℕ)
{Z A B : Type u}
[Fintype Z]
[Fintype A]
[Fintype B]
(guard : FlipFlopSizeGuard n m L e)
(size : matchedBlockOutputBits 64 L ≤ m)
(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 → ℝ)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(nonnegative : ∀ (z : Z), 0 ≤ μ z)
(cap : ∀ (z : Z) (x₀ : Fin n → Bool), w z * mapWeight (x z) (l z) x₀ ≤ μ z)
(uniform : ∀ (z : Z), mapWeight (y z) (r z) = uniformWeight (Fin m → Bool))
(length : advice.length = advice'.length)
(different : advice ≠ advice')
:
have actual := adviceCorrelationBreakerWeight n m L e w l r x x' y y' advice advice';
have D := ↑(Fintype.card (Fin (matchedBlockSeedBits L) → Bool));
weightDist actual (uniformSecondWeight actual) ≤ adviceChainError L e 0 (∑ z : Z, μ z) (2 ^ m)⁻¹ advice.length + (2 ^ e)⁻¹ + 2 ^ (2 ^ 62 * L) * D ^ (8 * advice.length + 1) * ∑ z : Z, μ z
theorem
Algebraic.Cutwidth.Extractor.Internal.adviceCorrelationBreaker_dist_le
(n m L e : ℕ)
{Z A B : Type u}
[Fintype Z]
[Fintype A]
[Fintype B]
(guard : FlipFlopSizeGuard n m L e)
(size : matchedBlockOutputBits 64 L ≤ m)
(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 → ℝ)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(nonnegative : ∀ (z : Z), 0 ≤ μ z)
(cap : ∀ (z : Z) (x₀ : Fin n → Bool), w z * mapWeight (x z) (l z) x₀ ≤ μ z)
(uniform : ∀ (z : Z), mapWeight (y z) (r z) = uniformWeight (Fin m → Bool))
(length : advice.length = advice'.length)
(different : advice ≠ advice')
:
have actual := adviceCorrelationBreakerWeight n m L e w l r x x' y y' advice advice';
weightDist actual (uniformSecondWeight actual) ≤ adviceCorrelationBreakerError m L e advice.length (∑ z : Z, μ z)
theorem
Algebraic.Cutwidth.Extractor.Internal.adviceCorrelationBreaker_dyadic_dist_le
(n m L target : ℕ)
{Z A B : Type u}
[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 → ℝ)
(guard : FlipFlopSizeGuard n m L (adviceErrorExponent advice.length target))
(size : matchedBlockOutputBits 64 L ≤ m)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(nonnegative : ∀ (z : Z), 0 ≤ μ z)
(cap : ∀ (z : Z) (x₀ : Fin n → Bool), w z * mapWeight (x z) (l z) x₀ ≤ μ z)
(uniform : ∀ (z : Z), mapWeight (y z) (r z) = uniformWeight (Fin m → Bool))
(length : advice.length = advice'.length)
(different : advice ≠ advice')
(left : ∑ z : Z, μ z ≤ (2 ^ (2 ^ 150 * (advice.length + 1) * L))⁻¹)
(right : 2 ^ 150 * (advice.length + 1) * L ≤ m)
:
have e := adviceErrorExponent advice.length target;
have actual := adviceCorrelationBreakerWeight n m L e w l r x x' y y' advice advice';
weightDist actual (uniformSecondWeight actual) ≤ (2 ^ target)⁻¹