Documentation

DescriptiveComplexity.HeadBit

The bit of a rank, as a head program #

The fragment DescriptiveComplexity.HeadProgram.bitP: a deterministic multi-head program deciding BIT, that is, whether the bit of the rank of one head at the index given by the rank of another is set. It is what lets the multi-head automaton of DescriptiveComplexity.HeadEvalArith evaluate the bit-level logic of DescriptiveComplexity.LogTime – the third arithmetic fragment, beside DescriptiveComplexity.HeadProgram.plusP and DescriptiveComplexity.HeadProgram.timesP.

The algorithm: halve, then read the parity #

BIT(x, i) is (x / 2 ^ i) % 2 = 1, so the program halves the value i times and then asks for its parity. Both loops are the shape this development already uses: an outer loop counting the rounds, and inside it a scan that walks a candidate up the order asking, at each stop, whether the candidate is the half of the current value. That question is two additions, so the scan's probe is an addition fragment – a decider made to compute, exactly as timesP's scan reuses plusP.

The half of v is the c with c + c = v (v even) or c + (c + 1) = v (v odd), and the two are tested in that order at each candidate, so the scan stops at the first c that works and that c is v / 2 whatever the parity. The successor c + 1 is not an addition but a head: the program moves w to the successor of the candidate, which is why the overflow test comes before that move – a successor move at the greatest element is disabled, and the walk would be stuck rather than wrong.

The parity, and why it needs no guard #

After the last round the value is x / 2 ^ i, and its parity is read by a second scan: v is even exactly when some c has c + c = v, and such a c is v / 2 ≤ v, so the scan finds it if it exists. The scan therefore answers false at the first candidate that halves v, and true when it reaches the marker having found none. No test against zero is needed anywhere, which is what makes the two scans the same four nodes with different exits.

What the fragment costs #

Five working heads – the value, the round counter, the scan's candidate, the successor w, and the scan's marker – above the interface, and the addition's own three scratch heads above those; the marker is parked by the fragment itself, as plusP's is, so a caller has no discipline to keep beyond the head layout DescriptiveComplexity.HeadProgram.BitHeads. The clock is O(log n) rounds of a scan, hence O(n log n) steps – irrelevant to the space bound, which is the number of heads.

The control graph of a bit #

source
inductive DescriptiveComplexity.HeadProgram.BitNode :
Type

The control nodes of a bit: an outer loop counting the halvings, a scan looking for the half of the current value, and a second scan reading the parity of the value the outer loop leaves.

  • init : BitNode

    Copy the value onto the working head, the round counter to the least element and the scan's marker to the greatest.

  • outer : BitNode

    Has the round counter reached the index?

  • scanInit : BitNode

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

  • probeE : BitNode

    Is the candidate twice itself the value, that is, is the value even with this half?

  • scanOver : BitNode

    It is not: is the candidate at the marker, i.e., is the scan over?

  • mkW : BitNode

    It is not: put w on the successor of the candidate.

  • probeO : BitNode

    Is the candidate plus its successor the value, that is, is the value odd with this half?

  • scanStep : BitNode

    Step the candidate.

  • commit : BitNode

    The candidate is the half: take it, and count the round.

  • parInit : BitNode

    The rounds are over: start the parity scan.

  • parProbe : BitNode

    Does the candidate halve the value, that is, is the value even?

  • parOver : BitNode

    It does not: is the parity scan over?

  • parStep : BitNode

    Step the parity scan's candidate.

