Arithmetic with heads: addition of ranks

A head holds an element of the universe, that is – through DescriptiveComplexity.orank – a number below Nat.card A. This file teaches a DescriptiveComplexity.HeadProgram to add two of them, which is the first of the fragments the inclusion AC⁰ ⊆ LOGSPACE needs: the numeric predicates of FirstOrder.Language.arith have to be decided by a machine whose guards are quantifier-free, and “these two heads are equal” is all such a guard can say.

The walk

DescriptiveComplexity.HeadProgram.plusP i j k a b mk decides orank (x i) + orank (x j) = orank (x k) with two scratch heads a, b and a marker head mk. It is a five-node control graph (DescriptiveComplexity.HeadProgram.PlusNode), every node a leafP or a moveP:

node	fragment	true →	false →
init	a := copy i, b := toMin, mk := toMax	test	test
test	b = j?	check	over
check	a = k?	exit true	exit false
over	a = mk?	exit false	step
step	a := succ a, b := succ b	test	test

so a runs up from x i while b counts up from the least element, and the answer is read off when b arrives at x j. The invariant is DescriptiveComplexity.HeadProgram.PlusBase: orank (x i) + orank (z b) = orank (z a), the counter is still below orank (x j), and the marker has not been passed.

Why the marker, and why the fragment parks it itself

“This head is at the greatest element” is not a quantifier-free fact of one head, while “these two heads are equal” is, so the overflow test compares a with a head parked at the maximum – the dmk idiom of DescriptiveComplexity.HeadCaptureDet. Overflow must exit false rather than die: a disabled succ transition is sound but not complete.

The marker is not an input the caller has to have parked, as in DescriptiveComplexity.HeadProgram.lexNextP: it is a third scratch head, sent to the greatest element by the fragment's own first move (HeadMove.toMax). That single choice is what makes the specification clean. A caller-supplied marker can sit anywhere, and the walk then has three regimes – exit false early, answer correctly, or run off the end with no exit at all – so its specification would have to be stated by the marker's value, as lexRel is. Parking it internally collapses all of that: the marker is the maximum, so a sum that does not fit is detected exactly when it does not fit, and a sum that does not fit is not the rank of anything either. What the fragment runs is therefore just DescriptiveComplexity.HeadProgram.Decides, with no side condition (DescriptiveComplexity.HeadProgram.decides_plusP).

Where the levels go

The control walk is assembled at protection level K – every head protected – because a fragment relation that mentions the scratch heads is not local at the caller's level, and DescriptiveComplexity.HeadProgram.runs_wireP needs locality. At level K locality is free (DescriptiveComplexity.HeadProgram.headLocal2_top), and the result is weakened to the caller's level afterwards, which is where the three scratch heads are forgotten.

Locality is free at the top

theorem DescriptiveComplexity.HeadProgram.headLocal2_top {K : ℕ} {A : Type} (R : (Fin K → A) → Bool → (Fin K → A) → Prop) : HeadLocal2 K R

Every relation is local at level K: there is no head beyond the last one to differ in. This is what lets a control walk over fragments that use scratch heads be assembled without any locality proof, the protection level being lowered only afterwards.

The control graph of an addition

inductive DescriptiveComplexity.HeadProgram.PlusNode : Type

The control nodes of an addition: initialize the two scratch heads, test whether the counter has arrived, read the answer off, test for overflow, step.

• init : PlusNode

  Copy the first summand onto a and send the counter b to the least element.

• test : PlusNode

  Has the counter reached the second summand?

• check : PlusNode

  It has: is a the claimed sum?

• over : PlusNode

  It has not: is a at the marker, i.e., would the next step overflow?

• step : PlusNode

  Step both scratch heads.

@[instance_reducible]

instance DescriptiveComplexity.HeadProgram.instDecidableEqPlusNode : DecidableEq PlusNode

Equations

• DescriptiveComplexity.HeadProgram.instDecidableEqPlusNode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.HeadProgram.instFinitePlusNode : Finite PlusNode

def DescriptiveComplexity.HeadProgram.plusWire : PlusNode → Bool → PlusNode ⊕ Bool

