The canonical DNF switching injection

This module packages the trace-level replay decoder into a single injection on the canonical-depth bad event. For each bad restriction, classical choice selects an exact-length path supplied by the structural depth theorem and the typed source-term trace proved for that path. This is proof-level witness selection, not enumeration or optimization.

The resulting encoder extends the bad restriction by the trace's satisfying assignment and stores one bounded position and two bits per path query. The explicit decoder is a left inverse, hence the encoder is injective on the bad event.

noncomputable def Algebraic.AC0.Switching.chosenPath {n : ℕ} (formula : DNF n) (rho : PartialAssignment n) (pathLength : ℕ) (deep : formula.CanonicalDepthAtLeast rho pathLength) : formula.CanonicalPath rho pathLength

A chosen exact-length canonical path witnessing the bad event.

Equations

• Algebraic.AC0.Switching.chosenPath formula rho pathLength deep = Classical.choice ⋯

noncomputable def Algebraic.AC0.Switching.chosenTrace {n : ℕ} (formula : DNF n) (rho : PartialAssignment n) (pathLength : ℕ) (deep : formula.CanonicalDepthAtLeast rho pathLength) : formula.CanonicalTrace rho (chosenPath formula rho pathLength deep).steps

The chosen source-term block trace carried by chosenPath.

Equations

• Algebraic.AC0.Switching.chosenTrace formula rho pathLength deep = Classical.choice ⋯

def Algebraic.AC0.Switching.defaultAdvice {widthBound : ℕ} [NeZero widthBound] (pathLength : ℕ) : Advice widthBound pathLength

A harmless total advice value used outside the bad event.

Equations

• Algebraic.AC0.Switching.defaultAdvice pathLength x✝ = { position := Fin.ofNat widthBound 0, closesBlock := false, difference := false }

noncomputable def Algebraic.AC0.Switching.canonicalExtension {n widthBound : ℕ} [NeZero widthBound] (formula : DNF n) (pathLength : ℕ) (rho : PartialAssignment n) : PartialAssignment n

Satisfying extension chosen for a bad restriction; the empty assignment is used outside the event to keep the probability encoder total.

Equations

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

noncomputable def Algebraic.AC0.Switching.canonicalEncoding {widthBound n : ℕ} [NeZero widthBound] (formula : DNF n) (pathLength : ℕ) (rho : PartialAssignment n) : PartialAssignment n × Advice widthBound pathLength

Total restriction/advice encoding used by the canonical switching injection.

Equations

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

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

On the bad event, the encoding output restriction is refinement by the chosen satisfying extension.

theorem Algebraic.AC0.Switching.canonicalExtension_fixedCount_of_deep {widthBound n : ℕ} [NeZero widthBound] (formula : DNF n) (pathLength : ℕ) (rho : PartialAssignment n) (deep : formula.CanonicalDepthAtLeast rho pathLength) : (canonicalExtension formula pathLength rho).fixedCount = pathLength

The chosen extension fixes exactly the requested path length.

theorem Algebraic.AC0.Switching.canonicalExtension_fixesOnlyLive_of_deep {widthBound n : ℕ} [NeZero widthBound] (formula : DNF n) (pathLength : ℕ) (rho : PartialAssignment n) (deep : formula.CanonicalDepthAtLeast rho pathLength) : (canonicalExtension formula pathLength rho).fixedVariables ⊆ rho.liveVariables

The chosen extension fixes only coordinates live in the bad restriction.

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

The explicit decoder recovers every restriction in the bad event from its chosen encoding.

theorem Algebraic.AC0.Switching.canonicalEncoding_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 → canonicalEncoding formula pathLength left = canonicalEncoding formula pathLength right → left = right

The canonical encoder is injective when restricted to the canonical-depth bad event.

theorem Algebraic.AC0.DNF.CanonicalTrace.steps_eq_nil_of_widthAtMost_zero {n : ℕ} {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) (bounded : formula.WidthAtMost 0) : steps = []

Under a width-zero hypothesis, every typed canonical trace has an empty query transcript.

theorem Algebraic.AC0.DNF.not_canonicalDepthAtLeast_of_widthAtMost_zero {n : ℕ} (formula : DNF n) (bounded : formula.WidthAtMost 0) (rho : PartialAssignment n) (pathLength : ℕ) (positive : 0 < pathLength) : ¬formula.CanonicalDepthAtLeast rho pathLength

A width-zero DNF cannot have positive canonical decision-tree depth under any restriction.

theorem Algebraic.AC0.RandomRestriction.probability_canonicalDepthAtLeast_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) ≤ ↑(4 * widthBound) ^ pathLength * ↑p ^ pathLength

Exact division-free canonical switching bound. The factor (4t)^s is the cardinality of one bounded position and two bits for each of the s path queries.

theorem Algebraic.AC0.RandomRestriction.four_ninths_le_fixedWeight (p : NNReal) (small : p ≤ 1 / 9) : 4 / 9 ≤ fixedWeight p

Under the standard small-p hypothesis, the probability of either fixed Boolean value is at least 4/9.

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

Standard 9pt corollary of the canonical switching injection. This is the weighted Razborov--Beame/Thapen constant obtained from one bounded position and two advice bits per query.

theorem Algebraic.AC0.RandomRestriction.probability_canonicalDepthAtLeast_eq_zero_of_widthAtMost_zero {n : ℕ} (formula : DNF n) (bounded : formula.WidthAtMost 0) (pathLength : ℕ) (positive : 0 < pathLength) (p : NNReal) (atMostOne : p ≤ 1) : (probability n p atMostOne fun (rho : PartialAssignment n) => formula.CanonicalDepthAtLeast rho pathLength) = 0

For a width-zero DNF and positive threshold, the canonical-depth event has probability zero.

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

Canonical 9pt switching bound, including width-zero DNFs.