What the control carries: contributions, not fold values

A design correction, found by writing the update rule down. The sweep's control cannot carry the fold values DescriptiveComplexity.foldFrom j v: at a step whose carry is c, the new value at a level j < c is the level's own contribution combined with the deeper value – and the contribution is not recoverable from the two old values (x = C ∨ y does not determine C). What is closed under the update is the family of contributions themselves:

• DescriptiveComplexity.Draw.accCVal j v – the completed-subtree contribution at level j: the disjunction (existential polarity) or conjunction (universal) over the values strictly below the current coordinate;
• DescriptiveComplexity.Draw.foldFrom_eq_accCVal – the fold value at a level is the contribution combined with the deeper fold value, so any fold value is a finite Boolean chain of the contributions and the current leaf (DescriptiveComplexity.foldFrom_last), which a rule's guard can spell out;
• the three update rules along an increment with carry c: DescriptiveComplexity.Draw.accCVal_congr_above (levels before the carry are untouched), DescriptiveComplexity.Draw.accCVal_carry (the carry level absorbs the completed subtree, which is the deeper chain at the old valuation), and DescriptiveComplexity.Draw.accCVal_reset (levels after the carry reset to the polarity's unit).

So the machine's payload holds one bit per level – the contribution – plus the last leaf, and every verdict it ever needs is a chain of those bits.

noncomputable def DescriptiveComplexity.Draw.accCVal {A : Type} {n : ℕ} (pol : ℕ → Bool) (P : (Fin n → A) → Prop) (le : A → A → Prop) (j : ℕ) (v : Fin n → A) : Prop

The completed-subtree contribution at a level: what the enumeration has finished below the current coordinate – a disjunction of subtrees under an existential polarity, a conjunction under a universal one. Past the last level it is the polarity's unit.

Equations

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

theorem DescriptiveComplexity.Draw.accCVal_of_lt {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {j : ℕ} (h : j < n) (hp : pol j = true) (v : Fin n → A) : accCVal pol P le j v ↔ ∃ (a : A), WMLt le a (v ⟨j, h⟩) ∧ altQuantFrom pol P (j + 1) (Function.update v ⟨j, h⟩ a)

theorem DescriptiveComplexity.Draw.accCVal_of_lt_all {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {j : ℕ} (h : j < n) (hp : pol j = false) (v : Fin n → A) : accCVal pol P le j v ↔ ∀ (a : A), WMLt le a (v ⟨j, h⟩) → altQuantFrom pol P (j + 1) (Function.update v ⟨j, h⟩ a)

theorem DescriptiveComplexity.Draw.foldFrom_eq_accCVal {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {j : ℕ} (h : j < n) (v : Fin n → A) : foldFrom pol P le j v ↔ if pol j = true then accCVal pol P le j v ∨ foldFrom pol P le (j + 1) v else accCVal pol P le j v ∧ foldFrom pol P le (j + 1) v

The fold value is the contribution combined with the deeper value – DescriptiveComplexity.foldFrom_ex / foldFrom_all read through the contribution. Iterated down to DescriptiveComplexity.foldFrom_last, any fold value is a finite Boolean chain of the contributions and the leaf.

The three update rules along an increment

theorem DescriptiveComplexity.Draw.accCVal_congr_above {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {v v' : Fin n → A} {j : ℕ} (h : j < n) (hagree : ∀ (i : Fin n), ↑i ≤ j → v i = v' i) : accCVal pol P le j v' ↔ accCVal pol P le j v

Levels before the carry are untouched: their coordinate and everything above it agree across the step.

theorem DescriptiveComplexity.Draw.accCVal_reset {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {v' : Fin n → A} {j : ℕ} (h : j < n) (hbot : ∀ (a : A), le (v' ⟨j, h⟩) a) : accCVal pol P le j v' ↔ pol j = false

Levels after the carry reset to the polarity's unit: nothing lies strictly below a minimal coordinate.

theorem DescriptiveComplexity.Draw.accCVal_carry {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} (h : IsLinOrd le) {v v' : Fin n → A} {c : ℕ} (hc : c < n) (hagree : ∀ (i : Fin n), ↑i < c → v i = v' i) (htop : ∀ (i : Fin n), c < ↑i → ∀ (a : A), le a (v i)) (hsucc : ∀ (a : A), WMLt le a (v' ⟨c, hc⟩) ↔ le a (v ⟨c, hc⟩)) : accCVal pol P le c v' ↔ if pol c = true then accCVal pol P le c v ∨ foldFrom pol P le (c + 1) v else accCVal pol P le c v ∧ foldFrom pol P le (c + 1) v

The carry level absorbs the completed subtree: the new contribution is the old one together with the deeper fold value at the old valuation – which the machine has as a chain of its stored bits and the old leaf.

The vector the control carries, and its update

What the machine holds is one bit per level – the contribution – plus the value of the last leaf. Two operations turn that into everything it needs: a fold value is the chain of the stored bits from a level down, closed by the leaf (DescriptiveComplexity.Draw.chainFrom, correct by chainFrom_iff_foldFrom), and one round of the enumeration rewrites the vector by the three rules above (accCVal_step: untouched before the carry, absorbing at it, reset after it). A rule's dstSt spells out the first and its guard the second; nothing else about the fold ever reaches the program.

def DescriptiveComplexity.Draw.chainAux (pol : ℕ → Bool) (acc : ℕ → Prop) (leaf : Prop) (n : ℕ) : ℕ → ℕ → Prop

The chain, with an explicit fuel so that the recursion is structural.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Draw.chainAux pol acc leaf n 0 x✝ = leaf

def DescriptiveComplexity.Draw.chainFrom (pol : ℕ → Bool) (acc : ℕ → Prop) (leaf : Prop) (n j : ℕ) : Prop

A fold value as the machine holds it: the chain of the stored contributions from a level down, closed by the last leaf.

Equations

• DescriptiveComplexity.Draw.chainFrom pol acc leaf n j = DescriptiveComplexity.Draw.chainAux pol acc leaf n (n - j) j

theorem DescriptiveComplexity.Draw.chainFrom_of_le {n : ℕ} {pol : ℕ → Bool} {acc : ℕ → Prop} {leaf : Prop} {j : ℕ} (h : n ≤ j) : chainFrom pol acc leaf n j = leaf

theorem DescriptiveComplexity.Draw.chainFrom_succ {n : ℕ} {pol : ℕ → Bool} {acc : ℕ → Prop} {leaf : Prop} {j : ℕ} (h : j < n) : chainFrom pol acc leaf n j = if pol j = true then acc j ∨ chainFrom pol acc leaf n (j + 1) else acc j ∧ chainFrom pol acc leaf n (j + 1)

theorem DescriptiveComplexity.Draw.chainFrom_iff_foldFrom {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {acc : ℕ → Prop} {leaf : Prop} {v : Fin n → A} (hacc : ∀ i < n, acc i ↔ accCVal pol P le i v) (hleaf : leaf ↔ P v) (j : ℕ) : chainFrom pol acc leaf n j ↔ foldFrom pol P le j v

The chain is the fold value: a control whose bits are the contributions and whose leaf bit is the matrix at the current valuation reads off every accumulator of the sweep.

theorem DescriptiveComplexity.Draw.accCVal_step {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {acc acc' : ℕ → Prop} {leaf : Prop} (h : IsLinOrd le) {v v' : Fin n → A} {c : ℕ} (hc : c < n) (hagree : ∀ (i : Fin n), ↑i < c → v i = v' i) (htop : ∀ (i : Fin n), c < ↑i → ∀ (a : A), le a (v i)) (hbot : ∀ (i : Fin n), c < ↑i → ∀ (a : A), le (v' i) a) (hsucc : ∀ (a : A), WMLt le a (v' ⟨c, hc⟩) ↔ le a (v ⟨c, hc⟩)) (hacc : ∀ i < n, acc i ↔ accCVal pol P le i v) (hleaf : leaf ↔ P v) (hnew : ∀ i < n, acc' i ↔ if i < c then acc i else if i = c then if pol c = true then acc c ∨ chainFrom pol acc leaf n (c + 1) else acc c ∧ chainFrom pol acc leaf n (c + 1) else pol i = false) (i : ℕ) (hi : i < n) : acc' i ↔ accCVal pol P le i v'

One round of the enumeration rewrites the vector: the levels before the carry keep their bit, the carry level absorbs the chain below it at the old valuation, and the levels after it reset to the polarity's unit. This is the whole content of the dstSt a landing rule carries.

theorem DescriptiveComplexity.Draw.accCVal_bot {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {v : Fin n → A} (hbot : ∀ (i : Fin n) (a : A), le (v i) a) (i : ℕ) : accCVal pol P le i v ↔ pol i = false

At the first valuation every accumulator is the polarity's unit: nothing lies below a minimal coordinate, so a cleared register starts the sweep.