The combined canonical DNF switching injection

This module replaces the elementary per-query advice alphabet in the canonical switching injection by the counted source-term block encoding. The explicit decoder proves injectivity on the bad event, and the general weighted restriction engine yields the exact scaled bound with advice base ((5t - 1) / 2)^s for positive width t.

def Algebraic.AC0.Switching.defaultBlock {width : ℕ} [NeZero width] (difference : Bool) : BlockAdvice width 1

The one-position block advice at position 0 with the given difference bit.

Equations

• Algebraic.AC0.Switching.defaultBlock difference = { positions := ⟨{Fin.ofNat width 0}, ⋯⟩, differences := fun (x : Fin 1) => difference }

theorem Algebraic.AC0.Switching.defaultBlock_true_hasMismatch {width : ℕ} [NeZero width] : (defaultBlock true).HasMismatch

def Algebraic.AC0.Switching.defaultCombinedAdvice {width : ℕ} [NeZero width] (pathLength : ℕ) : CombinedAdvice width pathLength

A harmless total combined-advice value used outside the bad event.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.AC0.Switching.defaultCombinedAdvice 0 = ⋯.mpr PUnit.unit
• Algebraic.AC0.Switching.defaultCombinedAdvice 1 = Algebraic.AC0.Switching.CombinedAdvice.ofFinalBlock (Algebraic.AC0.Switching.defaultBlock false) ⋯

noncomputable def Algebraic.AC0.Switching.combinedCanonicalEncoding {widthBound n : ℕ} [NeZero widthBound] (formula : DNF n) (bounded : formula.WidthAtMost widthBound) (pathLength : ℕ) (rho : PartialAssignment n) : PartialAssignment n × CombinedAdvice widthBound pathLength

Total combined restriction/advice encoding for the canonical-depth bad event.

Equations

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

theorem Algebraic.AC0.Switching.combinedCanonicalEncoding_fst_of_deep {widthBound n : ℕ} [NeZero widthBound] (formula : DNF n) (bounded : formula.WidthAtMost widthBound) (pathLength : ℕ) (rho : PartialAssignment n) (deep : formula.CanonicalDepthAtLeast rho pathLength) : (combinedCanonicalEncoding formula bounded pathLength rho).1 = rho.refine (canonicalExtension formula pathLength rho)

On the bad event, combined encoding refines by the same canonical satisfying extension as the elementary encoder.

theorem Algebraic.AC0.Switching.decodeCombined_combinedCanonicalEncoding_of_deep {widthBound n : ℕ} [NeZero widthBound] (formula : DNF n) (bounded : formula.WidthAtMost widthBound) (pathLength : ℕ) (rho : PartialAssignment n) (deep : formula.CanonicalDepthAtLeast rho pathLength) : decodeCombined formula (combinedCanonicalEncoding formula bounded pathLength rho) = rho

The combined decoder recovers every bad-event restriction.

theorem Algebraic.AC0.Switching.combinedCanonicalEncoding_injectiveOn_deep {widthBound n : ℕ} [NeZero widthBound] (formula : DNF n) (bounded : formula.WidthAtMost widthBound) (pathLength : ℕ) (left : PartialAssignment n) : formula.CanonicalDepthAtLeast left pathLength → ∀ (right : PartialAssignment n), formula.CanonicalDepthAtLeast right pathLength → combinedCanonicalEncoding formula bounded pathLength left = combinedCanonicalEncoding formula bounded pathLength right → left = right

The combined encoder is injective on the canonical-depth bad event.

theorem Algebraic.AC0.Switching.card_combinedAdvice_cast_le_ennreal (width pathLength : ℕ) (widthPositive : 0 < width) : ↑(Fintype.card (CombinedAdvice width pathLength)) ≤ (↑(5 * width - 1) / 2) ^ pathLength

The combined-advice cardinality bound transferred to extended nonnegative reals for probability estimates.

theorem Algebraic.AC0.RandomRestriction.probability_canonicalDepthAtLeast_combined_card_scaled_le {widthBound n : ℕ} [NeZero widthBound] (formula : DNF n) (bounded : formula.WidthAtMost widthBound) (pathLength : ℕ) (p : NNReal) (atMostOne : p ≤ 1) : (↑(fixedWeight p) ^ pathLength * probability n p atMostOne fun (rho : PartialAssignment n) => formula.CanonicalDepthAtLeast rho pathLength) ≤ ↑(Fintype.card (Switching.CombinedAdvice widthBound pathLength)) * ↑p ^ pathLength

Exact weighted switching inequality before inserting the combined-advice cardinality estimate.

theorem Algebraic.AC0.RandomRestriction.probability_canonicalDepthAtLeast_combined_scaled_le {widthBound n : ℕ} [NeZero widthBound] (formula : DNF n) (bounded : formula.WidthAtMost widthBound) (pathLength : ℕ) (p : NNReal) (atMostOne : p ≤ 1) : (↑(fixedWeight p) ^ pathLength * probability n p atMostOne fun (rho : PartialAssignment n) => formula.CanonicalDepthAtLeast rho pathLength) ≤ (↑(5 * widthBound - 1) / 2) ^ pathLength * ↑p ^ pathLength

Exact positive-width scaled switching inequality with Beame's combined advice base ((5t - 1) / 2)^s.

theorem Algebraic.AC0.RandomRestriction.probability_canonicalDepthAtLeast_le_five_of_pos {widthBound n : ℕ} [NeZero widthBound] (formula : DNF n) (bounded : formula.WidthAtMost widthBound) (pathLength : ℕ) (p : NNReal) (atMostOne : p ≤ 1) : (probability n p atMostOne fun (rho : PartialAssignment n) => formula.CanonicalDepthAtLeast rho pathLength) ≤ (5 * ↑p * ↑widthBound) ^ pathLength

Positive-width canonical switching lemma with the standard 5pt base.

theorem Algebraic.AC0.RandomRestriction.probability_canonicalDepthAtLeast_le_five {n widthBound : ℕ} (formula : DNF n) (bounded : formula.WidthAtMost widthBound) (pathLength : ℕ) (p : NNReal) (atMostOne : p ≤ 1) : (probability n p atMostOne fun (rho : PartialAssignment n) => formula.CanonicalDepthAtLeast rho pathLength) ≤ (5 * ↑p * ↑widthBound) ^ pathLength

Canonical 5pt switching lemma, including width-zero DNFs.