Instances For
    Dependency graph
    source
    @[instance_reducible]
    instance DescriptiveComplexity.HeadProgram.instDecidableEqBitNode :
    DecidableEq BitNode
    Equations
    Dependency graph
    source
    instance DescriptiveComplexity.HeadProgram.instFiniteBitNode :
    Finite BitNode
    Dependency graph
    source
    def DescriptiveComplexity.HeadProgram.bitWire :
    BitNode → Bool → BitNode ⊕ Bool

    The wiring of a bit: the outer loop outer → scan → commit → outer, the scan probeE → scanOver → mkW → probeO → scanStep → probeE, and the parity scan parProbe → parOver → parStep → parProbe carrying the two answers.

    Equations
    Instances For
      Dependency graph
      source
      noncomputable def DescriptiveComplexity.HeadProgram.bitInitMoves {K : ℕ} (xh y cnt tmk : Fin K) :
      Fin K → HeadMove K

      The moves that start a bit: the working head copies the value, the round counter goes to the least element, and the scan's marker is parked at the greatest.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Dependency graph
        source
        noncomputable def DescriptiveComplexity.HeadProgram.bitScanInitMoves {K : ℕ} (cand : Fin K) :
        Fin K → HeadMove K

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

        Equations
        Instances For
          Dependency graph
          source
          noncomputable def DescriptiveComplexity.HeadProgram.bitStepMoves {K : ℕ} (cand : Fin K) :
          Fin K → HeadMove K

          The move of one scan step: the candidate advances.

          Equations
          Instances For
            Dependency graph
            source
            noncomputable def DescriptiveComplexity.HeadProgram.bitWMoves {K : ℕ} (cand w : Fin K) :
            Fin K → HeadMove K

            The move that prepares the odd probe: w takes the successor of the candidate. It is guarded by the overflow test, a successor move at the greatest element being disabled.

            Equations
            Instances For
              Dependency graph
              source
              noncomputable def DescriptiveComplexity.HeadProgram.bitCommitMoves {K : ℕ} (y cnt cand : Fin K) :
              Fin K → HeadMove K

              The moves that close a round: the working head takes the half the scan found, and the round counter advances.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Dependency graph
                source
                noncomputable def DescriptiveComplexity.HeadProgram.bitFam {L : FirstOrder.Language} {K : ℕ} (ih xh y cnt cand w tmk a b mk : Fin K) :
                BitNode → HeadProgram L K

                The fragments of a bit. The two probes are addition programs (DescriptiveComplexity.HeadProgram.plusP): probeE asks whether the candidate doubles to the value, probeO whether the candidate plus its successor does.

                Equations
                Instances For
                  Dependency graph
                  source
                  noncomputable def DescriptiveComplexity.HeadProgram.bitP {L : FirstOrder.Language} {K : ℕ} (ih xh y cnt cand w tmk a b mk : Fin K) :
                  HeadProgram L K

                  The bit: decide whether the bit of orank (x xh) at the index orank (x ih) is set, by halving the value orank (x ih) times and reading the parity of what is left.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Dependency graph

                    The head layout of a bit #

                    source
                    structure DescriptiveComplexity.HeadProgram.BitHeads {K : ℕ} (ih xh y cnt cand w tmk a b mk : Fin K) (p S m : ℕ) :
                    Prop

                    The head indices a caller of a bit must respect. The two interface heads are below the caller's level p, the five working heads occupy S to S + 4 for some S ≥ p, and the addition's three scratch heads sit at m = S + 5 – so that every distinctness the construction needs is an arithmetic fact rather than a hypothesis.

                    • hih : ↑ih < p

                      The index is interface.

                    • hxh : ↑xh < p

                      The value is interface.

                    • hpS : p ≤ S

                      The caller's level is below the fragment's scratch.

                    • hy : ↑y = S

                      The working value sits at S.

                    • hcnt : ↑cnt = S + 1

                      The round counter sits at S + 1.

                    • hcand : ↑cand = S + 2

                      The scan's candidate sits at S + 2.

                    • hw : ↑w = S + 3

                      The candidate's successor sits at S + 3.

                    • htmk : ↑tmk = S + 4

                      The scan's marker sits at S + 4.

                    • hm : m = S + 5

                      The working heads end where the addition's scratch begins.

                    • ha : ↑a = m

                      The addition's running head sits at m.

                    • hb : ↑b = m + 1

                      The addition's counter sits at m + 1.

                    • hmk : ↑mk = m + 2

                      The addition's marker sits at m + 2.

                    Instances For
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.lt_m_y {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      ↑y < m
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.lt_m_cnt {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      ↑cnt < m
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.lt_m_cand {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      ↑cand < m
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.lt_m_w {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      ↑w < m
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.lt_m_tmk {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      ↑tmk < m
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.lt_m_ih {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      ↑ih < m
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.lt_m_xh {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      ↑xh < m
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.le_pm {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      p ≤ m
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.plusE {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      PlusHeads cand cand y a b mk m

                      The even probe has the head layout an addition asks for.

                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.plusO {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      PlusHeads cand w y a b mk m

                      The odd probe has it too.

                      Dependency graph

                      The distinctness of the working heads, read off their positions #

                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.ne_y_cnt {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      y ≠ cnt
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.ne_y_cand {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      y ≠ cand
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.ne_y_w {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      y ≠ w
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.ne_y_tmk {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      y ≠ tmk
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.ne_cnt_cand {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      cnt ≠ cand
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.ne_cnt_w {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      cnt ≠ w
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.ne_cnt_tmk {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      cnt ≠ tmk
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.ne_cand_w {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      cand ≠ w
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.ne_cand_tmk {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      cand ≠ tmk
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.ne_w_tmk {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) :
                      w ≠ tmk
                      Dependency graph
                      source
                      theorem DescriptiveComplexity.HeadProgram.BitHeads.ne_int {K : ℕ} {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (h : BitHeads ih xh y cnt cand w tmk a b mk p S m) {q : Fin K} (hq : ↑q < p) :
                      q ≠ y ∧ q ≠ cnt ∧ q ≠ cand ∧ q ≠ w ∧ q ≠ tmk

                      An interface head is none of the working ones.

                      Dependency graph

                      What the fragments of a bit run #

                      source
                      noncomputable def DescriptiveComplexity.HeadProgram.bitFamRel {K : ℕ} {A : Type} [LinearOrder A] (ih xh y cnt cand w tmk : Fin K) (m : ℕ) :
                      BitNode → (Fin K → A) → Bool → (Fin K → A) → Prop

                      The relations the fragments of a bit 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.
                      Instances For
                        Dependency graph
                        source
                        theorem DescriptiveComplexity.HeadProgram.runs_bitFam {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (hh : BitHeads ih xh y cnt cand w tmk a b mk p S m) (hmK : m ≤ K) (c : BitNode) :
                        (bitFam ih xh y cnt cand w tmk a b mk c).Runs A m (bitFamRel ih xh y cnt cand w tmk m c)
                        Dependency graph
                        source
                        theorem DescriptiveComplexity.HeadProgram.headLocal2_bitFamRel {K : ℕ} {A : Type} [LinearOrder A] {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (hh : BitHeads ih xh y cnt cand w tmk a b mk p S m) (c : BitNode) :
                        HeadLocal2 m (bitFamRel ih xh y cnt cand w tmk m c)
                        Dependency graph
                        source
                        theorem DescriptiveComplexity.HeadProgram.deterministic_bitP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (ih xh y cnt cand w tmk a b mk : Fin K) :
                        (bitP ih xh y cnt cand w tmk a b mk).Deterministic A

                        A bit is deterministic: every node of its control graph is – the two probes because an addition is.

                        Dependency graph

                        The invariant of the control walk #

                        source
                        def DescriptiveComplexity.HeadProgram.BitBase {K : ℕ} {A : Type} [LinearOrder A] (ih xh y cnt cand w tmk : Fin K) (m : ℕ) (x z : Fin K → A) :
                        Prop

                        The invariant of both loops: the working head carries the value halved once per round counted, the counter has not passed the index, the marker is parked at the greatest element, and nothing else below the protection level has moved.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Dependency graph
                          source
                          def DescriptiveComplexity.HeadProgram.NoHalf {K : ℕ} {A : Type} [LinearOrder A] (y cand : Fin K) (z : Fin K → A) :
                          Prop

                          The invariant of the halving scan: no candidate below the current one is the half of the value, on either parity.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Dependency graph
                            source
                            def DescriptiveComplexity.HeadProgram.NoEven {K : ℕ} {A : Type} [LinearOrder A] (y cand : Fin K) (z : Fin K → A) :
                            Prop

                            The invariant of the parity scan: no candidate below the current one halves the value.

                            Equations
                            Instances For
                              Dependency graph
                              source
                              def DescriptiveComplexity.HeadProgram.BitInv {K : ℕ} {A : Type} [LinearOrder A] (ih xh y cnt cand w tmk : Fin K) (m : ℕ) (x : Fin K → A) :
                              BitNode → (Fin K → A) → Prop

                              The invariant of the control walk of a bit, node by node.

                              Equations
                              Instances For
                                Dependency graph
                                source
                                theorem DescriptiveComplexity.HeadProgram.NoHalf.congr {K : ℕ} {A : Type} [LinearOrder A] {y cand : Fin K} {z z' : Fin K → A} (h : NoHalf y cand z) (hy : z' y = z y) (hc : z' cand = z cand) :
                                NoHalf y cand z'

                                The scan invariants only look at the value and the candidate.

                                Dependency graph
                                source
                                theorem DescriptiveComplexity.HeadProgram.NoEven.congr {K : ℕ} {A : Type} [LinearOrder A] {y cand : Fin K} {z z' : Fin K → A} (h : NoEven y cand z) (hy : z' y = z y) (hc : z' cand = z cand) :
                                NoEven y cand z'
                                Dependency graph
                                source
                                theorem DescriptiveComplexity.HeadProgram.BitBase.int {K : ℕ} {A : Type} [LinearOrder A] {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (hh : BitHeads ih xh y cnt cand w tmk a b mk p S m) {x z : Fin K → A} (hb : BitBase ih xh y cnt cand w tmk m x z) {q : Fin K} (hq : ↑q < p) :
                                z q = x q

                                The interface heads are untouched all along the walk.

                                Dependency graph
                                source
                                theorem DescriptiveComplexity.HeadProgram.BitBase.congr {K : ℕ} {A : Type} [LinearOrder A] {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} {x z z' : Fin K → A} (hh : BitHeads ih xh y cnt cand w tmk a b mk p S m) (hb : BitBase ih xh y cnt cand w tmk m x z) (hz : HeadAgree m z z') :
                                BitBase ih xh y cnt cand w tmk m x z'

                                The invariant survives a fragment that moves nothing below the protection level.

                                Dependency graph

                                Reading the moves #

                                source
                                theorem DescriptiveComplexity.HeadProgram.holds_bitInitMoves {K : ℕ} {A : Type} [LinearOrder A] {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} {x z : Fin K → A} (hh : BitHeads ih xh y cnt cand w tmk a b mk p S m) (hmv : ∀ (q : Fin K), ↑q < m → (bitInitMoves xh y cnt tmk q).Holds x q (z q)) :
                                z y = x xh ∧ (∀ (e : A), z cnt ≤ e) ∧ (∀ (e : A), e ≤ z tmk) ∧ ∀ (q : Fin K), ↑q < m → q ≠ y → q ≠ cnt → q ≠ tmk → z q = x q
                                Dependency graph
                                source
                                theorem DescriptiveComplexity.HeadProgram.holds_bitScanInitMoves {K : ℕ} {A : Type} [LinearOrder A] {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} {x z : Fin K → A} (hh : BitHeads ih xh y cnt cand w tmk a b mk p S m) (hmv : ∀ (q : Fin K), ↑q < m → (bitScanInitMoves cand q).Holds x q (z q)) :
                                (∀ (e : A), z cand ≤ e) ∧ ∀ (q : Fin K), ↑q < m → q ≠ cand → z q = x q
                                Dependency graph
                                source
                                theorem DescriptiveComplexity.HeadProgram.holds_bitStepMoves {K : ℕ} {A : Type} [LinearOrder A] {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} {x z : Fin K → A} (hh : BitHeads ih xh y cnt cand w tmk a b mk p S m) (hmv : ∀ (q : Fin K), ↑q < m → (bitStepMoves cand q).Holds x q (z q)) :
                                x cand ⋖ z cand ∧ ∀ (q : Fin K), ↑q < m → q ≠ cand → z q = x q
                                Dependency graph
                                source
                                theorem DescriptiveComplexity.HeadProgram.holds_bitWMoves {K : ℕ} {A : Type} [LinearOrder A] {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} {x z : Fin K → A} (hh : BitHeads ih xh y cnt cand w tmk a b mk p S m) (hmv : ∀ (q : Fin K), ↑q < m → (bitWMoves cand w q).Holds x q (z q)) :
                                x cand ⋖ z w ∧ ∀ (q : Fin K), ↑q < m → q ≠ w → z q = x q
                                Dependency graph
                                source
                                theorem DescriptiveComplexity.HeadProgram.holds_bitCommitMoves {K : ℕ} {A : Type} [LinearOrder A] {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} {x z : Fin K → A} (hh : BitHeads ih xh y cnt cand w tmk a b mk p S m) (hmv : ∀ (q : Fin K), ↑q < m → (bitCommitMoves y cnt cand q).Holds x q (z q)) :
                                z y = x cand ∧ x cnt ⋖ z cnt ∧ ∀ (q : Fin K), ↑q < m → q ≠ y → q ≠ cnt → z q = x q
                                Dependency graph

                                Soundness: the invariant of the control walk #

                                source
                                theorem DescriptiveComplexity.HeadProgram.bitInv_of_walk {K : ℕ} {A : Type} [LinearOrder A] [Finite A] {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (hh : BitHeads ih xh y cnt cand w tmk a b mk p S m) (x : Fin K → A) (u : BitNode × (Fin K → A)) :
                                Relation.ReflTransGen (wireStep (bitFamRel ih xh y cnt cand w tmk m) bitWire) (BitNode.init, x) u → BitInv ih xh y cnt cand w tmk m x u.1 u.2

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

                                Dependency graph

                                Completeness: building the walks #

                                source
                                theorem DescriptiveComplexity.HeadProgram.walk_scan_step {K : ℕ} {A : Type} [LinearOrder A] [Finite A] {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (hh : BitHeads ih xh y cnt cand w tmk a b mk p S m) {z : Fin K → A} (hlt : orank (z cand) + orank (z cand) + 1 < orank (z y)) (htop : ∀ (e : A), e ≤ z tmk) :
                                ∃ (z' : Fin K → A), DescriptiveComplexity.HeadProgram.BWalk✝ ih xh y cnt cand w tmk m (BitNode.probeE, z) (BitNode.probeE, z') ∧ orank (z' cand) = orank (z cand) + 1 ∧ ∀ (q : Fin K), ↑q < m → q ≠ cand → q ≠ w → z' q = z q

                                One turn of the halving scan: a candidate strictly below the half is rejected by both probes, so the scan steps on.

                                Dependency graph
                                source
                                theorem DescriptiveComplexity.HeadProgram.walk_scan {K : ℕ} {A : Type} [LinearOrder A] [Finite A] {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (hh : BitHeads ih xh y cnt cand w tmk a b mk p S m) {z : Fin K → A} (hmin : ∀ (e : A), z cand ≤ e) (htop : ∀ (e : A), e ≤ z tmk) (t : ℕ) :
                                t ≤ orank (z y) / 2 → ∃ (z' : Fin K → A), DescriptiveComplexity.HeadProgram.BWalk✝ ih xh y cnt cand w tmk m (BitNode.probeE, z) (BitNode.probeE, z') ∧ orank (z' cand) = t ∧ ∀ (q : Fin K), ↑q < m → q ≠ cand → q ≠ w → z' q = z q

                                The halving scan reaches the half: the candidate walks up to v / 2, every earlier candidate being rejected.

                                Dependency graph
                                source
                                theorem DescriptiveComplexity.HeadProgram.walk_commit {K : ℕ} {A : Type} [LinearOrder A] [Finite A] {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (hh : BitHeads ih xh y cnt cand w tmk a b mk p S m) {z : Fin K → A} (hcandh : orank (z cand) = orank (z y) / 2) (htop : ∀ (e : A), e ≤ z tmk) :
                                ∃ (z' : Fin K → A), DescriptiveComplexity.HeadProgram.BWalk✝ ih xh y cnt cand w tmk m (BitNode.probeE, z) (BitNode.commit, z') ∧ ∀ (q : Fin K), ↑q < m → q ≠ w → z' q = z q

                                The scan commits: at the half, one of the two probes succeeds and the round is closed.

                                Dependency graph
                                source
                                theorem DescriptiveComplexity.HeadProgram.walk_outer {K : ℕ} {A : Type} [LinearOrder A] [Finite A] {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (hh : BitHeads ih xh y cnt cand w tmk a b mk p S m) (x : Fin K → A) (t : ℕ) :
                                t ≤ orank (x ih) → ∃ (z : Fin K → A), DescriptiveComplexity.HeadProgram.BWalk✝ ih xh y cnt cand w tmk m (BitNode.init, x) (BitNode.outer, z) ∧ orank (z cnt) = t ∧ orank (z y) = orank (x xh) / 2 ^ t ∧ (∀ (e : A), e ≤ z tmk) ∧ ∀ (q : Fin K), ↑q < m → q ≠ y → q ≠ cnt → q ≠ cand → q ≠ w → q ≠ tmk → z q = x q

                                The outer loop runs: after t rounds the working head carries the value halved t times, and the counter has counted them.

                                Dependency graph
                                source
                                theorem DescriptiveComplexity.HeadProgram.walk_par_step {K : ℕ} {A : Type} [LinearOrder A] [Finite A] {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (_hh : BitHeads ih xh y cnt cand w tmk a b mk p S m) {z : Fin K → A} (hprobe : orank (z cand) + orank (z cand) ≠ orank (z y)) (hlt : orank (z cand) < orank (z tmk)) :
                                ∃ (z' : Fin K → A), DescriptiveComplexity.HeadProgram.BWalk✝ ih xh y cnt cand w tmk m (BitNode.parProbe, z) (BitNode.parProbe, z') ∧ orank (z' cand) = orank (z cand) + 1 ∧ ∀ (q : Fin K), ↑q < m → q ≠ cand → z' q = z q

                                One turn of the parity scan: a candidate that does not halve the value, and is not at the marker, steps on.

                                Dependency graph
                                source
                                theorem DescriptiveComplexity.HeadProgram.walk_par {K : ℕ} {A : Type} [LinearOrder A] [Finite A] {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (hh : BitHeads ih xh y cnt cand w tmk a b mk p S m) {z : Fin K → A} (hmin : ∀ (e : A), z cand ≤ e) (t : ℕ) :
                                t ≤ orank (z tmk) → (∀ d < t, d + d ≠ orank (z y)) → ∃ (z' : Fin K → A), DescriptiveComplexity.HeadProgram.BWalk✝ ih xh y cnt cand w tmk m (BitNode.parProbe, z) (BitNode.parProbe, z') ∧ orank (z' cand) = t ∧ ∀ (q : Fin K), ↑q < m → q ≠ cand → z' q = z q

                                The parity scan walks: as long as no candidate below has halved the value, the scan reaches every index up to the marker.

                                Dependency graph

                                What a bit decides #

                                source
                                theorem DescriptiveComplexity.HeadProgram.decides_bitP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {ih xh y cnt cand w tmk a b mk : Fin K} {p S m : ℕ} (hh : BitHeads ih xh y cnt cand w tmk a b mk p S m) (hmK : m ≤ K) :
                                (bitP ih xh y cnt cand w tmk a b mk).Decides A p fun (x : Fin K → A) => (orank (x xh)).testBit (orank (x ih)) = true

                                The bit fragment decides the bit, with no side condition: the marker is parked by the fragment itself, the halvings are exact, and the parity scan is exhaustive.

                                Dependency graph