Padding a kernel's block

A machine written against a DescriptiveComplexity.NexKernel pays for its run out of the drawing's own size, and the drawing's size is a count of tags – one per rule name, and a rule name of the guessing site carries an assignment of the guessed block. So a kernel with few relation variables draws a small machine and buys a short clock, while what the run costs is set by the machine's tape, which the block does not shrink.

The remedy is to pad: give the block extra relation variables that the kernel never mentions. It says the same thing – an existential block whose extra variables do not occur is satisfied exactly when the original is – and it multiplies the guessing site's rule names by 2 ^ (number of extra variables).

This file is that padding: the block (SOBlock.pad), the language morphism that reads a kernel over it (blockPadLHom), the two directions of the transport (realize_blockPad), and the kernel-level statement (NexKernel.pad_holds).

def DescriptiveComplexity.SOBlock.pad (B : SOBlock) (n a : ℕ) : SOBlock

A block with n more relation variables, each of arity a, which no kernel of the original block mentions.

Equations

• B.pad n a = { ι := B.ι ⊕ Fin n, ιFinite := ⋯, arity := Sum.elim B.arity fun (x : Fin n) => a }

@[simp]

theorem DescriptiveComplexity.SOBlock.pad_arity_inl (B : SOBlock) (n a : ℕ) (i : B.ι) : (B.pad n a).arity (Sum.inl i) = B.arity i

theorem DescriptiveComplexity.SOBlock.card_pad_ι (B : SOBlock) (n a : ℕ) : Nat.card (B.pad n a).ι = Nat.card B.ι + n

The variables of a padded block, counted: the original's and the new ones. This is what a clock's counting hypothesis is discharged by – the guessing site's rule names are indexed by assignments of the block.

def DescriptiveComplexity.SOBlock.unpadAssign (B : SOBlock) {n a : ℕ} {M : Type} (ρ : (B.pad n a).Assignment M) : B.Assignment M

What a padded block's assignment says about the original's: forget the new variables.

Equations

• B.unpadAssign ρ i = ρ (Sum.inl i)

def DescriptiveComplexity.SOBlock.padAssign (B : SOBlock) (n a : ℕ) {M : Type} (ρ : B.Assignment M) : (B.pad n a).Assignment M

And back: the new variables empty.

Equations

• B.padAssign n a ρ t = Sum.rec (motive := fun (x : B.ι ⊕ Fin n) => (Fin ((B.pad n a).arity x) → M) → Prop) ρ (fun (x : Fin n) (x_1 : Fin ((B.pad n a).arity (Sum.inr x)) → M) => False) t

@[simp]

theorem DescriptiveComplexity.SOBlock.unpadAssign_padAssign (B : SOBlock) (n a : ℕ) {M : Type} (ρ : B.Assignment M) : B.unpadAssign (B.padAssign n a ρ) = ρ

def DescriptiveComplexity.blockPadLHom (L : FirstOrder.Language) (B : SOBlock) (n a : ℕ) : L.sum B.lang →ᴸ L.sum (B.pad n a).lang

The language morphism reading a kernel of the block over the padded one: every symbol goes to itself, and the new relation symbols are simply not in the image.

Equations

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

theorem DescriptiveComplexity.blockPadLHom_isExpansionOn (L : FirstOrder.Language) (B : SOBlock) (n a : ℕ) (M : Type) (instM : L.Structure M) (ρ : (B.pad n a).Assignment M) : (blockPadLHom L B n a).IsExpansionOn M

The padded structure is an expansion along it: the new symbols are the only ones added, and no formula in the image mentions them.

theorem DescriptiveComplexity.realize_blockPad {L : FirstOrder.Language} (B : SOBlock) (n a : ℕ) (M : Type) [instM : L.Structure M] (ρ : (B.pad n a).Assignment M) (φ : (L.sum B.lang).Sentence) : M ⊨ (blockPadLHom L B n a).onSentence φ ↔ M ⊨ φ

Padding the block changes no meaning: a kernel of the original block, read over the padded one, says of a padded assignment what it said of the assignment's own part.

The padded kernel

def DescriptiveComplexity.NexKernel.pad {L : FirstOrder.Language} (K : NexKernel L) (n a : ℕ) : NexKernel L

A kernel with a padded block: the same expansion, the same sentence read over more relation variables.

Equations

• K.pad n a = { X := K.X, B := K.B.pad n a, ker := (DescriptiveComplexity.blockPadLHom (K.X.E.sum FirstOrder.Language.order) K.B n a).onSentence K.ker }

@[simp]

theorem DescriptiveComplexity.NexKernel.pad_X {L : FirstOrder.Language} (K : NexKernel L) (n a : ℕ) : (K.pad n a).X = K.X

@[simp]

theorem DescriptiveComplexity.NexKernel.pad_B {L : FirstOrder.Language} (K : NexKernel L) (n a : ℕ) : (K.pad n a).B = K.B.pad n a

theorem DescriptiveComplexity.NexKernel.pad_holds {L : FirstOrder.Language} (K : NexKernel L) (n a : ℕ) {M : Type} [instM : K.X.E.Structure M] [instO : LinearOrder M] : (K.pad n a).Holds M ↔ K.Holds M

A padded kernel says what the kernel said. The extra variables occur in no atom, so an assignment satisfying the padded kernel restricts to one satisfying the kernel, and one satisfying the kernel extends – by the empty relation – to one satisfying the padded kernel.