Canonical switching-path advice

This module turns a typed canonical DNF path trace into the local data used by the switching-lemma injection. Each query is annotated with

• its position in the selected source term,
• whether it closes the current term block,
• whether the original path bit differs from the satisfying literal value, and
• the value satisfying that source literal.

Only the first three fields become finite advice. The queried coordinate and satisfying value remain internal witnesses used to define the output restriction and prove reconstruction. No paths or circuits are enumerated.

def Algebraic.AC0.LiteralSet.satisfyingValue {n : ℕ} (set : LiteralSet n) (index : Fin n) : Bool

Deterministic Boolean value extracted from a literal requirement. On the support of the literal set this is its unique satisfying value.

Equations

• set.satisfyingValue index = (set.requirements index).getD false

structure Algebraic.AC0.Switching.QueryAdvice (widthBound : ℕ) : Type

One symbol of switching advice. The position names a variable within the currently selected source term.

• position : Fin widthBound

  Zero-based position in the selected source term's ordered support.

• closesBlock : Bool

  Whether this query is the last one in the current source-term block.

• difference : Bool

  Whether the path bit differs from the selected literal's satisfying value.

def Algebraic.AC0.Switching.instDecidableEqQueryAdvice.decEq {widthBound✝ : ℕ} (x✝ x✝¹ : QueryAdvice widthBound✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Algebraic.AC0.Switching.instDecidableEqQueryAdvice {widthBound✝ : ℕ} : DecidableEq (QueryAdvice widthBound✝)

Equations

• Algebraic.AC0.Switching.instDecidableEqQueryAdvice = Algebraic.AC0.Switching.instDecidableEqQueryAdvice.decEq

@[instance_reducible]

instance Algebraic.AC0.Switching.instFintypeQueryAdvice {widthBound✝ : ℕ} : Fintype (QueryAdvice widthBound✝)

Equations

• Algebraic.AC0.Switching.instFintypeQueryAdvice = Fintype.ofEquiv ((_ : Fin widthBound✝) × (_ : Bool) × Bool) (Algebraic.AC0.Switching.QueryAdvice.proxyTypeEquiv widthBound✝)

def Algebraic.AC0.Switching.QueryAdvice.decodeValue {widthBound : ℕ} (advice : QueryAdvice widthBound) (satisfyingValue : Bool) : Bool

Recover the original path bit from its value relative to the selected literal's satisfying value.

Equations

• advice.decodeValue satisfyingValue = (satisfyingValue ^^ advice.difference)

@[simp]

theorem Algebraic.AC0.Switching.QueryAdvice.decodeValue_mk_xor {widthBound : ℕ} (position : Fin widthBound) (closesBlock satisfyingValue pathValue : Bool) : { position := position, closesBlock := closesBlock, difference := satisfyingValue ^^ pathValue }.decodeValue satisfyingValue = pathValue

Encoding a path bit by its difference from the satisfying value and then decoding it recovers that path bit.

@[reducible, inline]

abbrev Algebraic.AC0.Switching.Advice (widthBound pathLength : ℕ) : Type

Fixed-length switching advice.

Equations

• Algebraic.AC0.Switching.Advice widthBound pathLength = (Fin pathLength → Algebraic.AC0.Switching.QueryAdvice widthBound)

structure Algebraic.AC0.Switching.QueryRecord (n widthBound : ℕ) : Type

Internal annotation of one canonical query. The source term, coordinate, and satisfying value are deliberately not part of the finite advice.

• term : Term n

  Source term selected for this block.

• index : Fin n

  Coordinate queried at this step.

• satisfyingValue : Bool

  Value that satisfies the source literal at index.

• advice : QueryAdvice widthBound

  Finite symbol retained by the switching encoding.

@[instance_reducible]

instance Algebraic.AC0.Switching.instDecidableEqQueryRecord {n✝ widthBound✝ : ℕ} : DecidableEq (QueryRecord n✝ widthBound✝)

Equations

• Algebraic.AC0.Switching.instDecidableEqQueryRecord = Algebraic.AC0.Switching.instDecidableEqQueryRecord.decEq

def Algebraic.AC0.Switching.instDecidableEqQueryRecord.decEq {n✝ widthBound✝ : ℕ} (x✝ x✝¹ : QueryRecord n✝ widthBound✝) : Decidable (x✝ = x✝¹)

Equations

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

def Algebraic.AC0.Switching.QueryRecord.WellFormed {n widthBound : ℕ} (record : QueryRecord n widthBound) : Prop

The two local facts needed to decode an internal query record: its hidden value satisfies the named literal, and its public position selects the hidden coordinate from the source term.

Equations

• record.WellFormed = (record.term.requirements record.index = some record.satisfyingValue ∧ (Algebraic.AC0.LiteralSet.orderedSupport record.term)[↑record.advice.position]? = some record.index)

def Algebraic.AC0.Switching.QueryRecord.satisfyingStep {n widthBound : ℕ} (record : QueryRecord n widthBound) : DecisionTree.PathStep n

The internal query record's satisfying assignment step.

Equations

• record.satisfyingStep = { index := record.index, value := record.satisfyingValue }

def Algebraic.AC0.Switching.QueryRecord.toAdvice {n widthBound : ℕ} (record : QueryRecord n widthBound) : QueryAdvice widthBound

Forget the internal fields of a query record.

Equations

• record.toAdvice = record.advice

def Algebraic.AC0.Switching.QueryAdvice.equivProduct (widthBound : ℕ) : QueryAdvice widthBound ≃ Fin widthBound × Bool × Bool

Query advice is exactly a bounded position and two bits.

Equations

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

theorem Algebraic.AC0.Switching.card_queryAdvice (widthBound : ℕ) : Fintype.card (QueryAdvice widthBound) = 4 * widthBound

There are exactly 4 * widthBound possible symbols per query.

theorem Algebraic.AC0.Switching.card_advice (widthBound pathLength : ℕ) : Fintype.card (Advice widthBound pathLength) = (4 * widthBound) ^ pathLength

Fixed-length advice has the exact cardinality used by the weighted switching calculation.

def Algebraic.AC0.Switching.listToFn {α : Type u_1} (values : List α) {length : ℕ} (length_eq : values.length = length) : Fin length → α

Reindex a list of known length as a fixed finite function.

Equations

• Algebraic.AC0.Switching.listToFn values length_eq index = values.get (Fin.cast ⋯ index)

theorem Algebraic.AC0.Switching.ofFn_listToFn {α : Type u_1} (values : List α) {length : ℕ} (length_eq : values.length = length) : List.ofFn (listToFn values length_eq) = values

Reindexing a list and then listing the function loses no information.

def Algebraic.AC0.Switching.selectTerm {n : ℕ} (formula : DNF n) (state : PartialAssignment n) : Option (Term n) → Option (Term n)

Choose the source term currently being decoded. A term is retained inside a block; at a block boundary the canonical first-surviving selector is run on the replay state.

Equations

• Algebraic.AC0.Switching.selectTerm formula state (some term) = some term
• Algebraic.AC0.Switching.selectTerm formula state none = formula.firstSurviving state

def Algebraic.AC0.Switching.replayIndices {n widthBound : ℕ} (formula : DNF n) : PartialAssignment n → Option (Term n) → List (QueryAdvice widthBound) → List (Fin n)

Replay switching advice and recover its queried coordinates. Malformed advice is handled totally by returning the successfully decoded prefix.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.AC0.Switching.replayIndices formula x✝¹ x✝ [] = []

def Algebraic.AC0.Switching.decode {n widthBound pathLength : ℕ} (formula : DNF n) (encoded : PartialAssignment n × Advice widthBound pathLength) : PartialAssignment n

Decode an encoded restriction/advice pair by replaying its coordinates and clearing them from the refined restriction.

Equations

• Algebraic.AC0.Switching.decode formula encoded = encoded.1.clear (Algebraic.AC0.Switching.replayIndices formula encoded.1 none (List.ofFn encoded.2)).toFinset

theorem Algebraic.AC0.Switching.replayIndices_none_eq_some_of_firstSurviving {n widthBound : ℕ} (formula : DNF n) (state : PartialAssignment n) (term : Term n) (found : formula.firstSurviving state = some term) (advice : List (QueryAdvice widthBound)) : replayIndices formula state none advice = replayIndices formula state (some term) advice

If the canonical selector returns term, replay from a block boundary is the same as replay with term already selected.

def Algebraic.AC0.LiteralSet.sourcePosition {widthBound n : ℕ} [NeZero widthBound] (set : LiteralSet n) (index : Fin n) : Fin widthBound

Position of a coordinate in a source term, reduced into the declared width bound. Valid traced queries are proved below to lie below the bound, so the reduction does not change their position.

Equations

• set.sourcePosition index = Fin.ofNat widthBound (List.idxOf index set.orderedSupport)

theorem Algebraic.AC0.LiteralSet.requirements_satisfyingValue_of_mem_support {n : ℕ} (set : LiteralSet n) (index : Fin n) (present : index ∈ set.support) : set.requirements index = some (set.satisfyingValue index)

A support coordinate's extracted Boolean value is its literal's required value.

theorem Algebraic.AC0.LiteralSet.length_orderedSupport {n : ℕ} (set : LiteralSet n) : set.orderedSupport.length = set.width

The ordered support lists each support coordinate exactly once, so its length is the literal-set width.

theorem Algebraic.AC0.LiteralSet.sourcePosition_val_of_mem_support {widthBound n : ℕ} [NeZero widthBound] (set : LiteralSet n) (index : Fin n) (bounded : set.width ≤ widthBound) (present : index ∈ set.support) : ↑(set.sourcePosition index) = List.idxOf index set.orderedSupport

For a valid bounded term coordinate, reduction modulo the width bound is inert.

theorem Algebraic.AC0.LiteralSet.getElem?_sourcePosition_of_mem_support {widthBound n : ℕ} [NeZero widthBound] (set : LiteralSet n) (index : Fin n) (bounded : set.width ≤ widthBound) (present : index ∈ set.support) : set.orderedSupport[↑(set.sourcePosition index)]? = some index

Decoding a valid bounded source position recovers its coordinate.

theorem Algebraic.AC0.LiteralSet.not_conflicts_refine_fix_satisfying {n : ℕ} (set : LiteralSet n) (rho : PartialAssignment n) (index : Fin n) (noConflict : ¬set.ConflictsWith rho) (live : rho index = none) (present : index ∈ set.support) : ¬set.ConflictsWith (rho.refine (PartialAssignment.fix index (set.satisfyingValue index)))

Assigning a live support coordinate its satisfying value preserves nonconflict with the literal set.

theorem Algebraic.AC0.LiteralSet.not_conflicts_refine_of_liveSupport_eq_nil {n : ℕ} (set : LiteralSet n) (rho extension : PartialAssignment n) (noConflict : ¬set.ConflictsWith rho) (supportEmpty : DNF.liveSupport set rho = []) : ¬set.ConflictsWith (rho.refine extension)

Once a nonconflicting literal set has no live support, no later refinement can create a conflict with it.

theorem Algebraic.AC0.LiteralSet.not_conflicts_refine_of_satisfying_on_liveSupport {n : ℕ} (set : LiteralSet n) (rho extension : PartialAssignment n) (noConflict : ¬set.ConflictsWith rho) (compatible : ∀ index ∈ DNF.liveSupport set rho, extension index = none ∨ extension index = some (set.satisfyingValue index)) : ¬set.ConflictsWith (rho.refine extension)

A refinement cannot falsify a nonconflicting literal set when every value it adds on the set's live support is either absent or the satisfying value.

theorem Algebraic.AC0.DNF.liveSupport_refine_fix_eq_tail {n : ℕ} (term : Term n) (rho : PartialAssignment n) (index : Fin n) (rest : List (Fin n)) (value : Bool) (support_eq : liveSupport term rho = index :: rest) : liveSupport term (rho.refine (PartialAssignment.fix index value)) = rest

Fixing the head of a live-support list removes exactly that coordinate.

def Algebraic.AC0.DNF.CanonicalTrace.queryRecords {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) : List (Switching.QueryRecord n widthBound)

Annotate all queries in a canonical trace.

Equations

• (Algebraic.AC0.DNF.CanonicalTrace.nil rho).queryRecords = []
• (Algebraic.AC0.DNF.CanonicalTrace.start found support_eq nonempty block).queryRecords = block.queryRecords

def Algebraic.AC0.DNF.CanonicalBlockTrace.queryRecords {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) : List (Switching.QueryRecord n widthBound)

Annotate the queries remaining in one canonical source-term block.

Equations

• One or more equations did not get rendered due to their size.
• (Algebraic.AC0.DNF.CanonicalBlockTrace.nil rho index rest).queryRecords = []

def Algebraic.AC0.DNF.CanonicalTrace.satisfyingSteps {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) : List (DecisionTree.PathStep n)

The satisfying query transcript underlying the output assignment.

Equations

• trace.satisfyingSteps = List.map Algebraic.AC0.Switching.QueryRecord.satisfyingStep trace.queryRecords

def Algebraic.AC0.DNF.CanonicalBlockTrace.satisfyingSteps {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) : List (DecisionTree.PathStep n)

Satisfying transcript for the remaining queries of one source-term block.

Equations

• trace.satisfyingSteps = List.map Algebraic.AC0.Switching.QueryRecord.satisfyingStep trace.queryRecords

def Algebraic.AC0.DNF.CanonicalTrace.satisfyingAssignment {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) : PartialAssignment n

Satisfying assignment placed into the injection's output restriction.

Equations

• trace.satisfyingAssignment = Algebraic.AC0.DecisionTree.PathStep.assignment trace.satisfyingSteps

def Algebraic.AC0.DNF.CanonicalBlockTrace.satisfyingAssignment {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) : PartialAssignment n

Satisfying assignment for the remaining queries of one source-term block.

Equations

• trace.satisfyingAssignment = Algebraic.AC0.DecisionTree.PathStep.assignment trace.satisfyingSteps

def Algebraic.AC0.DNF.CanonicalTrace.adviceList {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) : List (Switching.QueryAdvice widthBound)

Variable-length advice before it is reindexed by the prescribed path length.

Equations

• trace.adviceList = List.map Algebraic.AC0.Switching.QueryRecord.toAdvice trace.queryRecords

def Algebraic.AC0.DNF.CanonicalBlockTrace.adviceList {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) : List (Switching.QueryAdvice widthBound)

Variable-length advice for the remaining queries in one source-term block.

Equations

• trace.adviceList = List.map Algebraic.AC0.Switching.QueryRecord.toAdvice trace.queryRecords

@[simp]

theorem Algebraic.AC0.DNF.CanonicalTrace.satisfyingAssignment_start {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {term : Term n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (found : formula.firstSurviving rho = some term) (support_eq : liveSupport term rho = indices) (nonempty : indices ≠ []) (block : formula.CanonicalBlockTrace term rho indices steps) : (start found support_eq nonempty block).satisfyingAssignment = block.satisfyingAssignment

@[simp]

theorem Algebraic.AC0.DNF.CanonicalTrace.adviceList_start {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {term : Term n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (found : formula.firstSurviving rho = some term) (support_eq : liveSupport term rho = indices) (nonempty : indices ≠ []) (block : formula.CanonicalBlockTrace term rho indices steps) : (start found support_eq nonempty block).adviceList = block.adviceList

@[simp]

theorem Algebraic.AC0.DNF.CanonicalBlockTrace.satisfyingAssignment_takeMore {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {index next : Fin n} {rest : List (Fin n)} {value : Bool} {steps : List (DecisionTree.PathStep n)} (tail : formula.CanonicalBlockTrace term (rho.refine (PartialAssignment.fix index value)) (next :: rest) steps) : tail.takeMore.satisfyingAssignment = (PartialAssignment.fix index (LiteralSet.satisfyingValue term index)).refine tail.satisfyingAssignment

@[simp]

theorem Algebraic.AC0.DNF.CanonicalBlockTrace.adviceList_takeMore {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {index next : Fin n} {rest : List (Fin n)} {value : Bool} {steps : List (DecisionTree.PathStep n)} (tail : formula.CanonicalBlockTrace term (rho.refine (PartialAssignment.fix index value)) (next :: rest) steps) : tail.takeMore.adviceList = { position := LiteralSet.sourcePosition term index, closesBlock := false, difference := LiteralSet.satisfyingValue term index ^^ value } :: tail.adviceList

@[simp]

theorem Algebraic.AC0.DNF.CanonicalBlockTrace.satisfyingAssignment_takeLast {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {index : Fin n} {value : Bool} {steps : List (DecisionTree.PathStep n)} (tail : formula.CanonicalTrace (rho.refine (PartialAssignment.fix index value)) steps) : (takeLast tail).satisfyingAssignment = (PartialAssignment.fix index (LiteralSet.satisfyingValue term index)).refine tail.satisfyingAssignment

@[simp]

theorem Algebraic.AC0.DNF.CanonicalBlockTrace.adviceList_takeLast {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {index : Fin n} {value : Bool} {steps : List (DecisionTree.PathStep n)} (tail : formula.CanonicalTrace (rho.refine (PartialAssignment.fix index value)) steps) : (takeLast tail).adviceList = { position := LiteralSet.sourcePosition term index, closesBlock := true, difference := LiteralSet.satisfyingValue term index ^^ value } :: tail.adviceList

theorem Algebraic.AC0.DNF.CanonicalTrace.queryRecords_indices {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) : List.map Switching.QueryRecord.index trace.queryRecords = DecisionTree.PathStep.indices steps

Query-record coordinates agree exactly with the original path coordinates.

theorem Algebraic.AC0.DNF.CanonicalBlockTrace.queryRecords_indices {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) : List.map Switching.QueryRecord.index trace.queryRecords = DecisionTree.PathStep.indices steps

The same coordinate agreement while traversing a source-term block.

theorem Algebraic.AC0.DNF.CanonicalTrace.queryRecords_wellFormed {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) (bounded : formula.WidthAtMost widthBound) (record : Switching.QueryRecord n widthBound) : record ∈ trace.queryRecords → record.WellFormed

Every record extracted from a width-bounded canonical trace carries a genuine satisfying literal value and a correctly decodable source position.

theorem Algebraic.AC0.DNF.CanonicalBlockTrace.queryRecords_wellFormed {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) (bounded : formula.WidthAtMost widthBound) (termBound : LiteralSet.width term ≤ widthBound) (supported : ∀ index ∈ indices, index ∈ LiteralSet.support term) (record : Switching.QueryRecord n widthBound) : record ∈ trace.queryRecords → record.WellFormed

The record invariant while traversing one source-term block.

theorem Algebraic.AC0.DNF.CanonicalTrace.satisfyingSteps_indices {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) : DecisionTree.PathStep.indices trace.satisfyingSteps = DecisionTree.PathStep.indices steps

The satisfying transcript queries precisely the original path's coordinates, changing only their Boolean values.

theorem Algebraic.AC0.DNF.CanonicalTrace.satisfyingAssignment_fixedVariables {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) : trace.satisfyingAssignment.fixedVariables = (DecisionTree.PathStep.assignment steps).fixedVariables

The satisfying assignment fixes the same coordinates as the original path assignment.

theorem Algebraic.AC0.DNF.CanonicalTrace.length_adviceList {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) : trace.adviceList.length = steps.length

Variable-length advice has one symbol per original path query.

def Algebraic.AC0.DNF.CanonicalTrace.advice {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} {pathLength : ℕ} (trace : formula.CanonicalTrace rho steps) (length_eq : steps.length = pathLength) : Switching.Advice widthBound pathLength

Fixed-length advice associated to a trace whose path has the prescribed length.

Equations

• trace.advice length_eq = Algebraic.AC0.Switching.listToFn trace.adviceList ⋯

theorem Algebraic.AC0.DNF.CanonicalTrace.ofFn_advice {widthBound n : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} {pathLength : ℕ} (trace : formula.CanonicalTrace rho steps) (length_eq : steps.length = pathLength) : List.ofFn (trace.advice length_eq) = trace.adviceList

Listing fixed-length trace advice recovers the original advice list.

theorem Algebraic.AC0.DNF.CanonicalBlockTrace.satisfyingAssignment_compatible {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) (nodup : indices.Nodup) (index : Fin n) : index ∈ indices → trace.satisfyingAssignment index = none ∨ trace.satisfyingAssignment index = some (LiteralSet.satisfyingValue term index)

On every pending coordinate, a block's satisfying assignment either leaves the variable live or assigns the selected term's satisfying value.

theorem Algebraic.AC0.DNF.CanonicalBlockTrace.not_conflicts_refine_satisfyingAssignment {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) (support_eq : liveSupport term rho = indices) (noConflict : ¬LiteralSet.ConflictsWith term rho) : ¬LiteralSet.ConflictsWith term (rho.refine trace.satisfyingAssignment)

Satisfying all queries remaining in one source-term block never falsifies that term. The invariant support_eq says precisely which of its source coordinates are still live at the current state.

theorem Algebraic.AC0.DNF.CanonicalTrace.not_conflicts_refine_satisfyingAssignment {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) {term : Term n} (found : formula.firstSurviving rho = some term) : ¬LiteralSet.ConflictsWith term (rho.refine trace.satisfyingAssignment)

A source term surviving at the start of a canonical trace still survives after the trace's satisfying assignment is added.

theorem Algebraic.AC0.DNF.CanonicalTrace.firstSurviving_refine_satisfyingAssignment {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) {term : Term n} (found : formula.firstSurviving rho = some term) : formula.firstSurviving (rho.refine trace.satisfyingAssignment) = some term

The first-surviving source-term selector is unchanged when the satisfying assignment extracted from the trace is added. This is the selector equation used by the reconstruction decoder.

theorem Algebraic.AC0.DNF.CanonicalTrace.replayIndices_satisfyingAssignment {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalTrace rho steps) (bounded : formula.WidthAtMost widthBound) : Switching.replayIndices formula (rho.refine trace.satisfyingAssignment) none trace.adviceList = DecisionTree.PathStep.indices steps

Replaying the advice extracted from a satisfying canonical trace recovers the original path's query coordinates exactly.

theorem Algebraic.AC0.DNF.CanonicalBlockTrace.replayIndices_satisfyingAssignment {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {term : Term n} {rho : PartialAssignment n} {indices : List (Fin n)} {steps : List (DecisionTree.PathStep n)} (trace : formula.CanonicalBlockTrace term rho indices steps) (bounded : formula.WidthAtMost widthBound) (termBound : LiteralSet.width term ≤ widthBound) (support_eq : liveSupport term rho = indices) : Switching.replayIndices formula (rho.refine trace.satisfyingAssignment) (some term) trace.adviceList = DecisionTree.PathStep.indices steps

The replay invariant inside one selected source-term block.

theorem Algebraic.AC0.DNF.CanonicalPath.satisfyingAssignment_fixedCount {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {pathLength : ℕ} (path : formula.CanonicalPath rho pathLength) (trace : formula.CanonicalTrace rho path.steps) : trace.satisfyingAssignment.fixedCount = pathLength

A traced satisfying assignment fixes exactly the prescribed canonical path length.

theorem Algebraic.AC0.DNF.CanonicalPath.satisfyingAssignment_fixesOnlyLive {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {pathLength : ℕ} (path : formula.CanonicalPath rho pathLength) (trace : formula.CanonicalTrace rho path.steps) : trace.satisfyingAssignment.fixedVariables ⊆ rho.liveVariables

A traced satisfying assignment fixes only variables live before the path began.

theorem Algebraic.AC0.DNF.CanonicalPath.decode_satisfyingEncoding {n widthBound : ℕ} [NeZero widthBound] {formula : DNF n} {rho : PartialAssignment n} {pathLength : ℕ} (path : formula.CanonicalPath rho pathLength) (trace : formula.CanonicalTrace rho path.steps) (bounded : formula.WidthAtMost widthBound) : Switching.decode formula (rho.refine trace.satisfyingAssignment, trace.advice ⋯) = rho

The explicit replay-and-clear decoder is a left inverse of every valid canonical trace encoding.