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.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