One block instead of two: the doubled block

Plumbing for the hardness discharge of SUCCINCT-REACH (DescriptiveComplexity.Problems.SuccinctReach.Hardness).

A DescriptiveComplexity.SOTCSpec states its transition condition as a sentence over two successive expansions by the same block – the current state reads the first copy, the next state the second. That shape is what makes the pullback through an interpretation cheap (DescriptiveComplexity.SecondOrderTransitiveClosurePull). The Tseitin encoding, on the other hand, encodes a kernel over one block expansion, giving one propositional variable per relation variable of that block and tuple. So the discharge needs the two presentations identified:

• DescriptiveComplexity.SOBlock.double is the block with two disjoint copies of the original relation variables, whose assignments are pairs of assignments (DescriptiveComplexity.SOBlock.joinAssign);
• DescriptiveComplexity.blockPairLHom renames a sentence over two successive expansions into one over the doubled expansion, and DescriptiveComplexity.blockFstLHom renames a sentence over a single expansion into one over the doubled expansion that only mentions the first copy – which is how the endpoint sentences are put on the same footing as the transition sentence, so that the three Tseitin encodings of the discharge share one block and hence share their propositional variables for the state.

Both renamings are FirstOrder.Language.LHom.IsExpansionOn for the structures concerned, so they preserve realization; the corresponding statements are DescriptiveComplexity.realize_blockPairLHom and DescriptiveComplexity.realize_blockFstLHom.

A third renaming lives here for the same reason. The Tseitin builders produce formulas over L ⊕ order for a base vocabulary L; the discharge instantiates L at an already ordered L₀ ⊕ order, so their output mentions two copies of the order symbol, both read by the same linear order. DescriptiveComplexity.mergeOrdLHom merges them, which is what lets the formulas be used as the defining formulas of an interpretation whose source vocabulary is L₀ ⊕ order.

The doubled block

def DescriptiveComplexity.SOBlock.double (B : SOBlock) : SOBlock

The doubled block: two disjoint copies of a block's relation variables, the first standing for the current state and the second for the next one.

Equations

• B.double = { ι := B.ι ⊕ B.ι, ιFinite := ⋯, arity := Sum.elim B.arity B.arity }

def DescriptiveComplexity.SOBlock.joinAssign {A : Type} (B : SOBlock) (ρ σ : B.Assignment A) : B.double.Assignment A

The assignment of the doubled block made of two assignments of the original.

Equations

• B.joinAssign ρ σ (Sum.inl i) = ρ i
• B.joinAssign ρ σ (Sum.inr i) = σ i

def DescriptiveComplexity.SOBlock.fstAssign {A : Type} (B : SOBlock) (μ : B.double.Assignment A) : B.Assignment A

The first component of an assignment of the doubled block.

Equations

• B.fstAssign μ i = μ (Sum.inl i)

def DescriptiveComplexity.SOBlock.sndAssign {A : Type} (B : SOBlock) (μ : B.double.Assignment A) : B.Assignment A

The second component of an assignment of the doubled block.

Equations

• B.sndAssign μ i = μ (Sum.inr i)

@[simp]

theorem DescriptiveComplexity.SOBlock.fstAssign_joinAssign {A : Type} (B : SOBlock) (ρ σ : B.Assignment A) : B.fstAssign (B.joinAssign ρ σ) = ρ

@[simp]

theorem DescriptiveComplexity.SOBlock.sndAssign_joinAssign {A : Type} (B : SOBlock) (ρ σ : B.Assignment A) : B.sndAssign (B.joinAssign ρ σ) = σ

theorem DescriptiveComplexity.SOBlock.joinAssign_fst_snd {A : Type} (B : SOBlock) (μ : B.double.Assignment A) : B.joinAssign (B.fstAssign μ) (B.sndAssign μ) = μ

Renaming two successive expansions into the doubled one

def DescriptiveComplexity.blockPairLHom {L₀ : FirstOrder.Language} (B : SOBlock) : (L₀.sum B.lang).sum B.lang →ᴸ L₀.sum B.double.lang

The renaming of two successive expansions by a block into the expansion by the doubled block: the first copy's symbols become the first copy's, the second copy's the second's.

Equations

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

def DescriptiveComplexity.blockFstLHom {L₀ : FirstOrder.Language} (B : SOBlock) : L₀.sum B.lang →ᴸ L₀.sum B.double.lang

The renaming of a single expansion by a block into the expansion by the doubled block, landing in the first copy.

Equations

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

theorem DescriptiveComplexity.blockPairLHom_isExpansionOn {L₀ : FirstOrder.Language} (B : SOBlock) {A : Type} [instA : L₀.Structure A] (ρ σ : B.Assignment A) : (blockPairLHom B).IsExpansionOn A

The pair renaming is an expansion, the two copies being interpreted by the two components of a joined assignment.

theorem DescriptiveComplexity.blockFstLHom_isExpansionOn {L₀ : FirstOrder.Language} (B : SOBlock) {A : Type} [instA : L₀.Structure A] (μ : B.double.Assignment A) : (blockFstLHom B).IsExpansionOn A

The first-copy renaming is an expansion.

theorem DescriptiveComplexity.realize_blockPairLHom {L₀ : FirstOrder.Language} (B : SOBlock) {A : Type} [instA : L₀.Structure A] (ρ σ : B.Assignment A) (φ : ((L₀.sum B.lang).sum B.lang).Sentence) : A ⊨ (blockPairLHom B).onSentence φ ↔ A ⊨ φ

The pair renaming preserves realization: a sentence over two successive expansions says of a pair of assignments what its renaming says of the joined assignment.

theorem DescriptiveComplexity.realize_blockFstLHom {L₀ : FirstOrder.Language} (B : SOBlock) {A : Type} [instA : L₀.Structure A] (μ : B.double.Assignment A) (φ : (L₀.sum B.lang).Sentence) : A ⊨ (blockFstLHom B).onSentence φ ↔ A ⊨ φ

The first-copy renaming preserves realization, and in particular the result does not depend on the second component of the assignment.

Merging two copies of the order

def DescriptiveComplexity.mergeOrdLHom (L₀ : FirstOrder.Language) : (L₀.sum FirstOrder.Language.order).sum FirstOrder.Language.order →ᴸ L₀.sum FirstOrder.Language.order

The renaming merging the two order symbols of a doubly ordered expansion: the Tseitin builders add an order to the vocabulary they are given, which here is already ordered.

Equations

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

theorem DescriptiveComplexity.mergeOrdLHom_isExpansionOn {L₀ : FirstOrder.Language} {A : Type} [L₀.Structure A] [LinearOrder A] : (mergeOrdLHom L₀).IsExpansionOn A

Merging the two order symbols is an expansion: both are read by the same linear order.

theorem DescriptiveComplexity.realize_mergeOrdLHom {L₀ : FirstOrder.Language} {A : Type} [L₀.Structure A] [LinearOrder A] {γ : Type} (φ : ((L₀.sum FirstOrder.Language.order).sum FirstOrder.Language.order).Formula γ) (v : γ → A) : ((mergeOrdLHom L₀).onFormula φ).Realize v ↔ φ.Realize v

Merging the two order symbols preserves realization.