Composite kits: how the program instantiates its subroutines

The composites of the layer take their phases and rule families as parameters (“no continuation labels”: a program's phase set is its list of call sites). The program therefore assembles as a sum of kits, one per composite shape:

• a phase shape – a small inductive, one constructor per phase the composite visits (DescriptiveComplexity.Draw.ReadPh);
• a rule shape – one constructor per rule family, each with its concrete guard (DescriptiveComplexity.Draw.ReadRule);
• the rules function – the shape's DescriptiveComplexity.Draw.Rules, at a phase embedding and the kit's slots (DescriptiveComplexity.Draw.ReadKit.rule);
• a discharge – any program whose rule set contains the kit's rules satisfies the composite's rule hypotheses, so the composite's run theorem holds for it (DescriptiveComplexity.Draw.ReadKit.reaches_pos/_neg);
• an in-shape separation lemma – two of the kit's rules firing in the same phase on the same data are the same rule (DescriptiveComplexity.Draw.ReadKit.sep).

Global determinism then reduces to: each kit separates in-shape, the phase embeddings are injective, and distinct kits use disjoint phases – the source phase of a rule names its kit, so DescriptiveComplexity.Draw.Prog.sep_of's hypothesis never crosses kits.

This file builds the smallest kit with full content – the named-bit read of DescriptiveComplexity.Problems.Wide.DrawRead – as the template the others follow.

Summing kits: separation of a program assembled from sites

theorem DescriptiveComplexity.Draw.sep_sigma {A Q W P S : Type} {Sh : S → Type} (rules : (i : S) × Sh i → Rule A Q W P) (owner : P → S) (howner : ∀ (i : S) (ρ : Sh i), owner (rules ⟨i, ρ⟩).srcPh = i) (hsep : ∀ (i : S) (ρ ρ' : Sh i) (f : Q → A) (g : W → A), (rules ⟨i, ρ⟩).guard f g → (rules ⟨i, ρ'⟩).guard f g → (rules ⟨i, ρ⟩).srcPh = (rules ⟨i, ρ'⟩).srcPh → ρ = ρ') (r r' : (i : S) × Sh i) (f : Q → A) (g : W → A) : (rules r).guard f g → (rules r').guard f g → (rules r).srcPh = (rules r').srcPh → r = r'

Separation of a program assembled from kits: when the rule names are a sigma of per-site shapes, every rule's source phase is owned by its site, and each site separates in-shape, the whole program separates. This is the form DescriptiveComplexity.Draw.Prog.sep_of receives from an assembly: the cross-site case is settled by ownership, the in-site case by the kits' sep lemmas – which is why a kit's exit rules, fired from another kit's end phases, must be grouped under the site owning those phases, not the site they serve.

The read trip's shapes

inductive DescriptiveComplexity.Draw.ReadPh : Type

The phases of a read trip: at the marker, scanning up, and the two verdict returns.

• start : ReadPh

  At the working-cell marker, about to leave.

• up : ReadPh

  Scanning up to the named cell.

• ry : ReadPh

  The bit was set: returning.

• rn : ReadPh

  The bit was clear: returning.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqReadPh : DecidableEq ReadPh

Equations

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

instance DescriptiveComplexity.Draw.instFiniteReadPh : Finite ReadPh

inductive DescriptiveComplexity.Draw.ReadRule : Type

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

• turn : ReadRule

  Leave the marker rightwards.

• up : ReadRule

  Scan right while the name does not match.

• rd1 : ReadRule

  At the named cell with the bit set: branch positive, step left.

• rd0 : ReadRule

  At the named cell with the bit clear: branch negative, step left.

• backY : ReadRule

  Return leftwards in the positive phase.

• backN : ReadRule

  Return leftwards in the negative phase.

• stayS : ReadRule

  Walk left back to the marker before leaving it: what lets a dispatch enter the trip by stepping right off the marker.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqReadRule : DecidableEq ReadRule

Equations

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

instance DescriptiveComplexity.Draw.instFiniteReadRule : Finite ReadRule

The kit

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

A read-trip kit: the two slots it reads, the name guard, and where its phases sit in the program.

• t : W

  The walked track being read.

• wk : W

  The working-cell marker slot.

• Match : (Q → A) → (W → A) → Prop

  The name guard: this cell is the one the control names.

• emb : ReadPh → P

  The kit's phases in the program.

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

The kit's rules. Every attribute is a function of the constructor, and every guard is decided by the slots the shape reads.

Equations

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

theorem DescriptiveComplexity.Draw.ReadKit.sep {A Q W P : Type} (κ : ReadKit A Q W P) (one : A) (hemb : Function.Injective κ.emb) (ρ ρ' : ReadRule) (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. The phase splits the families into four groups, and within a group the guards are mutually exclusive.

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

A trip stays inside its own phases: every rule of the kit lands in one of the four the kit was given, so a caller that knows a property of those knows it of every phase the trip can be in. This is what a determinism-after- the-guess argument needs of a sub-machinery (DescriptiveComplexity.Draw.Data.nexProg_uniqueFrom).

theorem DescriptiveComplexity.Draw.ReadKit.exit_disjoint {A Q W P : Type} (κ : ReadKit A Q W P) (one : A) (hemb : Function.Injective κ.emb) (ρ : ReadRule) (f : Q → A) (g : W → A) : (κ.rule one ρ).guard f g → g κ.wk = one → (κ.rule one ρ).srcPh = κ.emb ReadPh.ry ∨ (κ.rule one ρ).srcPh = κ.emb ReadPh.rn → False

Exit disjointness at the kit's two verdict phases: no kit rule fires there on a symbol with the marker set.

The discharge

theorem DescriptiveComplexity.Draw.ReadKit.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} {κ : ReadKit A Q W P} {rEmb : ReadRule → R} (hrules : ∀ (ρ : ReadRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) {I : Type} {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnewk : κ.wk ≠ κ.t) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {v : Univ A R P K dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = v)) {fc : Q → A} {x₀ : I} (hname : κ.Match fc (PR.passTracksAt F.cell κ.t rest m (F.cell x₀))) (huniq : ∀ (r : Univ A R P K dd → Prop), κ.Match fc (PR.passTracksAt F.cell κ.t rest m r) → r = F.cell x₀) (hm : m x₀) : (wideData (Univ A R P K dd)).ReachesIn (2 * (wideRank (F.cell x₀) - wideRank v) + 2) { state := Sum.inr (PR.stElt (κ.emb ReadPh.start) fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb ReadPh.ry) fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) }

The kit reads a set bit: the composite's run theorem, with every rule hypothesis discharged from the kit's rules.

theorem DescriptiveComplexity.Draw.ReadKit.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} {κ : ReadKit A Q W P} {rEmb : ReadRule → R} (hrules : ∀ (ρ : ReadRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) {I : Type} {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnewk : κ.wk ≠ κ.t) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {v : Univ A R P K dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = v)) {fc : Q → A} {x₀ : I} (hname : κ.Match fc (PR.passTracksAt F.cell κ.t rest m (F.cell x₀))) (huniq : ∀ (r : Univ A R P K dd → Prop), κ.Match fc (PR.passTracksAt F.cell κ.t rest m r) → r = F.cell x₀) (hm : m x₀) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (κ.emb ReadPh.start) fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb ReadPh.ry) fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) }

