Unrestricted depth-three lower bound: tape encoding

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/TapeEncoding.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister : Type

The 32 registers used by the explicit multitape evaluator.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister = Fin 32

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.input : TapeRegister

Register 0, reserved for input.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.input = 0

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.length : TapeRegister

Register 1, reserved for length.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.length = 1

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.dataLength : TapeRegister

Register 2, reserved for data length.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.dataLength = 2

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.ringDegree : TapeRegister

Register 3, reserved for ring degree.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.ringDegree = 3

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.coeffCount : TapeRegister

Register 4, reserved for coeff count.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.coeffCount = 4

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.candidate : TapeRegister

Register 5, reserved for candidate.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.candidate = 5

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.powerTarget : TapeRegister

Register 6, reserved for power target.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.powerTarget = 6

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.powerScratch : TapeRegister

Register 7, reserved for power scratch.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.powerScratch = 7

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.requiredLength : TapeRegister

Register 8, reserved for required length.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.requiredLength = 8

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.loop0 : TapeRegister

Register 9, reserved for loop0.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.loop0 = 9

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.loop1 : TapeRegister

Register 10, reserved for loop1.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.loop1 = 10

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.loop2 : TapeRegister

Register 11, reserved for loop2.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.loop2 = 11

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.loop3 : TapeRegister

Register 12, reserved for loop3.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.loop3 = 12

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.loop4 : TapeRegister

Register 13, reserved for loop4.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.loop4 = 13

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.loop5 : TapeRegister

Register 14, reserved for loop5.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.loop5 = 14

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.dataBits : TapeRegister

Register 15, reserved for data bits.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.dataBits = 15

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.keyBits : TapeRegister

Register 16, reserved for key bits.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.keyBits = 16

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.polyBits : TapeRegister

Register 17, reserved for poly bits.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.polyBits = 17

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.coeffBits : TapeRegister

Register 18, reserved for coeff bits.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.coeffBits = 18

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.hashBits : TapeRegister

Register 19, reserved for hash bits.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.hashBits = 19

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.accumBits : TapeRegister

Register 20, reserved for accum bits.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.accumBits = 20

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.productBits : TapeRegister

Register 21, reserved for product bits.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.productBits = 21

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.indexA : TapeRegister

Register 22, reserved for index a.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.indexA = 22

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.indexB : TapeRegister

Register 23, reserved for index b.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.indexB = 23

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.indexC : TapeRegister

Register 24, reserved for index c.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.indexC = 24

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.scratchA : TapeRegister

Register 25, reserved for scratch a.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.scratchA = 25

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.scratchB : TapeRegister

Register 26, reserved for scratch b.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.scratchB = 26

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.scratchC : TapeRegister

Register 27, reserved for scratch c.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.scratchC = 27

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.savedCount : TapeRegister

Register 28, reserved for saved count.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.savedCount = 28

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.temp0 : TapeRegister

Register 29, reserved for temp0.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.temp0 = 29

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.temp1 : TapeRegister

Register 30, reserved for temp1.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.temp1 = 30

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRegister.temp2 : TapeRegister

Register 31, reserved for temp2.

Equations

• Complexity.DepthThreeLowerBound.TapeRegister.temp2 = 31

inductive Complexity.DepthThreeLowerBound.TapeAtom : Type

Tape atoms for blank cells, boundaries, register delimiters, and bits.

• blank : TapeAtom
• home : TapeAtom
• delimiter (r : TapeRegister) : TapeAtom
• bit (b : Bool) : TapeAtom
• endMark : TapeAtom

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom : DecidableEq TapeAtom

Equations

• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom = Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq

def Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq (x✝ x✝¹ : TapeAtom) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq Complexity.DepthThreeLowerBound.TapeAtom.blank Complexity.DepthThreeLowerBound.TapeAtom.blank = isTrue ⋯
• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq Complexity.DepthThreeLowerBound.TapeAtom.blank (Complexity.DepthThreeLowerBound.TapeAtom.delimiter r) = isFalse ⋯
• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq Complexity.DepthThreeLowerBound.TapeAtom.blank (Complexity.DepthThreeLowerBound.TapeAtom.bit b) = isFalse ⋯
• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq Complexity.DepthThreeLowerBound.TapeAtom.home Complexity.DepthThreeLowerBound.TapeAtom.home = isTrue ⋯
• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq Complexity.DepthThreeLowerBound.TapeAtom.home (Complexity.DepthThreeLowerBound.TapeAtom.delimiter r) = isFalse ⋯
• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq Complexity.DepthThreeLowerBound.TapeAtom.home (Complexity.DepthThreeLowerBound.TapeAtom.bit b) = isFalse ⋯
• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq (Complexity.DepthThreeLowerBound.TapeAtom.delimiter r) Complexity.DepthThreeLowerBound.TapeAtom.blank = isFalse ⋯
• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq (Complexity.DepthThreeLowerBound.TapeAtom.delimiter r) Complexity.DepthThreeLowerBound.TapeAtom.home = isFalse ⋯
• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq (Complexity.DepthThreeLowerBound.TapeAtom.delimiter r) (Complexity.DepthThreeLowerBound.TapeAtom.bit b) = isFalse ⋯
• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq (Complexity.DepthThreeLowerBound.TapeAtom.delimiter r) Complexity.DepthThreeLowerBound.TapeAtom.endMark = isFalse ⋯
• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq (Complexity.DepthThreeLowerBound.TapeAtom.bit b) Complexity.DepthThreeLowerBound.TapeAtom.blank = isFalse ⋯
• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq (Complexity.DepthThreeLowerBound.TapeAtom.bit b) Complexity.DepthThreeLowerBound.TapeAtom.home = isFalse ⋯
• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq (Complexity.DepthThreeLowerBound.TapeAtom.bit b) (Complexity.DepthThreeLowerBound.TapeAtom.delimiter r) = isFalse ⋯
• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq (Complexity.DepthThreeLowerBound.TapeAtom.bit b) Complexity.DepthThreeLowerBound.TapeAtom.endMark = isFalse ⋯
• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq Complexity.DepthThreeLowerBound.TapeAtom.endMark (Complexity.DepthThreeLowerBound.TapeAtom.delimiter r) = isFalse ⋯
• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq Complexity.DepthThreeLowerBound.TapeAtom.endMark (Complexity.DepthThreeLowerBound.TapeAtom.bit b) = isFalse ⋯
• Complexity.DepthThreeLowerBound.instDecidableEqTapeAtom.decEq Complexity.DepthThreeLowerBound.TapeAtom.endMark Complexity.DepthThreeLowerBound.TapeAtom.endMark = isTrue ⋯

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.instFintypeTapeAtom : Fintype TapeAtom

Equations

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

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.instInhabitedTapeAtom : Inhabited TapeAtom

Equations

• Complexity.DepthThreeLowerBound.instInhabitedTapeAtom = { default := Complexity.DepthThreeLowerBound.instInhabitedTapeAtom.default }

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeMark : Type

The four marker positions carried by each tape symbol.

Equations

• Complexity.DepthThreeLowerBound.TapeMark = Fin 4

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeSymbol : Type

A tape atom together with four Boolean marker flags.

Equations

• Complexity.DepthThreeLowerBound.TapeSymbol = (Complexity.DepthThreeLowerBound.TapeAtom × (Complexity.DepthThreeLowerBound.TapeMark → Bool))

def Complexity.DepthThreeLowerBound.cleanAtom (a : TapeAtom) : TapeSymbol

A tape atom with all marker flags cleared.

Equations

• Complexity.DepthThreeLowerBound.cleanAtom a = (a, fun (x : Complexity.DepthThreeLowerBound.TapeMark) => false)

def Complexity.DepthThreeLowerBound.blankSymbol : TapeSymbol

The blank tape atom with no marker flags.

Equations

• Complexity.DepthThreeLowerBound.blankSymbol = Complexity.DepthThreeLowerBound.cleanAtom Complexity.DepthThreeLowerBound.TapeAtom.blank

def Complexity.DepthThreeLowerBound.rawInputSymbol (b : Bool) : TapeSymbol

Encode an input bit with no marker flags.

Equations

• Complexity.DepthThreeLowerBound.rawInputSymbol b = Complexity.DepthThreeLowerBound.cleanAtom (Complexity.DepthThreeLowerBound.TapeAtom.bit b)

@[simp]

theorem Complexity.DepthThreeLowerBound.cleanAtom_atom (a : TapeAtom) : (cleanAtom a).1 = a

@[simp]

theorem Complexity.DepthThreeLowerBound.cleanAtom_mark (a : TapeAtom) (m : TapeMark) : (cleanAtom a).2 m = false

@[simp]

theorem Complexity.DepthThreeLowerBound.default_tapeSymbol : default = blankSymbol

theorem Complexity.DepthThreeLowerBound.cleanAtom_injective : Function.Injective cleanAtom

theorem Complexity.DepthThreeLowerBound.rawInputSymbol_injective : Function.Injective rawInputSymbol

@[simp]

