Block and wire layout of the uniform tableau circuit

For a multi-tape Turing machine with k work tapes and state type State running for T steps on inputs of length n, the uniform tableau circuit (Complexity/Computability/Circuit/Boolean/Tableau/Basic.lean) has n input wires, two constant gates (false at wire n and true at wire n + 1), and T + 1 blocks of blockSize k State T gates. Work-tape cells -T, …, T and input positions 0, …, n + 1 share numCols T = 2 T + 1 columns. Within each block, gates are arranged into four regions:

• the scan (ScanLoc), repeated across the 2 T + 1 columns;
• the global gates (GlobLoc): conjunctions for situations and disjunctions for action attributes (Attr);
• the global feature gadgets (GFeat), sixteen gates per state or output view;
• the column feature gadgets (ColFeat), sixteen gates per column feature in each column.

Gates refer to earlier wires symbolically (Ref, ColSel, Guard), and Ref.resolve translates each symbolic reference to a concrete wire index via wire. Every region position has an index (idx, Loc.offset) and an arithmetic decoder (ofIdx, gadgetB, gadgetJ) that invert each other on valid indices, so every gate index 2 ≤ g < numGates k State T sits at a unique admissible block position (div_mod_wire, exists_wire_eq).

Main definitions

• Cslib.Circuits.Boolean.Tableau.Attr, Cslib.Circuits.Boolean.Tableau.ColFeat, Cslib.Circuits.Boolean.Tableau.GFeat, Cslib.Circuits.Boolean.Tableau.ScanQ, Cslib.Circuits.Boolean.Tableau.ScanLoc, Cslib.Circuits.Boolean.Tableau.GlobLoc, Cslib.Circuits.Boolean.Tableau.Loc: positions within a tableau block.
• Cslib.Circuits.Boolean.Tableau.ColSel, Cslib.Circuits.Boolean.Tableau.Guard, Cslib.Circuits.Boolean.Tableau.Ref: symbolic wire references relative to a block and column.
• Cslib.Circuits.Boolean.Tableau.blockSize, Cslib.Circuits.Boolean.Tableau.numGates, Cslib.Circuits.Boolean.Tableau.Loc.offset, Cslib.Circuits.Boolean.Tableau.wire, Cslib.Circuits.Boolean.Tableau.Ref.resolve: numerical layout and wire resolution.
• Cslib.Circuits.Boolean.Tableau.ScanLoc.ofIdx, Cslib.Circuits.Boolean.Tableau.GlobLoc.ofIdx, Cslib.Circuits.Boolean.Tableau.GFeat.ofIdx, Cslib.Circuits.Boolean.Tableau.ColFeat.ofIdx: arithmetic decoders for block offsets.

Main results

• Cslib.Circuits.Boolean.Tableau.Loc.offset_lt: every admissible position lies within its block.
• Cslib.Circuits.Boolean.Tableau.div_mod_wire: dividing and reducing a wire index modulo blockSize recovers its time block and intra-block offset.
• Cslib.Circuits.Boolean.Tableau.exists_wire_eq: every gate index after the two constants is the wire of an admissible block position.

References

• R. E. Ladner, The circuit value problem is log space complete for P
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Sections 6.1 and 6.7
• C. H. Papadimitriou, Computational Complexity, Theorem 8.1

Positions within a block

inductive Cslib.Circuits.Boolean.Tableau.Attr (k : ℕ) (State : Type) : Type

One aspect of an action: the next state, the move of the input head, what is written on a work tape, the move of a work head, and the output symbol.

• state {k : ℕ} {State : Type} (q : Option State) : Attr k State

  The next state is q (none to halt).

• inMove {k : ℕ} {State : Type} (m : SignType) : Attr k State

  The input head moves by m.

• write {k : ℕ} {State : Type} (i : Fin k) (w : Option (Option Bool)) : Attr k State

  Work tape i is written w (none to leave the cell).

• move {k : ℕ} {State : Type} (i : Fin k) (m : SignType) : Attr k State

  Work head i moves by m.

• out {k : ℕ} {State : Type} (e : Option Bool) : Attr k State

  The output symbol is e.