The wiring of an addition: the loop test → over → step → test, with the two answers hanging off check and the overflow answer off over.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.plusWire DescriptiveComplexity.HeadProgram.PlusNode.init x✝ = Sum.inl DescriptiveComplexity.HeadProgram.PlusNode.test
• DescriptiveComplexity.HeadProgram.plusWire DescriptiveComplexity.HeadProgram.PlusNode.check x✝ = Sum.inr x✝
• DescriptiveComplexity.HeadProgram.plusWire DescriptiveComplexity.HeadProgram.PlusNode.over x✝ = if x✝ = true then Sum.inr false else Sum.inl DescriptiveComplexity.HeadProgram.PlusNode.step
• DescriptiveComplexity.HeadProgram.plusWire DescriptiveComplexity.HeadProgram.PlusNode.step x✝ = Sum.inl DescriptiveComplexity.HeadProgram.PlusNode.test

noncomputable def DescriptiveComplexity.HeadProgram.plusInitMoves {K : ℕ} (i a b mk : Fin K) : Fin K → HeadMove K

The moves of the initialization: the running head copies the first summand, the counter goes to the least element, and the marker is parked at the greatest element – which is what makes the specification of the fragment clean.

Equations

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

noncomputable def DescriptiveComplexity.HeadProgram.plusStepMoves {K : ℕ} (a b : Fin K) : Fin K → HeadMove K

The moves of one step: both scratch heads advance.

Equations

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

noncomputable def DescriptiveComplexity.HeadProgram.plusFam {L : FirstOrder.Language} {K : ℕ} (i j k a b mk : Fin K) : PlusNode → HeadProgram L K

The fragments of an addition.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.plusFam i j k a b mk DescriptiveComplexity.HeadProgram.PlusNode.test = DescriptiveComplexity.HeadProgram.leafP (DescriptiveComplexity.HeadMove.eqVarF L b j) ⋯
• DescriptiveComplexity.HeadProgram.plusFam i j k a b mk DescriptiveComplexity.HeadProgram.PlusNode.check = DescriptiveComplexity.HeadProgram.leafP (DescriptiveComplexity.HeadMove.eqVarF L a k) ⋯
• DescriptiveComplexity.HeadProgram.plusFam i j k a b mk DescriptiveComplexity.HeadProgram.PlusNode.over = DescriptiveComplexity.HeadProgram.leafP (DescriptiveComplexity.HeadMove.eqVarF L a mk) ⋯

noncomputable def DescriptiveComplexity.HeadProgram.plusP {L : FirstOrder.Language} {K : ℕ} (i j k a b mk : Fin K) : HeadProgram L K

Addition: decide orank (x i) + orank (x j) = orank (x k), using the scratch heads a, b and a marker mk.

Equations

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

What the fragments run

noncomputable def DescriptiveComplexity.HeadProgram.plusFamRel {K : ℕ} {A : Type} [LinearOrder A] (i j k a b mk : Fin K) : PlusNode → (Fin K → A) → Bool → (Fin K → A) → Prop

The relations the fragments of an addition run, at the top protection level.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.plusFamRel i j k a b mk DescriptiveComplexity.HeadProgram.PlusNode.test = fun (x : Fin K → A) (c : Bool) (y : Fin K → A) => (c = true ↔ x b = x j) ∧ y = x
• DescriptiveComplexity.HeadProgram.plusFamRel i j k a b mk DescriptiveComplexity.HeadProgram.PlusNode.check = fun (x : Fin K → A) (c : Bool) (y : Fin K → A) => (c = true ↔ x a = x k) ∧ y = x
• DescriptiveComplexity.HeadProgram.plusFamRel i j k a b mk DescriptiveComplexity.HeadProgram.PlusNode.over = fun (x : Fin K → A) (c : Bool) (y : Fin K → A) => (c = true ↔ x a = x mk) ∧ y = x

theorem DescriptiveComplexity.HeadProgram.runs_eqLeafP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (u v : Fin K) : (leafP (HeadMove.eqVarF L u v) ⋯).Runs A K fun (x : Fin K → A) (c : Bool) (y : Fin K → A) => (c = true ↔ x u = x v) ∧ y = x

An equality test between two heads, as a fragment at the top protection level: it answers the equality and moves nothing.

