The number written by unit propagation reduces to the number written by a machine

DescriptiveComplexity.MachNum.hornNumber_ordered_parsimonious_dtmNumber: the ordered parsimonious reduction HornNumber ≤ᵖ[≤] DTMNumber.

The machine is the unit-propagation machine of deterministic machine acceptance (DescriptiveComplexity.hornMachine), unchanged: it keeps one cell per element of the instance, in the order of the instance, marked when the element is forced, and on a satisfiable Horn formula it accepts with the propagation closure on its tape (DescriptiveComplexity.hornMachine_final). What the reduction adds is the reading of the number: the output cells are the cells of the output variables and the symbols read as 1 are the marked ones (DescriptiveComplexity.MachNum.numTuringInterp).

The machine reads its digits in tape order, while the Horn formula compares its output variables by a relation of the instance, below. The reduction reconciles the two by reordering its input first (DescriptiveComplexity.FOInterpretation.reorder): when below linearly orders the output variables, the new order puts them first, in that order, and the other elements after, in the order given (DescriptiveComplexity.MachNum.newOrder); the machine then lays its cells out in the new order, and the cells of the output variables come in the order of significance. When below is not such an order the number written by the formula is 0, and the reduction marks no output cell.

The vocabulary

def DescriptiveComplexity.MachNum.satOutHom : SatOcc.satOrd →ᴸ FirstOrder.Language.satOut.sum FirstOrder.Language.order

The vocabulary of ordered CNF instances, read in the one of ordered Horn formulas writing a number.

Equations

• DescriptiveComplexity.MachNum.satOutHom = FirstOrder.Language.LHom.sumInl.sumMap (FirstOrder.Language.LHom.id FirstOrder.Language.order)

instance DescriptiveComplexity.MachNum.satOutHom_isExpansionOn (A : Type) [FirstOrder.Language.satOut.Structure A] [LinearOrder A] : satOutHom.IsExpansionOn A

@[reducible, inline]

abbrev DescriptiveComplexity.MachNum.oOutSym : (FirstOrder.Language.satOut.sum FirstOrder.Language.order).Relations 1

“Is an output variable”, over the ordered vocabulary.

Equations

• DescriptiveComplexity.MachNum.oOutSym = Sum.inl DescriptiveComplexity.hnOut

@[reducible, inline]

abbrev DescriptiveComplexity.MachNum.oBelowSym : (FirstOrder.Language.satOut.sum FirstOrder.Language.order).Relations 2

The comparison of the output variables, over the ordered vocabulary.

Equations

• DescriptiveComplexity.MachNum.oBelowSym = Sum.inl DescriptiveComplexity.hnBelow

The order of the output variables, as a sentence

noncomputable def DescriptiveComplexity.MachNum.varOrdS : (FirstOrder.Language.satOut.sum FirstOrder.Language.order).Sentence

“The comparison of the output variables is a linear order on them” (DescriptiveComplexity.VarOrder), as a sentence.

Equations

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

noncomputable def DescriptiveComplexity.MachNum.varOrdF (α : Type) : (FirstOrder.Language.satOut.sum FirstOrder.Language.order).Formula α

The sentence, as a formula over any set of free variables.

Equations

• DescriptiveComplexity.MachNum.varOrdF α = FirstOrder.Language.Formula.relabel (fun (e : Empty) => e.elim) DescriptiveComplexity.MachNum.varOrdS

Reordering the instance

noncomputable def DescriptiveComplexity.MachNum.reordF : (FirstOrder.Language.satOut.sum FirstOrder.Language.order).Formula (Fin 2 × Fin 1)

The new order of the instance, as a formula of its two arguments: when the output variables are linearly ordered by below, they come first, in that order, and the other elements after, in the order given; otherwise the order given.

Equations

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

The interpretation

noncomputable def DescriptiveComplexity.MachNum.numTuringInterp : FOInterpretation (FirstOrder.Language.satOut.sum FirstOrder.Language.order) FirstOrder.Language.turingOut UPTag 3

The unit-propagation machine, with its output: the machine of DescriptiveComplexity.HornTM.hornTuringInterp, the cells of the output variables as output cells – when the output variables are linearly ordered – and the marked symbols read as 1.

Equations

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

def DescriptiveComplexity.MachNum.numMapEquiv {A : Type} : HV A ≃ numTuringInterp.Map A

The universe of the interpreted structure is the tagged triples.

Equations

• DescriptiveComplexity.MachNum.numMapEquiv = Equiv.refl (DescriptiveComplexity.HV A)

noncomputable def DescriptiveComplexity.MachNum.cellPt {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : numTuringInterp.Map A

The cell of an element.

Equations

• DescriptiveComplexity.MachNum.cellPt x = DescriptiveComplexity.MachNum.numMapEquiv (DescriptiveComplexity.posHCell x)

theorem DescriptiveComplexity.MachNum.relMap_out {A : Type} [FirstOrder.Language.satOut.Structure A] [LinearOrder A] (p : HV A) : FirstOrder.Language.Structure.RelMap mnOut ![numMapEquiv p] ↔ p.1 = UPTag.pCell ∧ (((∀ (a : A), p.2 1 ≤ a) ∧ ∀ (a : A), p.2 2 ≤ a) ∧ FirstOrder.Language.Structure.RelMap hnOut ![p.2 0]) ∧ VarOrder A

theorem DescriptiveComplexity.MachNum.relMap_one {A : Type} [FirstOrder.Language.satOut.Structure A] [LinearOrder A] (a : HV A) : FirstOrder.Language.Structure.RelMap mnOne ![numMapEquiv a] ↔ a.1 = UPTag.sM

theorem DescriptiveComplexity.MachNum.cellPt_injective {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : Function.Injective cellPt