The drawn instance draws the intended code

The correctness of the drawing: the instance built by DescriptiveComplexity.codeProgInterp is well formed (DescriptiveComplexity.codeWF_codeProg) and its root draws

comp cP (pair (numeral card) (nest of the tables))

(DescriptiveComplexity.decodesTo_rootPt).

Everything is a walk of the input order, taken with the increasing enumeration DescriptiveComplexity.ordEnum of the universe: the numeral chain and each level of each table block are proved by the same downward induction, from the tail of the chain – the shared zero element – back to its head.

The subtree of the fixed code cP is the one place the induction is on a code rather than on the order: DescriptiveComplexity.decodesTo_subPos says that a drawing whose marks and children follow DescriptiveComplexity.subAt, DescriptiveComplexity.sub1 and DescriptiveComplexity.sub2 draws every subterm at its position, by structural induction on the code.

Drawing a fixed code

structure DescriptiveComplexity.Draws {N : Type} [FirstOrder.Language.code.Structure N] (c : Nat.Partrec.Code) (F : SubPos c → N) : Prop

A drawing of the syntax tree of a code: every position carries the mark of its subterm's constructor, and the child relations follow the positions of the children.

• mark (p : SubPos c) : Mark (tagOf (subAt c p)) (F p)

  Every position carries the mark of its subterm's constructor.

• arg1 (p q : SubPos c) : sub1 c p = some q → CArg1 (F p) (F q)

  The first-child relation follows the first child of a position.

• arg2 (p q : SubPos c) : sub2 c p = some q → CArg2 (F p) (F q)

  The second-child relation follows the second child of a position.