The kit reads a set bit, the budget forgotten.

theorem DescriptiveComplexity.Draw.ReadKit.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} {κ : ReadKit A Q W P} {rEmb : ReadRule → R} (hrules : ∀ (ρ : ReadRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) {I : Type} {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnewk : κ.wk ≠ κ.t) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {v : Univ A R P K dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = v)) {fc : Q → A} {x₀ : I} (hname : κ.Match fc (PR.passTracksAt F.cell κ.t rest m (F.cell x₀))) (huniq : ∀ (r : Univ A R P K dd → Prop), κ.Match fc (PR.passTracksAt F.cell κ.t rest m r) → r = F.cell x₀) (hm : ¬m x₀) : (wideData (Univ A R P K dd)).ReachesIn (2 * (wideRank (F.cell x₀) - wideRank v) + 2) { state := Sum.inr (PR.stElt (κ.emb ReadPh.start) fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb ReadPh.rn) fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) }

The kit reads a clear bit.

theorem DescriptiveComplexity.Draw.ReadKit.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} {κ : ReadKit A Q W P} {rEmb : ReadRule → R} (hrules : ∀ (ρ : ReadRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) {I : Type} {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnewk : κ.wk ≠ κ.t) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {v : Univ A R P K dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = v)) {fc : Q → A} {x₀ : I} (hname : κ.Match fc (PR.passTracksAt F.cell κ.t rest m (F.cell x₀))) (huniq : ∀ (r : Univ A R P K dd → Prop), κ.Match fc (PR.passTracksAt F.cell κ.t rest m r) → r = F.cell x₀) (hm : ¬m x₀) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (κ.emb ReadPh.start) fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb ReadPh.rn) fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) }

The kit reads a clear bit, the budget forgotten.

The write trip's shapes

The same trip writing the digit: the kit carries the written bit as a function of the control payload, so one shape serves constant writes and writes of a previously computed bit alike.

inductive DescriptiveComplexity.Draw.WritePh : Type

The phases of a write trip.

• start : WritePh

  At the working-cell marker, about to leave.

