The number written by a circuit ignores isolated elements

A circuit with elements added that are no gate, wired to nothing, not outputs and compared with nothing writes the same number (DescriptiveComplexity.circuitNumber_of_embedding). So a relativized reduction to DescriptiveComplexity.CircuitNumber, whose target universe is a definable set of tagged tuples, is a reduction with the whole set of tagged tuples as universe: guard every relation by the domain formulas of its arguments (DescriptiveComplexity.RelFOInterpretation.guard), and the tuples outside the domain are such isolated elements (DescriptiveComplexity.RelOrderedParsimoniousReduction.unrelCircuitNumber).

This is what closes FP under relativized parsimonious reductions (DescriptiveComplexity.mem_FP_of_relOrderedParsimonious, in DescriptiveComplexity.Problems.CircuitNumber): the class has a complete problem that tolerates junk.

Isolated elements

theorem DescriptiveComplexity.circuitNumber_of_embedding {X Y : Type} [FirstOrder.Language.numCircuit.Structure X] [FirstOrder.Language.numCircuit.Structure Y] (φ : X → Y) (hφ : Function.Injective φ) (hrel : ∀ {n : ℕ} (R : FirstOrder.Language.numCircuit.Relations n) (xs : Fin n → X), (FirstOrder.Language.Structure.RelMap R fun (i : Fin n) => φ (xs i)) ↔ FirstOrder.Language.Structure.RelMap R xs) (hrange : ∀ {n : ℕ} (R : FirstOrder.Language.numCircuit.Relations n) (ys : Fin n → Y), FirstOrder.Language.Structure.RelMap R ys → ∀ (i : Fin n), ys i ∈ Set.range φ) : circuitNumber Y = circuitNumber X

Isolated elements do not change the number written. If X embeds in Y with the same relations, and every relation of Y holds only of elements of X, the two circuits write the same number.

Guarding an interpretation by its domain

A relativized reduction to the number written by a circuit