def Cslib.Circuits.Boolean.Tableau.instDecidableEqAttr.decEq {k✝ : ℕ} {State✝ : Type} [DecidableEq State✝] (x✝ x✝¹ : Attr k✝ State✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instDecidableEqAttr {k✝ : ℕ} {State✝ : Type} [DecidableEq State✝] : DecidableEq (Attr k✝ State✝)

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instFintypeAttr {k✝ : ℕ} {State✝ : Type} [Fintype State✝] : Fintype (Attr k✝ State✝)

inductive Cslib.Circuits.Boolean.Tableau.ColFeat (k : ℕ) : Type

The features held in each column: the input head, a work head and a work cell.

• inPos {k : ℕ} : ColFeat k

  The input head is at the position of the column.

• head {k : ℕ} (i : Fin k) : ColFeat k

  Work head i is at the cell of the column.

• cell {k : ℕ} (i : Fin k) (s : Option Bool) : ColFeat k

  The cell of the column on work tape i holds s.

def Cslib.Circuits.Boolean.Tableau.instDecidableEqColFeat.decEq {k✝ : ℕ} (x✝ x✝¹ : ColFeat k✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instDecidableEqColFeat {k✝ : ℕ} : DecidableEq (ColFeat k✝)

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instFintypeColFeat {k✝ : ℕ} : Fintype (ColFeat k✝)

inductive Cslib.Circuits.Boolean.Tableau.GFeat (State : Type) : Type

The global features: the state and the view of the output.

• state {State : Type} (q : Option State) : GFeat State

  The state is q (none once halted).

• out {State : Type} (o : Turing.OutView) : GFeat State

  The output written so far has the view o.

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instDecidableEqGFeat {State✝ : Type} [DecidableEq State✝] : DecidableEq (GFeat State✝)

def Cslib.Circuits.Boolean.Tableau.instDecidableEqGFeat.decEq {State✝ : Type} [DecidableEq State✝] (x✝ x✝¹ : GFeat State✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instFintypeGFeat {State✝ : Type} [Fintype State✝] : Fintype (GFeat State✝)

inductive Cslib.Circuits.Boolean.Tableau.ScanQ (k : ℕ) : Type

The quantities accumulated by the scan across the columns: the symbol under the input head and the symbols under the work heads.

• inRead {k : ℕ} (s : Option Bool) : ScanQ k

  The input head reads s.

• read {k : ℕ} (i : Fin k) (s : Option Bool) : ScanQ k

  Work head i reads s.

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instDecidableEqScanQ {k✝ : ℕ} : DecidableEq (ScanQ k✝)

def Cslib.Circuits.Boolean.Tableau.instDecidableEqScanQ.decEq {k✝ : ℕ} (x✝ x✝¹ : ScanQ k✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instFintypeScanQ {k✝ : ℕ} : Fintype (ScanQ k✝)

inductive Cslib.Circuits.Boolean.Tableau.ScanLoc (k : ℕ) : Type

The gates of a column of the scan.

• nh {k : ℕ} (i : Fin k) : ScanLoc k

  Work head i is not at the cell of the column.

• nx {k : ℕ} : ScanLoc k

  The negated input bit of the column.

• term {k : ℕ} (q : ScanQ k) : ScanLoc k

  The contribution of the column to a scanned quantity.

• acc {k : ℕ} (q : ScanQ k) : ScanLoc k

  The disjunction of the contributions of the columns so far.

def Cslib.Circuits.Boolean.Tableau.instDecidableEqScanLoc.decEq {k✝ : ℕ} (x✝ x✝¹ : ScanLoc k✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instDecidableEqScanLoc {k✝ : ℕ} : DecidableEq (ScanLoc k✝)

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instFintypeScanLoc {k✝ : ℕ} : Fintype (ScanLoc k✝)

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.Tableau.numSit (k : ℕ) (State : Type) [Fintype State] : ℕ

The number of situations of a machine.

inductive Cslib.Circuits.Boolean.Tableau.GlobLoc (k : ℕ) (State : Type) [Fintype State] : Type

The global gates: the situations, as chains of conjunctions, and the attributes, as chains of disjunctions over the situations.

• sit {k : ℕ} {State : Type} [Fintype State] (j : Fin (numSit k State)) (i : Fin (k + 1)) : GlobLoc k State

  The conjunction of the first i + 1 conditions of situation number j.

• attr {k : ℕ} {State : Type} [Fintype State] (v : Attr k State) (j : Fin (numSit k State + 1)) : GlobLoc k State

  The disjunction of the first j situations having the attribute v.

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instDecidableEqGlobLoc {k✝ : ℕ} {State✝ : Type} {inst✝ : Fintype State✝} [DecidableEq State✝] : DecidableEq (GlobLoc k✝ State✝)

def Cslib.Circuits.Boolean.Tableau.instDecidableEqGlobLoc.decEq {k✝ : ℕ} {State✝ : Type} {inst✝ : Fintype State✝} [DecidableEq State✝] (x✝ x✝¹ : GlobLoc k✝ State✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instFintypeGlobLoc {k✝ : ℕ} {State✝ : Type} {inst✝ : Fintype State✝} [Fintype State✝] : Fintype (GlobLoc k✝ State✝)

inductive Cslib.Circuits.Boolean.Tableau.Loc (k : ℕ) (State : Type) [Fintype State] : Type

The position of a gate within its block: a gate of the scan, a global gate, or one of the sixteen gates computing a feature from its terms (the conjunction false and the running disjunction true of term j).

• scan {k : ℕ} {State : Type} [Fintype State] (l : ScanLoc k) : Loc k State

  A gate of the scan.

• glob {k : ℕ} {State : Type} [Fintype State] (l : GlobLoc k State) : Loc k State

  A global gate.

• gf {k : ℕ} {State : Type} [Fintype State] (f : GFeat State) (b : Bool) (j : Fin 8) : Loc k State

  A gate computing a global feature.

• col {k : ℕ} {State : Type} [Fintype State] (f : ColFeat k) (b : Bool) (j : Fin 8) : Loc k State

  A gate computing a column feature.

def Cslib.Circuits.Boolean.Tableau.instDecidableEqLoc.decEq {k✝ : ℕ} {State✝ : Type} {inst✝ : Fintype State✝} [DecidableEq State✝] (x✝ x✝¹ : Loc k✝ State✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instDecidableEqLoc {k✝ : ℕ} {State✝ : Type} {inst✝ : Fintype State✝} [DecidableEq State✝] : DecidableEq (Loc k✝ State✝)

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instFintypeLoc {k✝ : ℕ} {State✝ : Type} {inst✝ : Fintype State✝} [Fintype State✝] : Fintype (Loc k✝ State✝)

References to wires

inductive Cslib.Circuits.Boolean.Tableau.ColSel : Type

The column of a reference, relative to the column c of the gate: c, c - 1, c + 1, or the last column.

• same : ColSel

  The column c.

• prev : ColSel

  The column c - 1.

• next : ColSel

  The column c + 1.

• last : ColSel

  The last column.

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instDecidableEqColSel : DecidableEq ColSel

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instFintypeColSel : Fintype ColSel

inductive Cslib.Circuits.Boolean.Tableau.Guard : Type

A condition on the column c of a gate, under which a reference is used; otherwise it reads false.

• always : Guard

  Always.

• pos : Guard

  1 ≤ c.

• ltLast : Guard

  c is not the last column.

• inRange : Guard

  1 ≤ c ≤ n: the column holds an input bit.

• outRange : Guard

  The column holds no input bit.

• isZero : Guard

  c = 0.

• isEnd : Guard

  c = n + 1.

• leEnd : Guard

  1 ≤ c ≤ n + 1.

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instDecidableEqGuard : DecidableEq Guard

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instFintypeGuard : Fintype Guard

inductive Cslib.Circuits.Boolean.Tableau.Ref (k : ℕ) (State : Type) [Fintype State] : Type

A reference to a wire, relative to the block and the column of the gate: the constant wires, the input bit of the column, or a position of the current or the previous block.

• fls {k : ℕ} {State : Type} [Fintype State] : Ref k State

  The constant false.

• tru {k : ℕ} {State : Type} [Fintype State] : Ref k State

  The constant true.

• inp {k : ℕ} {State : Type} [Fintype State] : Ref k State

  The input bit of the column, if it holds one.

• node {k : ℕ} {State : Type} [Fintype State] (prev : Bool) (l : Loc k State) (cs : ColSel) (g : Guard) : Ref k State

  The position l of the previous block (prev = true) or the current one, in the column selected by cs, under the guard g.

def Cslib.Circuits.Boolean.Tableau.instDecidableEqRef.decEq {k✝ : ℕ} {State✝ : Type} {inst✝ : Fintype State✝} [DecidableEq State✝] (x✝ x✝¹ : Ref k✝ State✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instDecidableEqRef {k✝ : ℕ} {State✝ : Type} {inst✝ : Fintype State✝} [DecidableEq State✝] : DecidableEq (Ref k✝ State✝)

def Cslib.Circuits.Boolean.Tableau.Ref.toData {k : ℕ} {State : Type} [Fintype State] : Ref k State → Option (Option (Option (Bool × Loc k State × ColSel × Guard)))

References as data.

instance Cslib.Circuits.Boolean.Tableau.instFiniteRef {k : ℕ} {State : Type} [Fintype State] : Finite (Ref k State)

def Cslib.Circuits.Boolean.Tableau.colF {k : ℕ} {State : Type} [Fintype State] (f : ColFeat k) (cs : ColSel) (g : Guard) : Ref k State

A column feature of the previous block, in the column selected by cs, under the guard g.

def Cslib.Circuits.Boolean.Tableau.gfF {k : ℕ} {State : Type} [Fintype State] (f : GFeat State) : Ref k State

A global feature of the previous block.

def Cslib.Circuits.Boolean.Tableau.act {k : ℕ} {State : Type} [Fintype State] (v : Attr k State) : Ref k State

The attribute v of the action of the current step.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.Tableau.halted {k : ℕ} {State : Type} [Fintype State] : Ref k State

The previous configuration has halted.

def Cslib.Circuits.Boolean.Tableau.scanAt {k : ℕ} {State : Type} [Fintype State] (l : ScanLoc k) (cs : ColSel) (g : Guard) : Ref k State

A gate of the scan of the current block.

The layout

def Cslib.Circuits.Boolean.Tableau.symIdx : Option Bool → ℕ

The number of a cell symbol: blank, false, true.

def Cslib.Circuits.Boolean.Tableau.ScanQ.idx {k : ℕ} : ScanQ k → ℕ

The number of a scanned quantity.

def Cslib.Circuits.Boolean.Tableau.ScanLoc.idx {k : ℕ} : ScanLoc k → ℕ

The position of a gate within a column of the scan.

def Cslib.Circuits.Boolean.Tableau.scanWidth (k : ℕ) : ℕ

The number of gates of a column of the scan.

noncomputable def Cslib.Circuits.Boolean.Tableau.attrIdx {k : ℕ} {State : Type} [Fintype State] (v : Attr k State) : ℕ

The number of an attribute.

noncomputable def Cslib.Circuits.Boolean.Tableau.GlobLoc.idx {k : ℕ} {State : Type} [Fintype State] : GlobLoc k State → ℕ

The position of a global gate.

def Cslib.Circuits.Boolean.Tableau.globWidth (k : ℕ) (State : Type) [Fintype State] : ℕ

The number of global gates.

noncomputable def Cslib.Circuits.Boolean.Tableau.GFeat.idx {State : Type} [Fintype State] : GFeat State → ℕ

The number of a global feature.

def Cslib.Circuits.Boolean.Tableau.ColFeat.idx {k : ℕ} : ColFeat k → ℕ

The number of a column feature.

def Cslib.Circuits.Boolean.Tableau.gadgetIdx (fi : ℕ) (b : Bool) (j : Fin 8) : ℕ

The position of gate j of kind b within the sixteen gates computing feature number fi.

def Cslib.Circuits.Boolean.Tableau.gfWidth (State : Type) [Fintype State] : ℕ

The number of gates computing the global features.

def Cslib.Circuits.Boolean.Tableau.colWidth (k : ℕ) : ℕ

The number of gates computing the features of a column.

def Cslib.Circuits.Boolean.Tableau.numCols (T : ℕ) : ℕ

The number of columns: the work cells -T, …, T.

def Cslib.Circuits.Boolean.Tableau.globStart (k T : ℕ) : ℕ

The start of the global gates within a block.

def Cslib.Circuits.Boolean.Tableau.gfStart (k : ℕ) (State : Type) [Fintype State] (T : ℕ) : ℕ

The start of the global features within a block.

def Cslib.Circuits.Boolean.Tableau.colStart (k : ℕ) (State : Type) [Fintype State] (T : ℕ) : ℕ

The start of the column features within a block.

def Cslib.Circuits.Boolean.Tableau.blockSize (k : ℕ) (State : Type) [Fintype State] (T : ℕ) : ℕ

The number of gates of a block.

def Cslib.Circuits.Boolean.Tableau.numGates (k : ℕ) (State : Type) [Fintype State] (T : ℕ) : ℕ

The number of gates of the tableau: the two constants and T + 1 blocks.

noncomputable def Cslib.Circuits.Boolean.Tableau.Loc.offset {k : ℕ} {State : Type} [Fintype State] (T c : ℕ) : Loc k State → ℕ

The offset of a position in column c from the start of its block.

noncomputable def Cslib.Circuits.Boolean.Tableau.wire {k : ℕ} {State : Type} [Fintype State] (n T t : ℕ) (l : Loc k State) (c : ℕ) : ℕ

The wire of a position l of block t, in column c: the inputs come first, then the two constants, then the blocks.

def Cslib.Circuits.Boolean.Tableau.Guard.test (n T c : ℕ) : Guard → Bool

Whether a guard holds in column c.

def Cslib.Circuits.Boolean.Tableau.ColSel.apply (T c : ℕ) : ColSel → ℕ

The column selected relative to column c.

noncomputable def Cslib.Circuits.Boolean.Tableau.Ref.resolve {k : ℕ} {State : Type} [Fintype State] (n T t c : ℕ) : Ref k State → ℕ

The wire of a reference from block t and column c.

def Cslib.Circuits.Boolean.Tableau.argsOf (op : Op) (a b : ℕ) : List ℕ

The arguments of a gate with operation op, from its two candidate wires.

Decoding positions

def Cslib.Circuits.Boolean.Tableau.symOf (m : ℕ) : Option Bool

The cell symbol with a number.

def Cslib.Circuits.Boolean.Tableau.ScanQ.ofIdx {k : ℕ} (m : ℕ) : ScanQ k

The scanned quantity with a number.

def Cslib.Circuits.Boolean.Tableau.ScanLoc.ofIdx {k : ℕ} (m : ℕ) : ScanLoc k

The gate of the scan at a position within a column.

noncomputable def Cslib.Circuits.Boolean.Tableau.GlobLoc.ofIdx {k : ℕ} {State : Type} [Fintype State] (m : ℕ) : GlobLoc k State

The global gate at a position.

noncomputable def Cslib.Circuits.Boolean.Tableau.GFeat.ofIdx {State : Type} [Fintype State] (m : ℕ) : GFeat State

The global feature with a number.

def Cslib.Circuits.Boolean.Tableau.ColFeat.ofIdx {k : ℕ} (m : ℕ) : ColFeat k

The column feature with a number.

def Cslib.Circuits.Boolean.Tableau.gadgetB (m : ℕ) : Bool

The kind of the gate at a position within the gates of a feature.

def Cslib.Circuits.Boolean.Tableau.gadgetJ (m : ℕ) : Fin 8

The term of the gate at a position within the gates of a feature.

Decoding inverts the layout

theorem Cslib.Circuits.Boolean.Tableau.ScanQ.ofIdx_idx {k : ℕ} (q : ScanQ k) : ofIdx q.idx = q

theorem Cslib.Circuits.Boolean.Tableau.ScanQ.idx_lt {k : ℕ} (q : ScanQ k) : q.idx < 3 + 3 * k

theorem Cslib.Circuits.Boolean.Tableau.ScanLoc.ofIdx_idx {k : ℕ} (l : ScanLoc k) : ofIdx l.idx = l

theorem Cslib.Circuits.Boolean.Tableau.ScanLoc.idx_lt {k : ℕ} (l : ScanLoc k) : l.idx < scanWidth k

theorem Cslib.Circuits.Boolean.Tableau.GlobLoc.idx_lt {k : ℕ} {State : Type} [Fintype State] (l : GlobLoc k State) : l.idx < globWidth k State

theorem Cslib.Circuits.Boolean.Tableau.GlobLoc.ofIdx_idx {k : ℕ} {State : Type} [Fintype State] (l : GlobLoc k State) : ofIdx l.idx = l

theorem Cslib.Circuits.Boolean.Tableau.GFeat.idx_lt {State : Type} [Fintype State] (f : GFeat State) : f.idx < Fintype.card (Option State) + 4

theorem Cslib.Circuits.Boolean.Tableau.GFeat.ofIdx_idx {State : Type} [Fintype State] (f : GFeat State) : ofIdx f.idx = f

theorem Cslib.Circuits.Boolean.Tableau.ColFeat.idx_lt {k : ℕ} (f : ColFeat k) : f.idx < 1 + 4 * k

theorem Cslib.Circuits.Boolean.Tableau.ColFeat.ofIdx_idx {k : ℕ} (f : ColFeat k) : ofIdx f.idx = f

theorem Cslib.Circuits.Boolean.Tableau.gadgetIdx_lt (fi : ℕ) (b : Bool) (j : Fin 8) : gadgetIdx fi b j < 16 * (fi + 1)

theorem Cslib.Circuits.Boolean.Tableau.gadgetIdx_div (fi : ℕ) (b : Bool) (j : Fin 8) : gadgetIdx fi b j / 16 = fi

theorem Cslib.Circuits.Boolean.Tableau.gadgetB_gadgetIdx (fi : ℕ) (b : Bool) (j : Fin 8) : gadgetB (gadgetIdx fi b j) = b

theorem Cslib.Circuits.Boolean.Tableau.gadgetJ_gadgetIdx (fi : ℕ) (b : Bool) (j : Fin 8) : gadgetJ (gadgetIdx fi b j) = j

Block bounds and wire division

def Cslib.Circuits.Boolean.Tableau.Loc.ColOK {k : ℕ} {State : Type} [Fintype State] (T c : ℕ) : Loc k State → Prop

The column c is admissible for the position l: a column of the window for a gate of the scan or a column feature, and 0 for a global gate.

theorem Cslib.Circuits.Boolean.Tableau.scan_offset_lt_globStart {k T c : ℕ} (hc : c < numCols T) (l : ScanLoc k) : c * scanWidth k + l.idx < globStart k T

theorem Cslib.Circuits.Boolean.Tableau.gfStart_add_gadgetIdx_lt {k : ℕ} {State : Type} [Fintype State] {T : ℕ} (f : GFeat State) (b : Bool) (j : Fin 8) : gfStart k State T + gadgetIdx f.idx b j < colStart k State T

theorem Cslib.Circuits.Boolean.Tableau.Loc.offset_lt {k : ℕ} {State : Type} [Fintype State] {T : ℕ} {l : Loc k State} {c : ℕ} (hl : ColOK T c l) : offset T c l < blockSize k State T

A position lies within its block.

theorem Cslib.Circuits.Boolean.Tableau.Loc.offset_lt_of_lt {k : ℕ} {State : Type} [Fintype State] {T : ℕ} {l : Loc k State} {c : ℕ} (hc : c < numCols T) : offset T c l < blockSize k State T

Every position lies within its block, for a column of the window.

theorem Cslib.Circuits.Boolean.Tableau.Loc.ColOK.lt {k : ℕ} {State : Type} [Fintype State] {T : ℕ} {l : Loc k State} {c : ℕ} (hl : ColOK T c l) : c < numCols T

theorem Cslib.Circuits.Boolean.Tableau.scanWidth_pos {k : ℕ} : 0 < scanWidth k

The scan region has positive width, including for a machine with no work tapes.

theorem Cslib.Circuits.Boolean.Tableau.wire_sub {k : ℕ} {State : Type} [Fintype State] (n T t : ℕ) (l : Loc k State) (c : ℕ) : wire n T t l c - n = 2 + t * blockSize k State T + Loc.offset T c l

Subtracting the input offset gives the index of a tableau gate.

theorem Cslib.Circuits.Boolean.Tableau.div_mod_wire {k : ℕ} {State : Type} [Fintype State] {n T t : ℕ} {l : Loc k State} {c : ℕ} (hl : Loc.ColOK T c l) : (wire n T t l c - n - 2) / blockSize k State T = t ∧ (wire n T t l c - n - 2) % blockSize k State T = Loc.offset T c l

Every gate sits at a position

theorem Cslib.Circuits.Boolean.Tableau.ScanQ.idx_ofIdx {k m : ℕ} (hm : m < 3 + 3 * k) : (ofIdx m).idx = m

theorem Cslib.Circuits.Boolean.Tableau.ScanLoc.idx_ofIdx {k m : ℕ} (hm : m < scanWidth k) : (ofIdx m).idx = m

theorem Cslib.Circuits.Boolean.Tableau.GlobLoc.idx_ofIdx {k : ℕ} {State : Type} [Fintype State] {m : ℕ} (hm : m < globWidth k State) : (ofIdx m).idx = m

theorem Cslib.Circuits.Boolean.Tableau.GFeat.idx_ofIdx {State : Type} [Fintype State] {m : ℕ} (hm : m < Fintype.card (Option State) + 4) : (ofIdx m).idx = m

theorem Cslib.Circuits.Boolean.Tableau.ColFeat.idx_ofIdx {k m : ℕ} (hm : m < 1 + 4 * k) : (ofIdx m).idx = m

theorem Cslib.Circuits.Boolean.Tableau.exists_wire_eq {k : ℕ} {State : Type} [Fintype State] {n T g : ℕ} (hg₂ : 2 ≤ g) (hg : g < numGates k State T) : ∃ t ≤ T, ∃ (l : Loc k State) (c : ℕ), Loc.ColOK T c l ∧ wire n T t l c - n = g

Every gate after the constants sits at a position of a block.