• up : WritePh

  Scanning up to the named cell.

• back : WritePh

  Written: returning.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqWritePh : DecidableEq WritePh

Equations

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

instance DescriptiveComplexity.Draw.instFiniteWritePh : Finite WritePh

inductive DescriptiveComplexity.Draw.WriteRule : Type

The rule families of a write trip.

• turn : WriteRule

  Leave the marker rightwards.

• up : WriteRule

  Scan right while the name does not match.

• put : WriteRule

  At the named cell: write the bit, step left.

• back : WriteRule

  Return leftwards.

• stayS : WriteRule

  Walk left back to the marker before leaving it.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqWriteRule : DecidableEq WriteRule

Equations

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

instance DescriptiveComplexity.Draw.instFiniteWriteRule : Finite WriteRule

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

A write-trip kit: the slots, the name guard, the written bit as a function of the payload, and the phases.

• t : W

  The walked track being written.

• wk : W

  The working-cell marker slot.

• Match : (Q → A) → (W → A) → Prop

  The name guard.

• bVal : (Q → A) → Prop

  The written bit, as a function of the payload.

• emb : WritePh → P

  The kit's phases in the program.

noncomputable def DescriptiveComplexity.Draw.WriteKit.rule {A Q W P : Type} [DecidableEq W] (κ : WriteKit A Q W P) (zero one : A) : WriteRule → 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.WriteKit.dstPh_emb {A Q W P : Type} [DecidableEq W] (κ : WriteKit A Q W P) (zero one : A) (ρ : WriteRule) : ∃ (p : WritePh), (κ.rule zero one ρ).dstPh = κ.emb p

A write trip stays inside its own phases: every rule of the kit lands in one of the phases the kit was given, which is what a determinism-after-the-guess argument needs of a sub-machinery (DescriptiveComplexity.Draw.Data.nexProg_uniqueFrom).

theorem DescriptiveComplexity.Draw.WriteKit.sep {A Q W P : Type} [DecidableEq W] (κ : WriteKit A Q W P) (zero one : A) (hemb : Function.Injective κ.emb) (ρ ρ' : WriteRule) (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.WriteKit.exit_disjoint {A Q W P : Type} [DecidableEq W] (κ : WriteKit A Q W P) (zero one : A) (hemb : Function.Injective κ.emb) (ρ : WriteRule) (f : Q → A) (g : W → A) : (κ.rule zero one ρ).guard f g → g κ.wk = one → (κ.rule zero one ρ).srcPh = κ.emb WritePh.back → False

Exit disjointness at the kit's return phase: no kit rule fires there on a symbol with the marker set.

theorem DescriptiveComplexity.Draw.WriteKit.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} {κ : WriteKit A Q W P} {rEmb : WriteRule → R} (hrules : ∀ (ρ : WriteRule), PR.rules (rEmb ρ) = κ.rule PR.zero PR.one ρ) {I : Type} {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnewk : κ.wk ≠ κ.t) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {v : Univ A R P K dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = v)) {fc : Q → A} {x₀ : I} (hname : κ.Match fc (PR.passTracksAt F.cell κ.t rest m (F.cell x₀))) (huniq : ∀ (r : Univ A R P K dd → Prop), κ.Match fc (PR.passTracksAt F.cell κ.t rest m r) → r = F.cell x₀) : (wideData (Univ A R P K dd)).ReachesIn (2 * (wideRank (F.cell x₀) - wideRank v) + 2) { state := Sum.inr (PR.stElt (κ.emb WritePh.start) fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb WritePh.back) fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell κ.t rest fun (y : I) => y = x₀ ∧ κ.bVal fc ∨ y ≠ x₀ ∧ m y) (PR.syElt PR.blank) }

The kit writes its bit at the named cell and returns to the marker.

theorem DescriptiveComplexity.Draw.WriteKit.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} {κ : WriteKit A Q W P} {rEmb : WriteRule → R} (hrules : ∀ (ρ : WriteRule), PR.rules (rEmb ρ) = κ.rule PR.zero PR.one ρ) {I : Type} {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnewk : κ.wk ≠ κ.t) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {v : Univ A R P K dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = v)) {fc : Q → A} {x₀ : I} (hname : κ.Match fc (PR.passTracksAt F.cell κ.t rest m (F.cell x₀))) (huniq : ∀ (r : Univ A R P K dd → Prop), κ.Match fc (PR.passTracksAt F.cell κ.t rest m r) → r = F.cell x₀) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (κ.emb WritePh.start) fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb WritePh.back) fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell κ.t rest fun (y : I) => y = x₀ ∧ κ.bVal fc ∨ y ≠ x₀ ∧ m y) (PR.syElt PR.blank) }

The kit writes a named bit, the budget forgotten.