Rules that never fire, and the tags they buy

A clocked program's budget is 2 ^ |Tag|, and its tags are its rule names: one per site and shape. A reduction that needs a longer clock therefore needs more rule names – and it needs them without changing anything else, because every constant the clock is measured against (the file's registers, the evaluation's widths, the record's own dimensions) is read off the same record.

This file is that knob. A junk site carries one rule whose guard is False: it can never fire, so no run, no separation argument and no determinism argument sees it, while the rule names go up by one. Padding a site type by Fin n adds n of them.

The whole thing is generic in the site type, so it applies to any program the definability layer writes down (padRules, uRulesDefinable_padRules), and the count is one line (card_rTagOf_pad).

def DescriptiveComplexity.Draw.falseRule {P A Q W : Type} (p : P) : Rule A Q W P

A rule that never fires: its guard is false, and everything else is the identity. It sits at a phase of the caller's choosing and is never reached there, the guard being what a step asks for first.

Equations

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

def DescriptiveComplexity.Draw.padSh {S : Type} (Sh : S → Type) (n : ℕ) : S ⊕ Fin n → Type

The shapes of a padded site type: the old sites keep theirs, and each new one has a single rule.

Equations

• DescriptiveComplexity.Draw.padSh Sh n (Sum.inl i) = Sh i
• DescriptiveComplexity.Draw.padSh Sh n (Sum.inr val) = Unit

instance DescriptiveComplexity.Draw.instFinitePadSh {S : Type} {Sh : S → Type} [∀ (i : S), Finite (Sh i)] (n : ℕ) (i : S ⊕ Fin n) : Finite (padSh Sh n i)

def DescriptiveComplexity.Draw.padRules {L : FirstOrder.Language} {dt : Data L} {S : Type} {Sh : S → Type} {P : Type} (rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P) (p₀ : P) (n : ℕ) (e : Env L) (i : S ⊕ Fin n) : padSh Sh n i → Rule e.α dt.CtlIx dt.SlotIx P

The rules of a padded site type: the old ones, and a rule that never fires at each new site.

Equations

• DescriptiveComplexity.Draw.padRules rules p₀ n x✝ (Sum.inl i) ρ = rules x✝ i ρ
• DescriptiveComplexity.Draw.padRules rules p₀ n x✝ (Sum.inr val) x_4 = DescriptiveComplexity.Draw.falseRule p₀

@[simp]

theorem DescriptiveComplexity.Draw.padRules_inl {L : FirstOrder.Language} {dt : Data L} {S : Type} {Sh : S → Type} {P : Type} (rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P) (p₀ : P) (n : ℕ) (e : Env L) (i : S) (ρ : Sh i) : padRules rules p₀ n e (Sum.inl i) ρ = rules e i ρ

@[simp]

theorem DescriptiveComplexity.Draw.padRules_inr {L : FirstOrder.Language} {dt : Data L} {S : Type} {Sh : S → Type} {P : Type} (rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P) (p₀ : P) {n : ℕ} (e : Env L) (k : Fin n) (ρ : padSh Sh n (Sum.inr k)) : padRules rules p₀ n e (Sum.inr k) ρ = falseRule p₀