theorem DescriptiveComplexity.HeadProgram.runs_plusFam {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (i j k a b mk : Fin K) (c : PlusNode) : (plusFam i j k a b mk c).Runs A K (plusFamRel i j k a b mk c)

The relation an addition runs

def DescriptiveComplexity.HeadProgram.PlusBase {K : ℕ} {A : Type} [LinearOrder A] (i j a b mk : Fin K) (x z : Fin K → A) : Prop

The invariant of the loop, at the nodes inside it: the running head is the first summand plus the counter, the counter has not passed the second summand, and the marker is parked at the greatest element. Nothing has to be said about the marker having been passed: a rank below the running head's is below the maximum.

Equations

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

def DescriptiveComplexity.HeadProgram.PlusInv {K : ℕ} {A : Type} [LinearOrder A] (i j a b mk : Fin K) (x : Fin K → A) : PlusNode → (Fin K → A) → Prop

The invariant of the control walk of an addition, node by node.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.PlusInv i j a b mk x DescriptiveComplexity.HeadProgram.PlusNode.init = fun (z : Fin K → A) => z = x
• DescriptiveComplexity.HeadProgram.PlusInv i j a b mk x DescriptiveComplexity.HeadProgram.PlusNode.test = fun (z : Fin K → A) => DescriptiveComplexity.HeadProgram.PlusBase i j a b mk x z
• DescriptiveComplexity.HeadProgram.PlusInv i j a b mk x DescriptiveComplexity.HeadProgram.PlusNode.over = fun (z : Fin K → A) => DescriptiveComplexity.HeadProgram.PlusBase i j a b mk x z ∧ z b ≠ x j
• DescriptiveComplexity.HeadProgram.PlusInv i j a b mk x DescriptiveComplexity.HeadProgram.PlusNode.step = fun (z : Fin K → A) => DescriptiveComplexity.HeadProgram.PlusBase i j a b mk x z ∧ z b ≠ x j

Soundness: the invariant of the control walk

structure DescriptiveComplexity.HeadProgram.PlusHeads {K : ℕ} (i j k a b mk : Fin K) (prot : ℕ) : Prop

The head indices a caller must respect: the four interface heads are protected, the two scratch heads are not.

• hi : ↑i < prot

  The first summand is protected.

• hj : ↑j < prot

  The second summand is protected.

• hk : ↑k < prot

  The claimed sum is protected.

• ha : prot ≤ ↑a

  The running head is scratch.

• hb : prot ≤ ↑b

  The counter is scratch.

• hmk : prot ≤ ↑mk

  The marker is scratch too: the fragment parks it itself.

• hab : a ≠ b

  The three scratch heads are distinct: being scratch does not make them so.

• hamk : a ≠ mk

  The running head is not the marker.

• hbmk : b ≠ mk

  The counter is not the marker.

theorem DescriptiveComplexity.HeadProgram.PlusHeads.imk {K : ℕ} {i j k a b mk : Fin K} {prot : ℕ} (h : PlusHeads i j k a b mk prot) : i ≠ mk

i and mk are distinct heads, being on opposite sides of the protection level.

theorem DescriptiveComplexity.HeadProgram.PlusHeads.ja {K : ℕ} {i j k a b mk : Fin K} {prot : ℕ} (h : PlusHeads i j k a b mk prot) : j ≠ a

j and a are distinct heads, being on opposite sides of the protection level.

theorem DescriptiveComplexity.HeadProgram.PlusHeads.jb {K : ℕ} {i j k a b mk : Fin K} {prot : ℕ} (h : PlusHeads i j k a b mk prot) : j ≠ b

j and b are distinct heads, being on opposite sides of the protection level.

theorem DescriptiveComplexity.HeadProgram.PlusHeads.jmk {K : ℕ} {i j k a b mk : Fin K} {prot : ℕ} (h : PlusHeads i j k a b mk prot) : j ≠ mk

j and mk are distinct heads, being on opposite sides of the protection level.

theorem DescriptiveComplexity.HeadProgram.PlusHeads.ka {K : ℕ} {i j k a b mk : Fin K} {prot : ℕ} (h : PlusHeads i j k a b mk prot) : k ≠ a

k and a are distinct heads, being on opposite sides of the protection level.

theorem DescriptiveComplexity.HeadProgram.PlusHeads.kb {K : ℕ} {i j k a b mk : Fin K} {prot : ℕ} (h : PlusHeads i j k a b mk prot) : k ≠ b

k and b are distinct heads, being on opposite sides of the protection level.

theorem DescriptiveComplexity.HeadProgram.PlusHeads.kmk {K : ℕ} {i j k a b mk : Fin K} {prot : ℕ} (h : PlusHeads i j k a b mk prot) : k ≠ mk

k and mk are distinct heads, being on opposite sides of the protection level.

theorem DescriptiveComplexity.HeadProgram.PlusHeads.ab {K : ℕ} {i j k a b mk : Fin K} {prot : ℕ} (h : PlusHeads i j k a b mk prot) : a ≠ b

The two arithmetic scratch heads are distinct, by fiat.

theorem DescriptiveComplexity.HeadProgram.PlusHeads.amk {K : ℕ} {i j k a b mk : Fin K} {prot : ℕ} (h : PlusHeads i j k a b mk prot) : a ≠ mk

The running head is not the marker, by fiat.

theorem DescriptiveComplexity.HeadProgram.PlusHeads.bmk {K : ℕ} {i j k a b mk : Fin K} {prot : ℕ} (h : PlusHeads i j k a b mk prot) : b ≠ mk

The counter is not the marker, by fiat.

theorem DescriptiveComplexity.HeadProgram.holds_plusInitMoves {K : ℕ} {A : Type} [LinearOrder A] {i j k a b mk : Fin K} {prot : ℕ} {x y : Fin K → A} (hh : PlusHeads i j k a b mk prot) (hmv : ∀ (h : Fin K), (plusInitMoves i a b mk h).Holds x h (y h)) : y a = x i ∧ (∀ (e : A), y b ≤ e) ∧ (∀ (e : A), e ≤ y mk) ∧ ∀ (p : Fin K), p ≠ a → p ≠ b → p ≠ mk → y p = x p

The moves of the initialization, read off: the running head, the counter, the marker, and everything else.

theorem DescriptiveComplexity.HeadProgram.holds_plusStepMoves {K : ℕ} {A : Type} [LinearOrder A] {i j k a b mk : Fin K} {prot : ℕ} {x y : Fin K → A} (hh : PlusHeads i j k a b mk prot) (hmv : ∀ (h : Fin K), (plusStepMoves a b h).Holds x h (y h)) : x a ⋖ y a ∧ x b ⋖ y b ∧ ∀ (p : Fin K), p ≠ a → p ≠ b → y p = x p

The moves of a step, read off.

theorem DescriptiveComplexity.HeadProgram.plusInv_of_walk {K : ℕ} {A : Type} [LinearOrder A] [Finite A] {i j k a b mk : Fin K} {prot : ℕ} (hh : PlusHeads i j k a b mk prot) (x : Fin K → A) (u : PlusNode × (Fin K → A)) : Relation.ReflTransGen (wireStep (plusFamRel i j k a b mk) plusWire) (PlusNode.init, x) u → PlusInv i j a b mk x u.1 u.2

The invariant holds all along the control walk: this is the whole soundness argument, the exits being read off it.

Completeness: building the walk

theorem DescriptiveComplexity.HeadProgram.exists_walk_test {K : ℕ} {A : Type} [LinearOrder A] [Finite A] {i j k a b mk : Fin K} {prot : ℕ} (hh : PlusHeads i j k a b mk prot) (x : Fin K → A) (t : ℕ) : t ≤ orank (x j) → orank (x i) + t < Nat.card A → ∃ (z : Fin K → A), Relation.ReflTransGen (wireStep (plusFamRel i j k a b mk) plusWire) (PlusNode.init, x) (PlusNode.test, z) ∧ (∀ (p : Fin K), p ≠ a → p ≠ b → p ≠ mk → z p = x p) ∧ orank (z a) = orank (x i) + t ∧ orank (z b) = t

The state after t iterations is reachable, as long as the counter has not passed the second summand and the running head still fits in the universe. No condition on the marker: the walk parks it itself, at the top, so it is reached exactly when the sum does not fit.

What an addition decides

theorem DescriptiveComplexity.HeadProgram.decides_plusP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {i j k a b mk : Fin K} {prot : ℕ} (hh : PlusHeads i j k a b mk prot) (hprotK : prot ≤ K) : (plusP i j k a b mk).Decides A prot fun (x : Fin K → A) => orank (x i) + orank (x j) = orank (x k)

The addition fragment decides the addition, with no side condition: it parks its own marker, so overflow is detected exactly where the sum leaves the universe, and a sum that leaves the universe is not the rank of the third head either.

theorem DescriptiveComplexity.HeadProgram.deterministic_plusP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (i j k a b mk : Fin K) : (plusP i j k a b mk).Deterministic A

The addition fragment is deterministic: every node of the control graph is, and DescriptiveComplexity.HeadProgram.wireP inherits it. This is what makes the assembled machine a deterministic automaton, hence FO(DTC) rather than merely FO(TC).

The control graph of a multiplication

inductive DescriptiveComplexity.HeadProgram.TimesNode : Type

The control nodes of a multiplication: an outer loop counting the rounds and, inside it, a scan looking for the element that carries the next partial product.

• init : TimesNode

  Send the accumulator and the round counter to the least element, and the scan's marker to the greatest.

• outer : TimesNode

  Has the round counter reached the second factor?

• final : TimesNode

  It has: is the accumulator the claimed product?

• scanInit : TimesNode

  It has not: start the scan at the least element.

• probe : TimesNode

  Does the candidate carry the accumulator plus the first factor?

• scanOver : TimesNode

  It does not: is the candidate at the marker, i.e., would the product overflow?

• scanStep : TimesNode

  Step the candidate.

• commit : TimesNode

  The candidate carries the next partial product: take it, and count the round.

@[instance_reducible]

instance DescriptiveComplexity.HeadProgram.instDecidableEqTimesNode : DecidableEq TimesNode

Equations

• DescriptiveComplexity.HeadProgram.instDecidableEqTimesNode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.HeadProgram.instFiniteTimesNode : Finite TimesNode

def DescriptiveComplexity.HeadProgram.timesWire : TimesNode → Bool → TimesNode ⊕ Bool

The wiring of a multiplication: the outer loop outer → scan → commit → outer, the scan probe → scanOver → scanStep → probe, and the two answers hanging off final and off the scan's overflow test.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.timesWire DescriptiveComplexity.HeadProgram.TimesNode.init x✝ = Sum.inl DescriptiveComplexity.HeadProgram.TimesNode.outer
• DescriptiveComplexity.HeadProgram.timesWire DescriptiveComplexity.HeadProgram.TimesNode.final x✝ = Sum.inr x✝
• DescriptiveComplexity.HeadProgram.timesWire DescriptiveComplexity.HeadProgram.TimesNode.scanInit x✝ = Sum.inl DescriptiveComplexity.HeadProgram.TimesNode.probe
• DescriptiveComplexity.HeadProgram.timesWire DescriptiveComplexity.HeadProgram.TimesNode.scanStep x✝ = Sum.inl DescriptiveComplexity.HeadProgram.TimesNode.probe
• DescriptiveComplexity.HeadProgram.timesWire DescriptiveComplexity.HeadProgram.TimesNode.commit x✝ = Sum.inl DescriptiveComplexity.HeadProgram.TimesNode.outer

noncomputable def DescriptiveComplexity.HeadProgram.timesInitMoves {K : ℕ} (acc cnt tmk : Fin K) : Fin K → HeadMove K

The moves that start a multiplication: accumulator and round counter to the least element, the scan's marker to the greatest.

Equations

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

noncomputable def DescriptiveComplexity.HeadProgram.timesScanInitMoves {K : ℕ} (cand : Fin K) : Fin K → HeadMove K

The move that starts a scan: the candidate to the least element.

Equations

• DescriptiveComplexity.HeadProgram.timesScanInitMoves cand h = if h = cand then DescriptiveComplexity.HeadMove.toMin else DescriptiveComplexity.HeadMove.stay

noncomputable def DescriptiveComplexity.HeadProgram.timesScanStepMoves {K : ℕ} (cand : Fin K) : Fin K → HeadMove K

The move of one scan step: the candidate advances.

Equations

• DescriptiveComplexity.HeadProgram.timesScanStepMoves cand h = if h = cand then DescriptiveComplexity.HeadMove.succ cand else DescriptiveComplexity.HeadMove.stay

noncomputable def DescriptiveComplexity.HeadProgram.timesCommitMoves {K : ℕ} (acc cnt cand : Fin K) : Fin K → HeadMove K

The moves that close a round: the accumulator takes the candidate's value and the round counter advances.

Equations

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

noncomputable def DescriptiveComplexity.HeadProgram.timesFam {L : FirstOrder.Language} {K : ℕ} (i j k acc cnt cand tmk a b mk : Fin K) : TimesNode → HeadProgram L K

The fragments of a multiplication. The probe node is a whole addition program (DescriptiveComplexity.HeadProgram.plusP), which is what makes the scan work: it asks whether the candidate carries the accumulator plus the first factor.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.timesFam i j k acc cnt cand tmk a b mk DescriptiveComplexity.HeadProgram.TimesNode.probe = DescriptiveComplexity.HeadProgram.plusP acc i cand a b mk

noncomputable def DescriptiveComplexity.HeadProgram.timesP {L : FirstOrder.Language} {K : ℕ} (i j k acc cnt cand tmk a b mk : Fin K) : HeadProgram L K

Multiplication: decide orank (x i) * orank (x j) = orank (x k), by adding the first factor to an accumulator once per round.

Equations

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

The head layout of a multiplication

structure DescriptiveComplexity.HeadProgram.TimesHeads {K : ℕ} (i j k acc cnt cand tmk a b mk : Fin K) (p m : ℕ) : Prop

The head indices a caller of a multiplication must respect. Three levels: the interface below p, the four working heads between p and m, and the addition's own three scratch heads at m and above – the last group being exactly what DescriptiveComplexity.HeadProgram.PlusHeads asks of the addition called at the probe node.

• hi : ↑i < p

  The first factor is interface.

• hj : ↑j < p

  The second factor is interface.

• hk : ↑k < p

  The claimed product is interface.

• hacc : p ≤ ↑acc

  The accumulator is a working head.

• hcnt : p ≤ ↑cnt ∧ ↑cnt < m

  The round counter is a working head.

• hcand : p ≤ ↑cand

  The scan's candidate is a working head.

• htmk : p ≤ ↑tmk ∧ ↑tmk < m

  The scan's marker is a working head.

• hplus : PlusHeads acc i cand a b mk m

  The addition at the probe node has the layout it needs, which also places acc, i and cand below m and a, b, mk at m or above.

• hac : acc ≠ cnt

  The accumulator is not the round counter.

• haca : acc ≠ cand

  The accumulator is not the candidate.

• hacm : acc ≠ tmk

  The accumulator is not the scan's marker.

• hcc : cnt ≠ cand

  The round counter is not the candidate.

• hcm : cnt ≠ tmk

  The round counter is not the scan's marker.

• hcam : cand ≠ tmk

  The candidate is not the scan's marker.

What the fragments of a multiplication run

noncomputable def DescriptiveComplexity.HeadProgram.timesFamRel {K : ℕ} {A : Type} [LinearOrder A] (i j k acc cnt cand tmk : Fin K) (m : ℕ) : TimesNode → (Fin K → A) → Bool → (Fin K → A) → Prop

The relations the fragments of a multiplication run, at the level m that protects the working heads and leaves the addition's scratch heads free.

Equations

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

theorem DescriptiveComplexity.HeadProgram.runs_timesFam {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {i j k acc cnt cand tmk a b mk : Fin K} {p m : ℕ} (hh : TimesHeads i j k acc cnt cand tmk a b mk p m) (hmK : m ≤ K) (c : TimesNode) : (timesFam i j k acc cnt cand tmk a b mk c).Runs A m (timesFamRel i j k acc cnt cand tmk m c)

theorem DescriptiveComplexity.HeadProgram.headLocal2_timesFamRel {K : ℕ} {A : Type} [LinearOrder A] {i j k acc cnt cand tmk a b mk : Fin K} {p m : ℕ} (hh : TimesHeads i j k acc cnt cand tmk a b mk p m) (c : TimesNode) : HeadLocal2 m (timesFamRel i j k acc cnt cand tmk m c)

theorem DescriptiveComplexity.HeadProgram.deterministic_timesP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (i j k acc cnt cand tmk a b mk : Fin K) : (timesP i j k acc cnt cand tmk a b mk).Deterministic A

A multiplication is deterministic: every node of its control graph is – the probe node because an addition is (DescriptiveComplexity.HeadProgram.deterministic_plusP).

The invariant of a multiplication

def DescriptiveComplexity.HeadProgram.TimesBase {K : ℕ} {A : Type} [LinearOrder A] (i j acc cnt cand tmk : Fin K) (m : ℕ) (x z : Fin K → A) : Prop

The invariant of both loops: the accumulator carries the first factor times the round counter, the round counter has not passed the second factor, the scan's marker is at the greatest element, and nothing else below m has moved.

Equations

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

def DescriptiveComplexity.HeadProgram.TimesInv {K : ℕ} {A : Type} [LinearOrder A] (i j acc cnt cand tmk : Fin K) (m : ℕ) (x : Fin K → A) : TimesNode → (Fin K → A) → Prop

The invariant of the control walk of a multiplication, node by node. Inside the scan it also records how far the candidate has got: below the target while the probe keeps failing, at it when the probe succeeds.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.TimesInv i j acc cnt cand tmk m x DescriptiveComplexity.HeadProgram.TimesNode.init = fun (z : Fin K → A) => z = x

theorem DescriptiveComplexity.HeadProgram.timesBase_headAgree {K : ℕ} {A : Type} {i j k acc cnt cand tmk a b mk : Fin K} {p m : ℕ} (hh : TimesHeads i j k acc cnt cand tmk a b mk p m) {x z : Fin K → A} (hz : ∀ (q : Fin K), ↑q < m → q ≠ acc → q ≠ cnt → q ≠ cand → q ≠ tmk → z q = x q) : HeadAgree p x z

The interface heads a multiplication must not disturb are below every working head.

theorem DescriptiveComplexity.HeadProgram.TimesBase.congr {K : ℕ} {A : Type} [LinearOrder A] {i j k acc cnt cand tmk a b mk : Fin K} {p m : ℕ} (hh : TimesHeads i j k acc cnt cand tmk a b mk p m) {x z z' : Fin K → A} (hb : TimesBase i j acc cnt cand tmk m x z) (hzz : HeadAgree m z z') : TimesBase i j acc cnt cand tmk m x z'

The invariant reads only the heads below m, so it survives a fragment that dirties the addition's scratch heads.

theorem DescriptiveComplexity.HeadProgram.holds_timesInitMoves {K : ℕ} {A : Type} [LinearOrder A] {i j k acc cnt cand tmk a b mk : Fin K} {p m : ℕ} (hh : TimesHeads i j k acc cnt cand tmk a b mk p m) {x y : Fin K → A} (hmv : ∀ (q : Fin K), ↑q < m → (timesInitMoves acc cnt tmk q).Holds x q (y q)) : (∀ (e : A), y acc ≤ e) ∧ (∀ (e : A), y cnt ≤ e) ∧ (∀ (e : A), e ≤ y tmk) ∧ ∀ (q : Fin K), ↑q < m → q ≠ acc → q ≠ cnt → q ≠ tmk → y q = x q

The moves that start a multiplication, read off.

theorem DescriptiveComplexity.HeadProgram.holds_timesScanInitMoves {K : ℕ} {A : Type} [LinearOrder A] {i j k acc cnt cand tmk a b mk : Fin K} {p m : ℕ} (hh : TimesHeads i j k acc cnt cand tmk a b mk p m) {x y : Fin K → A} (hmv : ∀ (q : Fin K), ↑q < m → (timesScanInitMoves cand q).Holds x q (y q)) : (∀ (e : A), y cand ≤ e) ∧ ∀ (q : Fin K), ↑q < m → q ≠ cand → y q = x q

The move that starts a scan, read off.

theorem DescriptiveComplexity.HeadProgram.holds_timesScanStepMoves {K : ℕ} {A : Type} [LinearOrder A] {i j k acc cnt cand tmk a b mk : Fin K} {p m : ℕ} (hh : TimesHeads i j k acc cnt cand tmk a b mk p m) {x y : Fin K → A} (hmv : ∀ (q : Fin K), ↑q < m → (timesScanStepMoves cand q).Holds x q (y q)) : x cand ⋖ y cand ∧ ∀ (q : Fin K), ↑q < m → q ≠ cand → y q = x q

The move of one scan step, read off.

theorem DescriptiveComplexity.HeadProgram.holds_timesCommitMoves {K : ℕ} {A : Type} [LinearOrder A] {i j k acc cnt cand tmk a b mk : Fin K} {p m : ℕ} (hh : TimesHeads i j k acc cnt cand tmk a b mk p m) {x y : Fin K → A} (hmv : ∀ (q : Fin K), ↑q < m → (timesCommitMoves acc cnt cand q).Holds x q (y q)) : y acc = x cand ∧ x cnt ⋖ y cnt ∧ ∀ (q : Fin K), ↑q < m → q ≠ acc → q ≠ cnt → y q = x q

The moves that close a round, read off.

theorem DescriptiveComplexity.HeadProgram.timesInv_of_walk {K : ℕ} {A : Type} [LinearOrder A] [Finite A] {i j k acc cnt cand tmk a b mk : Fin K} {p m : ℕ} (hh : TimesHeads i j k acc cnt cand tmk a b mk p m) (x : Fin K → A) (u : TimesNode × (Fin K → A)) : Relation.ReflTransGen (wireStep (timesFamRel i j k acc cnt cand tmk m) timesWire) (TimesNode.init, x) u → TimesInv i j acc cnt cand tmk m x u.1 u.2

The invariant holds all along the control walk of a multiplication.

Completeness: building the two walks

theorem DescriptiveComplexity.HeadProgram.exists_walk_probe {K : ℕ} {A : Type} [LinearOrder A] [Finite A] {i j k acc cnt cand tmk a b mk : Fin K} {p m : ℕ} (hh : TimesHeads i j k acc cnt cand tmk a b mk p m) (z₀ : Fin K → A) (hz₀ : orank (z₀ cand) = 0) (hmax : ∀ (e : A), e ≤ z₀ tmk) (t : ℕ) : t ≤ orank (z₀ acc) + orank (z₀ i) → t < Nat.card A → ∃ (z : Fin K → A), Relation.ReflTransGen (wireStep (timesFamRel i j k acc cnt cand tmk m) timesWire) (TimesNode.probe, z₀) (TimesNode.probe, z) ∧ (∀ (q : Fin K), ↑q < m → q ≠ cand → z q = z₀ q) ∧ orank (z cand) = t

The scan reaches every candidate up to its target: from the start of a scan, the walk can be continued until the candidate has any prescribed rank at most the target's, the probe failing at every earlier one.

theorem DescriptiveComplexity.HeadProgram.exists_walk_outer {K : ℕ} {A : Type} [LinearOrder A] [Finite A] {i j k acc cnt cand tmk a b mk : Fin K} {p m : ℕ} (hh : TimesHeads i j k acc cnt cand tmk a b mk p m) (x : Fin K → A) (r : ℕ) : r ≤ orank (x j) → orank (x i) * r < Nat.card A → ∃ (z : Fin K → A), Relation.ReflTransGen (wireStep (timesFamRel i j k acc cnt cand tmk m) timesWire) (TimesNode.init, x) (TimesNode.outer, z) ∧ (∀ (q : Fin K), ↑q < m → q ≠ acc → q ≠ cnt → q ≠ cand → q ≠ tmk → z q = x q) ∧ orank (z acc) = orank (x i) * r ∧ orank (z cnt) = r ∧ ∀ (e : A), e ≤ z tmk

The outer loop reaches every round whose partial product fits: the state after r rounds is reachable, the accumulator carrying orank (x i) * r.

What a multiplication decides

theorem DescriptiveComplexity.HeadProgram.decides_timesP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {i j k acc cnt cand tmk a b mk : Fin K} {p m : ℕ} (hh : TimesHeads i j k acc cnt cand tmk a b mk p m) (hmK : m ≤ K) : (timesP i j k acc cnt cand tmk a b mk).Decides A p fun (x : Fin K → A) => orank (x i) * orank (x j) = orank (x k)

The multiplication fragment decides the multiplication, with no side condition: the scan's marker is parked by the fragment itself, as the addition's is, so a product that leaves the universe is detected in the round where it does and is not the rank of the third head either.