theorem Complexity.DepthThreeLowerBound.rawInputSymbol_ne_blank (b : Bool) : rawInputSymbol b ≠ blankSymbol

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeStore : Type

A bit-list value for each register.

Equations

• Complexity.DepthThreeLowerBound.TapeStore = (Complexity.DepthThreeLowerBound.TapeRegister → List Bool)

def Complexity.DepthThreeLowerBound.tapeRegisters : List TapeRegister

Enumerate all 32 tape registers.

Equations

• Complexity.DepthThreeLowerBound.tapeRegisters = List.ofFn id

@[simp]

theorem Complexity.DepthThreeLowerBound.tapeRegisters_length : tapeRegisters.length = 32

@[simp]

theorem Complexity.DepthThreeLowerBound.mem_tapeRegisters (r : TapeRegister) : r ∈ tapeRegisters

theorem Complexity.DepthThreeLowerBound.tapeRegisters_nodup : tapeRegisters.Nodup

def Complexity.DepthThreeLowerBound.encodeInput (bits : List Bool) : List TapeSymbol

Encode input bits as unmarked tape symbols.

Equations

• Complexity.DepthThreeLowerBound.encodeInput bits = List.map Complexity.DepthThreeLowerBound.rawInputSymbol bits

@[simp]

theorem Complexity.DepthThreeLowerBound.encodeInput_length (bits : List Bool) : (encodeInput bits).length = bits.length

def Complexity.DepthThreeLowerBound.encodeBlock (σ : TapeStore) (r : TapeRegister) : List TapeSymbol

Encode one register's bit-list block with its delimiter.

Equations

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

def Complexity.DepthThreeLowerBound.encodeStore (σ : TapeStore) : List TapeSymbol

Concatenate the encoded blocks of the tape store.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.encodeBlock_length (σ : TapeStore) (r : TapeRegister) : (encodeBlock σ r).length = (σ r).length + 1

theorem Complexity.DepthThreeLowerBound.encodeBlocks_length (σ : TapeStore) (rs : List TapeRegister) : (List.flatMap (encodeBlock σ) rs).length = rs.length + (List.map (fun (r : TapeRegister) => (σ r).length) rs).sum

theorem Complexity.DepthThreeLowerBound.encodeStore_length (σ : TapeStore) : (encodeStore σ).length = 34 + (List.map (fun (r : TapeRegister) => (σ r).length) tapeRegisters).sum

@[simp]

theorem Complexity.DepthThreeLowerBound.encodeStore_head? (σ : TapeStore) : (encodeStore σ).head? = some (cleanAtom TapeAtom.home)

@[simp]

theorem Complexity.DepthThreeLowerBound.encodeStore_ne_nil (σ : TapeStore) : encodeStore σ ≠ []

theorem Complexity.DepthThreeLowerBound.encodeInput_symbols {bits : List Bool} {s : TapeSymbol} (hs : s ∈ encodeInput bits) : (∃ (b : Bool), s.1 = TapeAtom.bit b) ∧ ∀ (m : TapeMark), s.2 m = false

theorem Complexity.DepthThreeLowerBound.encodeBlock_symbols {σ : TapeStore} {r : TapeRegister} {s : TapeSymbol} (hs : s ∈ encodeBlock σ r) : s.1 ≠ TapeAtom.blank ∧ s.1 ≠ TapeAtom.home ∧ s.1 ≠ TapeAtom.endMark ∧ ∀ (m : TapeMark), s.2 m = false

theorem Complexity.DepthThreeLowerBound.encodeBlocks_symbols {σ : TapeStore} {rs : List TapeRegister} {s : TapeSymbol} (hs : s ∈ List.flatMap (encodeBlock σ) rs) : s.1 ≠ TapeAtom.blank ∧ s.1 ≠ TapeAtom.home ∧ s.1 ≠ TapeAtom.endMark ∧ ∀ (m : TapeMark), s.2 m = false

theorem Complexity.DepthThreeLowerBound.encodeStore_no_blank {σ : TapeStore} {s : TapeSymbol} (hs : s ∈ encodeStore σ) : s.1 ≠ TapeAtom.blank

theorem Complexity.DepthThreeLowerBound.encodeStore_clean {σ : TapeStore} {s : TapeSymbol} (hs : s ∈ encodeStore σ) (m : TapeMark) : s.2 m = false

theorem Complexity.DepthThreeLowerBound.encodeStore_tail_no_home {σ : TapeStore} {s : TapeSymbol} (hs : s ∈ (encodeStore σ).tail) : s.1 ≠ TapeAtom.home