Kits for the round trips: the file test

The kit wrapping the file-test round trip, by the template of DescriptiveComplexity.Problems.Wide.DrawKit: a phase inductive, a rule inductive with concrete guards, the rules function at a phase embedding, an in-shape separation lemma, and a discharge – any program whose rule set contains the kit's rules satisfies the composite's run theorem (DescriptiveComplexity.Draw.TestKit.reaches_pos/_neg: scan up to the file top, bounce, one question per register on the way down, verdict in the phase, return to the marker).

The verdict phases double as return phases, which is where the cell-coupled forms of the layer earn their keep: the walking rule of the passing phase is guarded rg ≠ one ∧ wk ≠ one, disjoint from the register rules, and the coupled hypotheses of DescriptiveComplexity.Draw.Prog.reaches_fileRoundTrip are exactly what shows it fires wherever the composite needs it. The failing phase hosts no register rule, so its single rule takes the disjunction rg = one ∨ wk ≠ one and serves hold, walk and return at once.

Rules are owned by their source phase: how a program enters the kit (at the scan phase, off the marker) and how it leaves the two verdict phases (at the marker, guarded wk = one ∧ rg ≠ one, disjoint from every rule here) is the caller's business.

The file test's shapes

inductive DescriptiveComplexity.Draw.TestPh : Type

The phases of a test trip: the up-scan, the bounce, and the two verdict phases – the passing one doubling as the descent phase of the pass.

• up : TestPh

  Scanning up to the file top.

• b2 : TestPh

  Bounced off the top, about to re-enter rightwards.

• ty : TestPh

  Every register so far passed (also: returning with verdict yes).

• tn : TestPh

  Some register failed (also: returning with verdict no).

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqTestPh : DecidableEq TestPh

Equations

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

instance DescriptiveComplexity.Draw.instFiniteTestPh : Finite TestPh

inductive DescriptiveComplexity.Draw.TestRule : Type

The rule families of a test trip, one constructor each.

• up : TestRule

  Scan right while the file-top mark is clear.

• b1 : TestRule

  At the file top: step left into the bounce phase.

• b2go : TestRule

  Bounce: step back right into the pass.

• pass : TestRule

  At a register that passes the question: carry on down.

• fail : TestRule

  At a register that fails it: switch to the failing phase.

• walkY : TestRule

  Walk left over unmarked cells, and return, in the passing phase.

• stayN : TestRule

  Hold at registers, walk and return, in the failing phase.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqTestRule : DecidableEq TestRule

Equations

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

instance DescriptiveComplexity.Draw.instFiniteTestRule : Finite TestRule

structure DescriptiveComplexity.Draw.TestKit (A Q W P : Type) : Type

A file-test kit: the walked track, the three service slots, the per-register question as a predicate of the tracks, and where its phases sit in the program.

• t : W

  The walked track being questioned.

• rg : W

  The register mark.

• rl : W

  The file-top mark.

• wk : W

  The working-cell marker slot.

• TestG : (W → A) → Prop

  The per-register question, decided by the tracks.

• emb : TestPh → P

  The kit's phases in the program.

def DescriptiveComplexity.Draw.TestKit.rule {A Q W P : Type} (κ : TestKit A Q W P) (one : A) : TestRule → Rule A Q W P

The kit's rules.

Equations

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