theorem DescriptiveComplexity.Draws.embed {N : Type} [FirstOrder.Language.code.Structure N] {c c' : Nat.Partrec.Code} {F : SubPos c → N} (h : Draws c F) (e : SubPos c' → SubPos c) (hsub : ∀ (q : SubPos c'), subAt c (e q) = subAt c' q) (h1e : ∀ (q : SubPos c'), sub1 c (e q) = Option.map e (sub1 c' q)) (h2e : ∀ (q : SubPos c'), sub2 c (e q) = Option.map e (sub2 c' q)) : Draws c' (F ∘ e)

A drawing restricts to a drawing of a subterm, along an embedding of positions that respects subterms and children.

theorem DescriptiveComplexity.decodesTo_subPos {N : Type} [FirstOrder.Language.code.Structure N] (c : Nat.Partrec.Code) (F : SubPos c → N) : Draws c F → ∀ (p : SubPos c), DecodesTo (F p) (subAt c p)

A drawing of a code draws every subterm at its position. The hypotheses are exactly what the defining formulas of the interpretation give for the tags of cP; the induction is on the code.

The increasing enumeration of a finite linear order

noncomputable def DescriptiveComplexity.ordEnum (A : Type) [LinearOrder A] [Finite A] : Fin (Nat.card A) ≃o A

The increasing enumeration of a finite linear order. Every chain of the drawing walks the order along it.

Equations

• DescriptiveComplexity.ordEnum A = monoEquivOfFin A ⋯

theorem DescriptiveComplexity.isBot_ordEnum_zero {A : Type} [LinearOrder A] [Finite A] (h : 0 < Nat.card A) : IsBot ((ordEnum A) ⟨0, h⟩)

theorem DescriptiveComplexity.isTop_ordEnum_last {A : Type} [LinearOrder A] [Finite A] (h : 0 < Nat.card A) : IsTop ((ordEnum A) ⟨Nat.card A - 1, ⋯⟩)

theorem DescriptiveComplexity.ordEnum_lt_succ {A : Type} [LinearOrder A] [Finite A] {k : ℕ} (h : k + 1 < Nat.card A) : (ordEnum A) ⟨k, ⋯⟩ < (ordEnum A) ⟨k + 1, h⟩

theorem DescriptiveComplexity.ordEnum_covBy {A : Type} [LinearOrder A] [Finite A] {k : ℕ} (h : k + 1 < Nat.card A) (a : A) : ¬((ordEnum A) ⟨k, ⋯⟩ < a ∧ a < (ordEnum A) ⟨k + 1, h⟩)

Uniqueness of the elements the guards pin down

theorem DescriptiveComplexity.eq_of_isBot {A : Type} [LinearOrder A] {a b : A} (ha : IsBot a) (hb : IsBot b) : a = b

theorem DescriptiveComplexity.canon_ext {A : Type} [LinearOrder A] {D m : ℕ} {u u' : Fin D → A} (h : Canon m u) (h' : Canon m u') (hag : ∀ (j : Fin D), ↑j < m → u j = u' j) : u = u'

theorem DescriptiveComplexity.cov_unique {A : Type} [LinearOrder A] {a b b' : A} (h1 : a < b) (h2 : ∀ (c : A), ¬(a < c ∧ c < b)) (h1' : a < b') (h2' : ∀ (c : A), ¬(a < c ∧ c < b')) : b = b'

theorem DescriptiveComplexity.not_isTop_of_lt {A : Type} [LinearOrder A] {a b : A} (h : a < b) : ¬IsTop a

theorem DescriptiveComplexity.canon_mono {A : Type} [LinearOrder A] {D m m' : ℕ} {u : Fin D → A} (h : Canon m u) (hm : m ≤ m') : Canon m' u

The elements of the drawing

noncomputable def DescriptiveComplexity.botOrd (A : Type) [LinearOrder A] [Finite A] [Nonempty A] : A

The least element of the input order.

Equations

• DescriptiveComplexity.botOrd A = (DescriptiveComplexity.ordEnum A) ⟨0, ⋯⟩

noncomputable def DescriptiveComplexity.botTup {L : FirstOrder.Language} (V : L.FinVocab) (A : Type) [LinearOrder A] [Finite A] [Nonempty A] : Fin (dimOf V) → A

The canonically padded tuple every unindexed element of the drawing carries.

Equations

• DescriptiveComplexity.botTup V A x✝ = DescriptiveComplexity.botOrd A

theorem DescriptiveComplexity.isBot_botA {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : IsBot (botOrd A)

theorem DescriptiveComplexity.canon_botTup {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (m : ℕ) : Canon m (botTup V A)

theorem DescriptiveComplexity.ordEnum_zero {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : (ordEnum A) ⟨0, ⋯⟩ = botOrd A

noncomputable def DescriptiveComplexity.bitPt {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (i : Fin V.numSyms) (u : Fin (dimOf V) → A) : (codeProgInterp V cP).Map A

The element carrying the bit of a tuple: the shared succ element if the symbol holds of it, the shared zero element if it does not.

Equations

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

noncomputable def DescriptiveComplexity.chainPt {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) (A : Type) [LinearOrder A] [Finite A] [Nonempty A] (i : Fin V.numSyms) (l : Fin (dimOf V)) (u : Fin (dimOf V) → A) (k : ℕ) : (codeProgInterp V cP).Map A

The element standing at position k of the level-l chain of the block of the symbol i, above the prefix u.

Equations

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

noncomputable def DescriptiveComplexity.levelPt {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (i : Fin V.numSyms) : ℕ → (Fin (dimOf V) → A) → (codeProgInterp V cP).Map A

The element whose value is that of DescriptiveComplexity.levelVal: the bit at the bottom, the head of the next chain above it.

Equations

• DescriptiveComplexity.levelPt V cP A i 0 x✝ = DescriptiveComplexity.bitPt V cP A i x✝
• DescriptiveComplexity.levelPt V cP A i m.succ x✝ = DescriptiveComplexity.chainPt V cP A i ⟨DescriptiveComplexity.dimOf V - (m + 1), ⋯⟩ x✝ 0

noncomputable def DescriptiveComplexity.numPt {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) (A : Type) [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) : (codeProgInterp V cP).Map A

The element standing at position k of the numeral chain.

Equations

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

noncomputable def DescriptiveComplexity.symPt {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) (A : Type) [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) : (codeProgInterp V cP).Map A

The element standing at the symbol k of the chain of blocks.

Equations

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

The two shared leaves

theorem DescriptiveComplexity.decodesTo_zeroPt {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : DecodesTo (progPt ProgTag.zeroN (botTup V A)) Nat.Partrec.Code.zero

theorem DescriptiveComplexity.decodesTo_onePt {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : DecodesTo (progPt ProgTag.oneN (botTup V A)) Nat.Partrec.Code.succ

The chains of the blocks

theorem DescriptiveComplexity.canon_setCo {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [LinearOrder A] {m j : ℕ} (hj : j < m) (a : A) {u : Fin (dimOf V) → A} (h : Canon m u) : Canon m (setCo V j a u)

theorem DescriptiveComplexity.setCo_at {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} (l : Fin (dimOf V)) (a : A) (t : Fin (dimOf V) → A) : setCo V (↑l) a t l = a

theorem DescriptiveComplexity.setCo_at_fz {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} (a : A) (t : Fin (dimOf V) → A) : setCo V 0 a t (CodeProgRed.fz V) = a

theorem DescriptiveComplexity.setCo_bot_at {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (l : Fin (dimOf V)) {u : Fin (dimOf V) → A} (h : IsBot (u l)) : setCo V (↑l) (botOrd A) u = u

theorem DescriptiveComplexity.okOn_chainN {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [LinearOrder A] (i : Fin V.numSyms) (l : Fin (dimOf V)) (u : Fin (dimOf V) → A) : OkOn (ProgTag.chainN i l) u ↔ Canon (↑l + 1) u

theorem DescriptiveComplexity.cArg1_chainPt {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (i : Fin V.numSyms) (l : Fin (dimOf V)) (m : ℕ) (hm : ↑l + m + 1 = dimOf V) {uk : Fin (dimOf V) → A} (hok : Canon (↑l + 1) uk) : CArg1 (progPt (ProgTag.chainN i l) uk) (levelPt V cP A i m uk)

theorem DescriptiveComplexity.cArg2_chainPt {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (i : Fin V.numSyms) (l : Fin (dimOf V)) {u : Fin (dimOf V) → A} (hu : Canon (↑l) u) (k : ℕ) (hk : k < Nat.card A) : CArg2 (progPt (ProgTag.chainN i l) (setCo V (↑l) ((ordEnum A) ⟨k, hk⟩) u)) (chainPt V cP A i l u (k + 1))

theorem DescriptiveComplexity.decodesTo_levelPt {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (m : ℕ) : m ≤ dimOf V → ∀ (i : Fin V.numSyms) (u : Fin (dimOf V) → A), Canon (dimOf V - m) u → DecodesTo (levelPt V cP A i m u) (levelCode V (Nat.card A) (⇑(ordEnum A)) i m u)

Every level of a block is drawn: the chain that walks the coordinate dimOf V - m draws the nest of the values below it. The induction is on the level, and inside it on the position along the chain, downwards from its tail.

theorem DescriptiveComplexity.decodesTo_blockPt {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (cP : Nat.Partrec.Code) (i : Fin V.numSyms) : DecodesTo (progPt (ProgTag.chainN i ⟨0, ⋯⟩) (botTup V A)) (blockCode V (Nat.card A) (⇑(ordEnum A)) (botTup V A) i)

The head of the chains of a block draws the block.

The chain of the blocks of the symbols

theorem DescriptiveComplexity.decodesTo_symPt {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (j k : ℕ) : k + j = V.numSyms → DecodesTo (symPt V cP A k) (codeNestFrom (blockCode V (Nat.card A) (⇑(ordEnum A)) (botTup V A)) k)

The numeral chain

theorem DescriptiveComplexity.decodesTo_numPt {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (j k : ℕ) : k + j = Nat.card A → DecodesTo (numPt V cP A k) (numCode (Nat.card A - k))

The whole instance

theorem DescriptiveComplexity.decodesTo_pairPt {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (cP : Nat.Partrec.Code) : DecodesTo (progPt ProgTag.pairN (botTup V A)) ((numCode (Nat.card A)).pair (codeNestFrom (blockCode V (Nat.card A) (⇑(ordEnum A)) (botTup V A)) 0))

The element of the pair draws the numeral of the universe size beside the nest of the tables.

theorem DescriptiveComplexity.decodesTo_rootPt {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (cP : Nat.Partrec.Code) : DecodesTo (progPt ProgTag.root (botTup V A)) (cP.comp ((numCode (Nat.card A)).pair (codeNestFrom (blockCode V (Nat.card A) (⇑(ordEnum A)) (botTup V A)) 0)))

The root of the drawn instance draws the intended program: the fixed procedure cP, composed with the pair of the numeral of the universe size and the nest of the tables.

The drawing is well formed

theorem DescriptiveComplexity.progPt_congr {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} {t t' : ProgTag V cP} {u u' : Fin (dimOf V) → A} (h : t = t') (h2 : u = u') : progPt t u = progPt t' u'

theorem DescriptiveComplexity.canon0_ext {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [LinearOrder A] {u u' : Fin (dimOf V) → A} (h : Canon 0 u) (h' : Canon 0 u') : u = u'

theorem DescriptiveComplexity.canon_one_bot {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [LinearOrder A] {u : Fin (dimOf V) → A} (h1 : Canon 1 u) (h0 : IsBot (u (CodeProgRed.fz V))) : Canon 0 u

theorem DescriptiveComplexity.okOn_numN {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [LinearOrder A] (u : Fin (dimOf V) → A) : OkOn ProgTag.numN u ↔ Canon 1 u

theorem DescriptiveComplexity.arg1_det {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [L.Structure A] [LinearOrder A] {ta tb tb' : ProgTag V cP} {ua ub ub' : Fin (dimOf V) → A} (hob : OkOn tb ub) (hob' : OkOn tb' ub') (h : Arg1On ta tb ua ub) (h' : Arg1On ta tb' ua ub') : progPt tb ub = progPt tb' ub'

The first child of an element is unique.

theorem DescriptiveComplexity.arg2_det {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [LinearOrder A] {ta tb tb' : ProgTag V cP} {ua ub ub' : Fin (dimOf V) → A} (hob : OkOn tb ub) (hob' : OkOn tb' ub') (h : Arg2On ta tb ua ub) (h' : Arg2On ta tb' ua ub') : progPt tb ub = progPt tb' ub'

The second child of an element is unique.

theorem DescriptiveComplexity.codeWF_codeProg {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) (A : Type) [L.Structure A] [LinearOrder A] : CodeWF ((codeProgInterp V cP).Map A)

The drawn instance is well formed: at most one constructor mark per element and functional child relations, which is what makes what an element draws unique.