One round of a variable's loop at an arbitrary file

DescriptiveComplexity.Problems.Wide.DrawInstRound read at a coarse file: the inner gates of a round (their file tests, their families and their flags), the control the round folds and the round's two runs. Everything below it is already at the file, so this is the last layer before the variable's loop.

One inner gate block, in the sequencer's shape

The concrete thread over the levels

noncomputable def DescriptiveComplexity.Draw.Data.ixIGTest {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] {I : Type} (F : LaidFile dt A R P I) (zero one : A) (stV : TapeSt dt A R P I) (b : Fin dt.ko ⊕ Fin dt.ki) (u : I) : Prop

The file-test question of an inner gate, semantically: every cell of the gated block that the round's register holds is encoding-shaped.

Equations

• dt.ixIGTest F zero one stV b u = dt.wellShapedIG zero one b (dt.ixBack F.toLayout zero one ⋯ stV (F.cell u))

noncomputable def DescriptiveComplexity.Draw.Data.ixIGFs {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : ℕ → dt.CtlIx → A

The control thread across one round's inner gates: each level's machinery entered through the pack's enterIGSt – the first level resetting the two flags – its conjoining exit the next level's input where the file test passes, the fail store where it does not.

Equations

• One or more equations did not get rendered due to their size.
• dt.ixIGFs F zero one hhas vi stV v f₀ 0 = f₀

noncomputable def DescriptiveComplexity.Draw.Data.ixIGPassP {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] (zero one : A) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)) : Prop

What one level's gate is worth: the file test passed, the block value's witness one-hot at the dispatched tag, and the domain condition there. By DescriptiveComplexity.Draw.Data.igVerdict_iff_isEnc this is IsEnc of the block value, once the encoding layer relates the test's marks to the true shapes.

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixIGPassP_congr {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] (zero one : A) (vi : dt.VarIx) {st st' : TapeSt dt A R P I} (hval : st.val = st'.val) (ℓ : Fin (dt.nIn vi)) : dt.ixIGPassP F zero one vi st ℓ ↔ dt.ixIGPassP F zero one vi st' ℓ

A round's pass depends on the VAL register alone. Hence at a round state (DescriptiveComplexity.Draw.Data.roundSt, which sets VAL and keeps everything else) the pass is the same proposition at every position of the spine – so a position's hp is the entry state's, and kindSemCast may carry the pack it unlocks.

The rides: what the round's machinery never writes

The two-flag characterization

theorem DescriptiveComplexity.Draw.Data.ixRoundPass_of_flags {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (hzo : zero ≠ one) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) (h : dt.ctlBit one (dt.ixIGFs F zero one hhas vi stV v f₀ (dt.nIn vi)) dt.existGateC ∧ dt.ctlBit one (dt.ixIGFs F zero one hhas vi stV v f₀ (dt.nIn vi)) dt.allGateC) (ℓ : Fin (dt.nIn vi)) : dt.ixIGPassP F zero one vi stV ℓ

The branch's guard delivers the pass: with both flags set after the inner gates' thread, every quantified level passed its gate – what unlocks the round's semantic pack.

noncomputable def DescriptiveComplexity.Draw.Data.ixRoundCtl {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (hzo : zero ≠ one) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.IxKindSem zero one vi stV elt (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control one round leaves at the fold checkpoint: the matrix thread applied to the inner gates' output at a passing round – both flags set, the round's conditional semantic pack unlocked by DescriptiveComplexity.Draw.Data.roundPass_of_flags – and the gates' output alone at a skipping one. The pack must be conditional: a garbage round holds no encodings to build one from, and its matrix never runs.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixRoundEndSt {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : TapeSt dt A R P I

The state one round leaves: the matrix runs on the passing branch only, so the round's exit state is the matrix's threaded state there and the entry state at a skipping round.

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixRoundEndSt_eq {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : dt.ixRoundEndSt F zero one hhas vi stV v f₀ = { mir := stV.mir, tgt := (dt.ixRoundEndSt F zero one hhas vi stV v f₀).tgt, sav := (dt.ixRoundEndSt F zero one hhas vi stV v f₀).sav, val := stV.val, old := stV.old, new := stV.new, wk := stV.wk, bot := stV.bot, ltp := stV.ltp }

A round's exit state is its entry state with the two scratch registers rewritten – the sharpening of DescriptiveComplexity.Draw.Data.roundEndSt_fields, and what lets the VAL loop thread those two registers rather than the whole state.

noncomputable def DescriptiveComplexity.Draw.Data.ixRoundCtlT {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (hzo : zero ≠ one) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.IxKindSem zero one vi (dt.ixMatSt vi stV v ↑a) elt (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control one round leaves, threaded: as DescriptiveComplexity.Draw.Data.roundCtl, with the matrix's thread taken at the states its atoms run at.

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixRoundCtl_congr_scratch {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (hzo : zero ≠ one) {v : Univ A R P dt.KIx dt.dd → Prop} {stV stV' : TapeSt dt A R P I} (h : dt.ScratchEq stV stV') (hreg : ¬∃ (u : I), v = F.cell u) (vi : dt.VarIx) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.IxKindSem zero one vi stV elt (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : dt.ixRoundCtl F hinj hhas helt hzo vi stV v sem f₀ = dt.ixRoundCtl F hinj hhas helt hzo vi stV' v (fun (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV' ℓ) (a : Fin (dt.natOf vi)) => dt.ixKindSemCast zero one vi ⋯ ⋯ (dt.kindOf vi a) (sem ⋯ a)) f₀

A round is blind to the two scratch registers: its gates by igFs_congr_scratch, its matrix by matFs_congr_scratch.

theorem DescriptiveComplexity.Draw.Data.ixRoundCtlT_eq_ixRoundCtl {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (hzo : zero ≠ one) {v : Univ A R P dt.KIx dt.dd → Prop} (hreg : ¬∃ (u : I), v = F.cell u) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.IxKindSem zero one vi (dt.ixMatSt vi stV v ↑a) elt (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : dt.ixRoundCtlT F hinj hhas helt hzo vi stV v sem f₀ = dt.ixRoundCtl F hinj hhas helt hzo vi stV v (fun (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) (a : Fin (dt.natOf vi)) => dt.ixKindSemCast zero one vi ⋯ ⋯ (dt.kindOf vi a) (sem hp a)) f₀

The threaded round is the unthreaded one: the gates decide the branch off the same registers, and on the passing branch the matrix threads SAV and TARGET alone (matFsT_eq_matFs). With this the control the run produces is the control the semantic capstone (DescriptiveComplexity.Draw.Data.accVerdict_leafP) is stated at.

The inner gates' run

The whole round, at the program's own rules

noncomputable def DescriptiveComplexity.Draw.Data.ixRoundCost {L : FirstOrder.Language} (dt : Data L) (A : Type) (vi : dt.VarIx) (w wP wR wK : ℕ) : ℕ

What one round of the VAL loop is charged: the walk-back, the inner gates, the walk-back at the branch checkpoint, the branching dispatch and its walk-back, the matrix, and the walk-back at the fold checkpoint. The skipping branch is shorter and is charged the same.

Equations

• dt.ixRoundCost A vi w wP wR wK = 1 + ((dt.ixGateCost A w wP + 2) * dt.nIn vi + 1) + 1 + 1 + 1 + ((dt.ixMatCost A vi w wP wR wK + 2) * dt.natOf vi + 1) + 1