theorem DescriptiveComplexity.Draw.TestKit.sep {A Q W P : Type} (κ : TestKit A Q W P) (one : A) (hemb : Function.Injective κ.emb) (ρ ρ' : TestRule) (f : Q → A) (g : W → A) : (κ.rule one ρ).guard f g → (κ.rule one ρ').guard f g → (κ.rule one ρ).srcPh = (κ.rule one ρ').srcPh → ρ = ρ'

In-shape separation: two of the kit's rules firing in the same phase on the same data are the same rule.

theorem DescriptiveComplexity.Draw.TestKit.exit_disjoint {A Q W P : Type} (κ : TestKit A Q W P) (one : A) (hemb : Function.Injective κ.emb) (ρ : TestRule) (f : Q → A) (g : W → A) : (κ.rule one ρ).guard f g → g κ.wk = one → g κ.rg ≠ one → (κ.rule one ρ).srcPh = κ.emb TestPh.ty ∨ (κ.rule one ρ).srcPh = κ.emb TestPh.tn → False

Exit disjointness: at the kit's two verdict phases – where a caller's exit rule, guarded wk = one ∧ rg ≠ one, lives – no kit rule fires on a symbol satisfying that guard.

theorem DescriptiveComplexity.Draw.TestKit.dstPh_emb {A Q W P : Type} (κ : TestKit A Q W P) (one : A) (ρ : TestRule) : ∃ (p : TestPh), (κ.rule one ρ).dstPh = κ.emb p

The trip stays inside its own phases: every rule lands in one the kit was given, which is what a caller that must know a property of the phases the machine can be in reads off a sub-machinery.

The discharge

theorem DescriptiveComplexity.Draw.TestKit.reachesIn_pos {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {κ : TestKit A Q W P} {rEmb : TestRule → R} (hrules : ∀ (ρ : TestRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnerg : κ.t ≠ κ.rg) (hnerl : κ.rl ≠ κ.t) (hnewk : κ.wk ≠ κ.t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {wkAddr : Univ A R P K dd → Prop} (hwkLt : WMSetLt WMLe wkAddr (F.cell gbot)) (hrg : ∀ (r : Univ A R P K dd → Prop), rest r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hrl : ∀ (r : Univ A R P K dd → Prop), rest r κ.rl = bitVal PR.zero PR.one (r = F.cell gtop)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = wkAddr)) {Test : I → Prop} (hcompat : ∀ (u : I), κ.TestG (PR.passTracksAt F.cell κ.t rest m (F.cell u)) ↔ Test u) {fc : Q → A} {s : Univ A R P K dd → Prop} (hsle : WMSetLe WMLe s (F.cell gtop)) {w : ℕ} (hgap : ∀ (u u' : I), IxSucc ile u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ w) (hTest : ∀ (u : I), Test u) : (wideData (Univ A R P K dd)).ReachesIn (wideRank (F.cell gtop) + 2 + ((ixRank ile gtop - ixRank ile gbot) * w + 1) + wideRank (F.cell gbot)) { state := Sum.inr (PR.stElt (κ.emb TestPh.up) fc), head := Sum.inl s, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb TestPh.ty) fc), head := Sum.inl wkAddr, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) }

The kit runs a passing file test: from the scan phase anywhere, up to the file top, down the file – every register passing – and back to the marker in the passing phase.

theorem DescriptiveComplexity.Draw.TestKit.reaches_pos {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {κ : TestKit A Q W P} {rEmb : TestRule → R} (hrules : ∀ (ρ : TestRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnerg : κ.t ≠ κ.rg) (hnerl : κ.rl ≠ κ.t) (hnewk : κ.wk ≠ κ.t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {wkAddr : Univ A R P K dd → Prop} (hwkLt : WMSetLt WMLe wkAddr (F.cell gbot)) (hrg : ∀ (r : Univ A R P K dd → Prop), rest r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hrl : ∀ (r : Univ A R P K dd → Prop), rest r κ.rl = bitVal PR.zero PR.one (r = F.cell gtop)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = wkAddr)) {Test : I → Prop} (hcompat : ∀ (u : I), κ.TestG (PR.passTracksAt F.cell κ.t rest m (F.cell u)) ↔ Test u) {fc : Q → A} {s : Univ A R P K dd → Prop} (hsle : WMSetLe WMLe s (F.cell gtop)) (hTest : ∀ (u : I), Test u) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (κ.emb TestPh.up) fc), head := Sum.inl s, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb TestPh.ty) fc), head := Sum.inl wkAddr, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) }

The kit runs a passing file test, the budget forgotten.

theorem DescriptiveComplexity.Draw.TestKit.reachesIn_neg {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {κ : TestKit A Q W P} {rEmb : TestRule → R} (hrules : ∀ (ρ : TestRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnerg : κ.t ≠ κ.rg) (hnerl : κ.rl ≠ κ.t) (hnewk : κ.wk ≠ κ.t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {wkAddr : Univ A R P K dd → Prop} (hwkLt : WMSetLt WMLe wkAddr (F.cell gbot)) (hrg : ∀ (r : Univ A R P K dd → Prop), rest r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hrl : ∀ (r : Univ A R P K dd → Prop), rest r κ.rl = bitVal PR.zero PR.one (r = F.cell gtop)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = wkAddr)) {Test : I → Prop} (hcompat : ∀ (u : I), κ.TestG (PR.passTracksAt F.cell κ.t rest m (F.cell u)) ↔ Test u) {fc : Q → A} {s : Univ A R P K dd → Prop} (hsle : WMSetLe WMLe s (F.cell gtop)) {w : ℕ} (hgap : ∀ (u u' : I), IxSucc ile u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ w) {u : I} (hTest : ¬Test u) : (wideData (Univ A R P K dd)).ReachesIn (wideRank (F.cell gtop) + 2 + ((ixRank ile gtop - ixRank ile gbot) * w + 1) + wideRank (F.cell gbot)) { state := Sum.inr (PR.stElt (κ.emb TestPh.up) fc), head := Sum.inl s, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb TestPh.tn) fc), head := Sum.inl wkAddr, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) }

The kit runs a failing file test: some register fails, and the trip ends at the marker in the failing phase.

theorem DescriptiveComplexity.Draw.TestKit.reaches_neg {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {κ : TestKit A Q W P} {rEmb : TestRule → R} (hrules : ∀ (ρ : TestRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnerg : κ.t ≠ κ.rg) (hnerl : κ.rl ≠ κ.t) (hnewk : κ.wk ≠ κ.t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {wkAddr : Univ A R P K dd → Prop} (hwkLt : WMSetLt WMLe wkAddr (F.cell gbot)) (hrg : ∀ (r : Univ A R P K dd → Prop), rest r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hrl : ∀ (r : Univ A R P K dd → Prop), rest r κ.rl = bitVal PR.zero PR.one (r = F.cell gtop)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = wkAddr)) {Test : I → Prop} (hcompat : ∀ (u : I), κ.TestG (PR.passTracksAt F.cell κ.t rest m (F.cell u)) ↔ Test u) {fc : Q → A} {s : Univ A R P K dd → Prop} (hsle : WMSetLe WMLe s (F.cell gtop)) {u : I} (hTest : ¬Test u) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (κ.emb TestPh.up) fc), head := Sum.inl s, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb TestPh.tn) fc), head := Sum.inl wkAddr, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) }

The kit runs a failing file test, the budget forgotten.

The clear and copy trips

The same itinerary with a writing pass in the middle: one phase runs the descent and the return alike, its register rule rewriting the walked digit and its walking rule – guarded rg ≠ one ∧ wk ≠ one – serving the gaps of the file and the way home.

inductive DescriptiveComplexity.Draw.TrackPh : Type

The phases of a write-pass trip: the up-scan, the bounce, and the one pass-and-return phase.

• up : TrackPh

  Scanning up to the file top.

• b2 : TrackPh

  Bounced off the top, about to re-enter rightwards.

• run : TrackPh

  Running the pass down the file, and returning.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqTrackPh : DecidableEq TrackPh

Equations

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

instance DescriptiveComplexity.Draw.instFiniteTrackPh : Finite TrackPh

inductive DescriptiveComplexity.Draw.TrackRule : Type

The rule families of a write-pass trip.

• up : TrackRule

  Scan right while the file-top mark is clear.

• b1 : TrackRule

  At the file top: step left into the bounce phase.

• b2go : TrackRule

  Bounce: step back right into the pass.

• put : TrackRule

  At a register: rewrite the walked digit and carry on down.

• walk : TrackRule

  Walk left over unmarked cells, and return.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqTrackRule : DecidableEq TrackRule

Equations

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

instance DescriptiveComplexity.Draw.instFiniteTrackRule : Finite TrackRule

structure DescriptiveComplexity.Draw.ClearKit (A Q W P : Type) : Type

A track-clearing kit: the walked track, the three service slots, and the phases.

• t : W

  The walked track being cleared.

• rg : W

  The register mark.

• rl : W

  The file-top mark.

• wk : W

  The working-cell marker slot.

• emb : TrackPh → P

  The kit's phases in the program.

def DescriptiveComplexity.Draw.ClearKit.rule {A Q W P : Type} [DecidableEq W] (κ : ClearKit A Q W P) (zero one : A) : TrackRule → Rule A Q W P

The kit's rules.

Equations

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

theorem DescriptiveComplexity.Draw.ClearKit.dstPh_emb {A Q W P : Type} [DecidableEq W] (κ : ClearKit A Q W P) (zero one : A) (ρ : TrackRule) : ∃ (p : TrackPh), (κ.rule zero one ρ).dstPh = κ.emb p

The trip stays inside its own phases: every rule lands in one the kit was given, which is what a caller that must know a property of the phases the machine can be in reads off a sub-machinery.

theorem DescriptiveComplexity.Draw.ClearKit.sep {A Q W P : Type} [DecidableEq W] (κ : ClearKit A Q W P) (zero one : A) (hemb : Function.Injective κ.emb) (ρ ρ' : TrackRule) (f : Q → A) (g : W → A) : (κ.rule zero one ρ).guard f g → (κ.rule zero one ρ').guard f g → (κ.rule zero one ρ).srcPh = (κ.rule zero one ρ').srcPh → ρ = ρ'

In-shape separation.

theorem DescriptiveComplexity.Draw.ClearKit.exit_disjoint {A Q W P : Type} [DecidableEq W] (κ : ClearKit A Q W P) (zero one : A) (hemb : Function.Injective κ.emb) (ρ : TrackRule) (f : Q → A) (g : W → A) : (κ.rule zero one ρ).guard f g → g κ.wk = one → g κ.rg ≠ one → (κ.rule zero one ρ).srcPh = κ.emb TrackPh.run → False

Exit disjointness at the kit's pass-and-return phase.

theorem DescriptiveComplexity.Draw.ClearKit.reachesIn {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {κ : ClearKit A Q W P} {rEmb : TrackRule → R} (hrules : ∀ (ρ : TrackRule), PR.rules (rEmb ρ) = κ.rule PR.zero PR.one ρ) {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnerg : κ.t ≠ κ.rg) (hnerl : κ.rl ≠ κ.t) (hnewk : κ.wk ≠ κ.t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {wkAddr : Univ A R P K dd → Prop} (hwkLt : WMSetLt WMLe wkAddr (F.cell gbot)) (hrg : ∀ (r : Univ A R P K dd → Prop), rest r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hrl : ∀ (r : Univ A R P K dd → Prop), rest r κ.rl = bitVal PR.zero PR.one (r = F.cell gtop)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = wkAddr)) {fc : Q → A} {s : Univ A R P K dd → Prop} (hsle : WMSetLe WMLe s (F.cell gtop)) {w : ℕ} (hgap : ∀ (u u' : I), IxSucc ile u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ w) : (wideData (Univ A R P K dd)).ReachesIn (wideRank (F.cell gtop) + 2 + ((ixRank ile gtop - ixRank ile gbot) * w + 1) + wideRank (F.cell gbot)) { state := Sum.inr (PR.stElt (κ.emb TrackPh.up) fc), head := Sum.inl s, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb TrackPh.run) fc), head := Sum.inl wkAddr, tape := wideTape (PR.trackTapeAt F.cell κ.t rest fun (x : I) => False) (PR.syElt PR.blank) }

The kit clears its track: from the scan phase anywhere, up to the file top, one pass writing the clear digit at every register, and back to the marker.

theorem DescriptiveComplexity.Draw.ClearKit.reaches {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {κ : ClearKit A Q W P} {rEmb : TrackRule → R} (hrules : ∀ (ρ : TrackRule), PR.rules (rEmb ρ) = κ.rule PR.zero PR.one ρ) {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnerg : κ.t ≠ κ.rg) (hnerl : κ.rl ≠ κ.t) (hnewk : κ.wk ≠ κ.t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {wkAddr : Univ A R P K dd → Prop} (hwkLt : WMSetLt WMLe wkAddr (F.cell gbot)) (hrg : ∀ (r : Univ A R P K dd → Prop), rest r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hrl : ∀ (r : Univ A R P K dd → Prop), rest r κ.rl = bitVal PR.zero PR.one (r = F.cell gtop)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = wkAddr)) {fc : Q → A} {s : Univ A R P K dd → Prop} (hsle : WMSetLe WMLe s (F.cell gtop)) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (κ.emb TrackPh.up) fc), head := Sum.inl s, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb TrackPh.run) fc), head := Sum.inl wkAddr, tape := wideTape (PR.trackTapeAt F.cell κ.t rest fun (x : I) => False) (PR.syElt PR.blank) }

The kit clears a track, the budget forgotten.

structure DescriptiveComplexity.Draw.CopyKit (A Q W P : Type) : Type

A track-copying kit: the walked track, the source slot – which must hold a bit at every register – the three service slots, and the phases.

• t : W

  The walked track being overwritten.

• src : W

  The source slot whose digit is copied.

• rg : W

  The register mark.

• rl : W

  The file-top mark.

• wk : W

  The working-cell marker slot.

• emb : TrackPh → P

  The kit's phases in the program.

def DescriptiveComplexity.Draw.CopyKit.rule {A Q W P : Type} [DecidableEq W] (κ : CopyKit A Q W P) (one : A) : TrackRule → Rule A Q W P

The kit's rules.

Equations

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

theorem DescriptiveComplexity.Draw.CopyKit.dstPh_emb {A Q W P : Type} [DecidableEq W] (κ : CopyKit A Q W P) (one : A) (ρ : TrackRule) : ∃ (p : TrackPh), (κ.rule one ρ).dstPh = κ.emb p

The trip stays inside its own phases: every rule lands in one the kit was given, which is what a caller that must know a property of the phases the machine can be in reads off a sub-machinery.

theorem DescriptiveComplexity.Draw.CopyKit.sep {A Q W P : Type} [DecidableEq W] (κ : CopyKit A Q W P) (one : A) (hemb : Function.Injective κ.emb) (ρ ρ' : TrackRule) (f : Q → A) (g : W → A) : (κ.rule one ρ).guard f g → (κ.rule one ρ').guard f g → (κ.rule one ρ).srcPh = (κ.rule one ρ').srcPh → ρ = ρ'

In-shape separation.

theorem DescriptiveComplexity.Draw.CopyKit.exit_disjoint {A Q W P : Type} [DecidableEq W] (κ : CopyKit A Q W P) (one : A) (hemb : Function.Injective κ.emb) (ρ : TrackRule) (f : Q → A) (g : W → A) : (κ.rule one ρ).guard f g → g κ.wk = one → g κ.rg ≠ one → (κ.rule one ρ).srcPh = κ.emb TrackPh.run → False

Exit disjointness at the kit's pass-and-return phase.

theorem DescriptiveComplexity.Draw.CopyKit.reachesIn {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {κ : CopyKit A Q W P} {rEmb : TrackRule → R} (hrules : ∀ (ρ : TrackRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnerg : κ.t ≠ κ.rg) (hnerl : κ.rl ≠ κ.t) (hnewk : κ.wk ≠ κ.t) (hnesrc : κ.src ≠ κ.t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {wkAddr : Univ A R P K dd → Prop} (hwkLt : WMSetLt WMLe wkAddr (F.cell gbot)) (hrg : ∀ (r : Univ A R P K dd → Prop), rest r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hrl : ∀ (r : Univ A R P K dd → Prop), rest r κ.rl = bitVal PR.zero PR.one (r = F.cell gtop)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = wkAddr)) (hsrcBit : ∀ (u : I), rest (F.cell u) κ.src = PR.zero ∨ rest (F.cell u) κ.src = PR.one) {fc : Q → A} {s : Univ A R P K dd → Prop} (hsle : WMSetLe WMLe s (F.cell gtop)) {w : ℕ} (hgap : ∀ (u u' : I), IxSucc ile u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ w) : (wideData (Univ A R P K dd)).ReachesIn (wideRank (F.cell gtop) + 2 + ((ixRank ile gtop - ixRank ile gbot) * w + 1) + wideRank (F.cell gbot)) { state := Sum.inr (PR.stElt (κ.emb TrackPh.up) fc), head := Sum.inl s, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb TrackPh.run) fc), head := Sum.inl wkAddr, tape := wideTape (PR.trackTapeAt F.cell κ.t rest fun (u : I) => rest (F.cell u) κ.src = PR.one) (PR.syElt PR.blank) }

The kit copies the source slot into its track: from the scan phase anywhere, up to the file top, one pass replacing every register's walked digit by its source digit, and back to the marker.

theorem DescriptiveComplexity.Draw.CopyKit.reaches {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {κ : CopyKit A Q W P} {rEmb : TrackRule → R} (hrules : ∀ (ρ : TrackRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnerg : κ.t ≠ κ.rg) (hnerl : κ.rl ≠ κ.t) (hnewk : κ.wk ≠ κ.t) (hnesrc : κ.src ≠ κ.t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {wkAddr : Univ A R P K dd → Prop} (hwkLt : WMSetLt WMLe wkAddr (F.cell gbot)) (hrg : ∀ (r : Univ A R P K dd → Prop), rest r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hrl : ∀ (r : Univ A R P K dd → Prop), rest r κ.rl = bitVal PR.zero PR.one (r = F.cell gtop)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = wkAddr)) (hsrcBit : ∀ (u : I), rest (F.cell u) κ.src = PR.zero ∨ rest (F.cell u) κ.src = PR.one) {fc : Q → A} {s : Univ A R P K dd → Prop} (hsle : WMSetLe WMLe s (F.cell gtop)) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (κ.emb TrackPh.up) fc), head := Sum.inl s, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb TrackPh.run) fc), head := Sum.inl wkAddr, tape := wideTape (PR.trackTapeAt F.cell κ.t rest fun (u : I) => rest (F.cell u) κ.src = PR.one) (PR.syElt PR.blank) }

The kit copies a track, the budget forgotten.

structure DescriptiveComplexity.Draw.MapKit (A Q W P : Type) : Type

A track-mapping kit: the walked track is rewritten by a bit the other tracks at each register decide – the pattern writes of the program, a target register loaded from the marks. The function ignoring the walked slot is the discharge's frame hypothesis.

• t : W

  The walked track being overwritten.

• rg : W

  The register mark.

• rl : W

  The file-top mark.

• wk : W

  The working-cell marker slot.

• Fb : (W → A) → Prop

  The written bit, computed from the tracks.

• emb : TrackPh → P

  The kit's phases in the program.

noncomputable def DescriptiveComplexity.Draw.MapKit.rule {A Q W P : Type} [DecidableEq W] (κ : MapKit A Q W P) (zero one : A) : TrackRule → Rule A Q W P

The kit's rules.

Equations

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

theorem DescriptiveComplexity.Draw.MapKit.dstPh_emb {A Q W P : Type} [DecidableEq W] (κ : MapKit A Q W P) (zero one : A) (ρ : TrackRule) : ∃ (p : TrackPh), (κ.rule zero one ρ).dstPh = κ.emb p

The trip stays inside its own phases: every rule lands in one the kit was given, which is what a caller that must know a property of the phases the machine can be in reads off a sub-machinery.

theorem DescriptiveComplexity.Draw.MapKit.sep {A Q W P : Type} [DecidableEq W] (κ : MapKit A Q W P) (zero one : A) (hemb : Function.Injective κ.emb) (ρ ρ' : TrackRule) (f : Q → A) (g : W → A) : (κ.rule zero one ρ).guard f g → (κ.rule zero one ρ').guard f g → (κ.rule zero one ρ).srcPh = (κ.rule zero one ρ').srcPh → ρ = ρ'

In-shape separation.

theorem DescriptiveComplexity.Draw.MapKit.exit_disjoint {A Q W P : Type} [DecidableEq W] (κ : MapKit A Q W P) (zero one : A) (hemb : Function.Injective κ.emb) (ρ : TrackRule) (f : Q → A) (g : W → A) : (κ.rule zero one ρ).guard f g → g κ.wk = one → g κ.rg ≠ one → (κ.rule zero one ρ).srcPh = κ.emb TrackPh.run → False

Exit disjointness at the kit's pass-and-return phase.

theorem DescriptiveComplexity.Draw.MapKit.reachesIn {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {κ : MapKit A Q W P} {rEmb : TrackRule → R} (hrules : ∀ (ρ : TrackRule), PR.rules (rEmb ρ) = κ.rule PR.zero PR.one ρ) {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnerg : κ.t ≠ κ.rg) (hnerl : κ.rl ≠ κ.t) (hnewk : κ.wk ≠ κ.t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {wkAddr : Univ A R P K dd → Prop} (hwkLt : WMSetLt WMLe wkAddr (F.cell gbot)) (hrg : ∀ (r : Univ A R P K dd → Prop), rest r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hrl : ∀ (r : Univ A R P K dd → Prop), rest r κ.rl = bitVal PR.zero PR.one (r = F.cell gtop)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = wkAddr)) (hFb : ∀ (g g' : W → A), (∀ (s : W), s ≠ κ.t → g s = g' s) → (κ.Fb g ↔ κ.Fb g')) {fc : Q → A} {s : Univ A R P K dd → Prop} (hsle : WMSetLe WMLe s (F.cell gtop)) {w : ℕ} (hgap : ∀ (u u' : I), IxSucc ile u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ w) : (wideData (Univ A R P K dd)).ReachesIn (wideRank (F.cell gtop) + 2 + ((ixRank ile gtop - ixRank ile gbot) * w + 1) + wideRank (F.cell gbot)) { state := Sum.inr (PR.stElt (κ.emb TrackPh.up) fc), head := Sum.inl s, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb TrackPh.run) fc), head := Sum.inl wkAddr, tape := wideTape (PR.trackTapeAt F.cell κ.t rest fun (u : I) => κ.Fb (PR.passTracksAt F.cell κ.t rest m (F.cell u))) (PR.syElt PR.blank) }

The kit rewrites its track by the function: from the scan phase anywhere, up to the file top, one pass writing the computed bit at every register, and back to the marker.

theorem DescriptiveComplexity.Draw.MapKit.reaches {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {κ : MapKit A Q W P} {rEmb : TrackRule → R} (hrules : ∀ (ρ : TrackRule), PR.rules (rEmb ρ) = κ.rule PR.zero PR.one ρ) {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnerg : κ.t ≠ κ.rg) (hnerl : κ.rl ≠ κ.t) (hnewk : κ.wk ≠ κ.t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {wkAddr : Univ A R P K dd → Prop} (hwkLt : WMSetLt WMLe wkAddr (F.cell gbot)) (hrg : ∀ (r : Univ A R P K dd → Prop), rest r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hrl : ∀ (r : Univ A R P K dd → Prop), rest r κ.rl = bitVal PR.zero PR.one (r = F.cell gtop)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = wkAddr)) (hFb : ∀ (g g' : W → A), (∀ (s : W), s ≠ κ.t → g s = g' s) → (κ.Fb g ↔ κ.Fb g')) {fc : Q → A} {s : Univ A R P K dd → Prop} (hsle : WMSetLe WMLe s (F.cell gtop)) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (κ.emb TrackPh.up) fc), head := Sum.inl s, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb TrackPh.run) fc), head := Sum.inl wkAddr, tape := wideTape (PR.trackTapeAt F.cell κ.t rest fun (u : I) => κ.Fb (PR.passTracksAt F.cell κ.t rest m (F.cell u))) (PR.syElt PR.blank) }

The kit rewrites a track, the budget forgotten.