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.

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 ρ