theorem DescriptiveComplexity.Draw.uRulesDefinable_padRules {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (h : URulesDefinable rules) (p₀ : P) (n : ℕ) : URulesDefinable (padRules rules p₀ n)

The padded rules are definable: the old ones by hypothesis, and a rule that never fires by uGDefinable_false.

theorem DescriptiveComplexity.Draw.falseRule_facts {L : FirstOrder.Language} {dt : Data L} {P A Q : Type} (zero one : A) (p : P) : Rule.KeepsFile dt (falseRule p) ∧ Rule.KeepsCellTracks dt (falseRule p) ∧ Rule.WritesBits dt zero one (falseRule p)

A junk rule writes nothing, so it keeps the file, keeps the addressed tracks, keeps every slot and writes bits – the four facts a backward reading asks of a rule it meets by name.

theorem DescriptiveComplexity.Draw.falseRule_keepsSlot {L : FirstOrder.Language} {dt : Data L} {P A Q : Type} (t : dt.SlotIx) (p : P) : Rule.KeepsSlot dt t (falseRule p)

And it leaves every slot as it found it.

def DescriptiveComplexity.Draw.padRulesAt {L : FirstOrder.Language} {dt : Data L} {S : Type} (Sh : S → Type) {P A : Type} (rl : (i : S) → Sh i → Rule A dt.CtlIx dt.SlotIx P) (p₀ : P) (n : ℕ) (i : S ⊕ Fin n) : padSh Sh n i → Rule A dt.CtlIx dt.SlotIx P

The rules of a padded site type, at one instance: the same padding as padRules, for a program written down at a fixed universe rather than as a family.

Equations

• DescriptiveComplexity.Draw.padRulesAt Sh rl p₀ n (Sum.inl i) ρ = rl i ρ
• DescriptiveComplexity.Draw.padRulesAt Sh rl p₀ n (Sum.inr val) x_2 = DescriptiveComplexity.Draw.falseRule p₀

@[simp]

theorem DescriptiveComplexity.Draw.padRulesAt_inl {L : FirstOrder.Language} {dt : Data L} {S : Type} {Sh : S → Type} {P A : Type} (rl : (i : S) → Sh i → Rule A dt.CtlIx dt.SlotIx P) (p₀ : P) (n : ℕ) (i : S) (ρ : Sh i) : padRulesAt Sh rl p₀ n (Sum.inl i) ρ = rl i ρ

theorem DescriptiveComplexity.Draw.not_guard_padRulesAt {L : FirstOrder.Language} {dt : Data L} {S : Type} {Sh : S → Type} {P A : Type} (rl : (i : S) → Sh i → Rule A dt.CtlIx dt.SlotIx P) {p₀ : P} {n : ℕ} (k : Fin n) (ρ : padSh Sh n (Sum.inr k)) (f : dt.CtlIx → A) (g : dt.SlotIx → A) : ¬(padRulesAt Sh rl p₀ n (Sum.inr k) ρ).guard f g

A junk rule never fires, which is all any run, separation or determinism argument needs to know about it.

theorem DescriptiveComplexity.Draw.sep_padRulesAt {L : FirstOrder.Language} {dt : Data L} {S : Type} {Sh : S → Type} {P A : Type} {rl : (i : S) → Sh i → Rule A dt.CtlIx dt.SlotIx P} {p₀ : P} {n : ℕ} {Ph : P → Prop} (hsep : ∀ (i i' : S) (ρ : Sh i) (ρ' : Sh i') (f : dt.CtlIx → A) (g : dt.SlotIx → A), Ph (rl i ρ).srcPh → (rl i ρ).guard f g → (rl i' ρ').guard f g → (rl i ρ).srcPh = (rl i' ρ').srcPh → ⟨i, ρ⟩ = ⟨i', ρ'⟩) (i i' : S ⊕ Fin n) (ρ : padSh Sh n i) (ρ' : padSh Sh n i') (f : dt.CtlIx → A) (g : dt.SlotIx → A) : Ph (padRulesAt Sh rl p₀ n i ρ).srcPh → (padRulesAt Sh rl p₀ n i ρ).guard f g → (padRulesAt Sh rl p₀ n i' ρ').guard f g → (padRulesAt Sh rl p₀ n i ρ).srcPh = (padRulesAt Sh rl p₀ n i' ρ').srcPh → ⟨i, ρ⟩ = ⟨i', ρ'⟩

Padding keeps in-shape separation: two rules that fire on the same data in the same phase are the same, the junk ones firing on none.

theorem DescriptiveComplexity.Draw.padRules_eq_padRulesAt {L : FirstOrder.Language} {dt : Data L} {S : Type} {Sh : S → Type} {P : Type} (rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P) (p₀ : P) (n : ℕ) (e : Env L) : padRules rules p₀ n e = padRulesAt Sh (rules e) p₀ n

The family and the pointwise padding agree, which is what lets a program written down at one universe be read as the definability layer's.

theorem DescriptiveComplexity.Draw.card_rTagOf_pad {S : Type} {Sh : S → Type} [Finite S] [∀ (i : S), Finite (Sh i)] (n : ℕ) : Nat.card (Data.RTagOf (S ⊕ Fin n) (padSh Sh n)) = Nat.card (Data.RTagOf S Sh) + n

What the padding buys: one rule name per junk site.