Weighted encodings for switching arguments

The switching lemma is proved by injecting each bad random restriction into a more fully assigned restriction together with bounded finite advice. This module isolates the exact finite probability calculation behind that method.

Its principal statement is division-free. If every encoded restriction fixes exactly s formerly live variables, multiplying the bad-event probability by ((1 - p) / 2) ^ s is at most the number of advice strings times p ^ s. Later estimates may divide by the fixed-coordinate weight under an explicit positivity hypothesis. No asymptotics or search enter this layer.

theorem Algebraic.AC0.RandomRestriction.distribution_refine_cross_mul (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) (rho extension : PartialAssignment n) (fixesOnlyLive : extension.fixedVariables ⊆ rho.liveVariables) : ↑(fixedWeight p) ^ extension.fixedCount * (distribution n p atMostOne) rho = ↑p ^ extension.fixedCount * (distribution n p atMostOne) (rho.refine extension)

Fixing only previously live variables gives an exact, division-free point mass identity. Each newly fixed coordinate exchanges one factor of p for one factor of (1 - p) / 2.

theorem Algebraic.AC0.RandomRestriction.probability_scaled_le_of_injective_encoding (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) (event : PartialAssignment n → Prop) [DecidablePred event] (Advice : Type) [Fintype Advice] [DecidableEq Advice] (scale factor : ENNReal) (encode : PartialAssignment n → PartialAssignment n × Advice) (injectiveOnEvent : ∀ (left : PartialAssignment n), event left → ∀ (right : PartialAssignment n), event right → encode left = encode right → left = right) (massBound : ∀ (rho : PartialAssignment n), event rho → scale * (distribution n p atMostOne) rho ≤ factor * (distribution n p atMostOne) (encode rho).1) : scale * probability n p atMostOne event ≤ ↑(Fintype.card Advice) * factor

A weighted injection from an event into restrictions paired with finite advice bounds the scaled event probability by the advice cardinality times the output-side factor.

theorem Algebraic.AC0.RandomRestriction.probability_scaled_le_of_refinement_encoding (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) (event : PartialAssignment n → Prop) [DecidablePred event] (Advice : Type) [Fintype Advice] [DecidableEq Advice] (fixedCount : ℕ) (extension : PartialAssignment n → PartialAssignment n) (encode : PartialAssignment n → PartialAssignment n × Advice) (injectiveOnEvent : ∀ (left : PartialAssignment n), event left → ∀ (right : PartialAssignment n), event right → encode left = encode right → left = right) (output_eq : ∀ (rho : PartialAssignment n), event rho → (encode rho).1 = rho.refine (extension rho)) (fixesOnlyLive : ∀ (rho : PartialAssignment n), event rho → (extension rho).fixedVariables ⊆ rho.liveVariables) (extensionCount : ∀ (rho : PartialAssignment n), event rho → (extension rho).fixedCount = fixedCount) : ↑(fixedWeight p) ^ fixedCount * probability n p atMostOne event ≤ ↑(Fintype.card Advice) * ↑p ^ fixedCount

Exact encoding bound specialized to extensions that fix exactly fixedCount live variables. This is the probability engine used by the canonical switching-path encoding.