Unrestricted depth-three lower bound: tape input guard length #

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

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

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.requiredLength (d r t : ℕ) :

ℕ

Total input length needed for the chosen data, hash, modulus, and coefficient blocks.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.requiredLength d r t = d + (d + r - 1) + r + t * r

Instances For

source

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.requiredLength_parameters (d : ℕ) :

requiredLength d (hashDimension d) (independenceOrder d) = blockLen d

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.outputStore (σ : TapeStore) (d r t : ℕ) :

TapeStore

Tape-store contents at the output stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.outputStore σ d r t = Function.update σ 8 (List.replicate (Complexity.DepthThreeLowerBound.TapeInputGuard.requiredLength d r t) true)

Instances For

source

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.outputStore_length (σ : TapeStore) (d r t : ℕ) :

outputStore σ d r t 8 = List.replicate (requiredLength d r t) true

source

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.outputStore_other (σ : TapeStore) (d r t : ℕ) (q : TapeRegister) (hq : q ≠ 8) :

outputStore σ d r t q = σ q

source

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputGuard.ProductState :

Type

Control states for the product stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.ProductState = (Complexity.DepthThreeLowerBound.TapeCopy.State ⊕ Complexity.DepthThreeLowerBound.TapeMultiply.State)

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.productProgram :

TapeMultiProgram ProductState

Transition function for the product stage of the input guard length routine.

Equations

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

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.productStart :

ProductState

Initial control state of the product stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.productStart = Sum.inl Complexity.DepthThreeLowerBound.TapeCopy.State.start

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.productDone :

ProductState

Terminal control state of the product stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.productDone = Sum.inr Complexity.DepthThreeLowerBound.TapeMultiply.done

Instances For

source

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.runs_product (σ : TapeStore) (t r z : ℕ) (h3 : σ 3 = List.replicate r true) (h4 : σ 4 = List.replicate t true) (h5 : σ 5 = []) (h6 : σ 6 = []) (h8 : σ 8 = List.replicate z true) :

RunsIn productProgram.step (TapeMultiProgram.cfg productStart (storeTapes σ)) (TapeMultiProgram.cfg productDone (storeTapes (Function.update σ 8 (List.replicate (z + t * r) true)))) (t * (10 * r + 14) + 2 * t + 8)

source

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputGuard.RingSumState :

Type

Control states for the ring sum stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.RingSumState = (Complexity.DepthThreeLowerBound.TapeCopyAdd.State ⊕ Complexity.DepthThreeLowerBound.TapeCopyAdd.State)

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.ringSumProgram :

TapeMultiProgram RingSumState

Transition function for the ring sum stage of the input guard length routine.

Equations

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

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.ringSumStart :

RingSumState

Initial control state of the ring sum stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.ringSumStart = Sum.inl Complexity.DepthThreeLowerBound.TapeCopyAdd.start

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.ringSumDone :

RingSumState

Terminal control state of the ring sum stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.ringSumDone = Sum.inr Complexity.DepthThreeLowerBound.TapeCopyAdd.done

Instances For

source

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputGuard.AddSumState :

Type

Control states for the add sum stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.AddSumState = (Complexity.DepthThreeLowerBound.TapeCopyAdd.State ⊕ Complexity.DepthThreeLowerBound.TapeInputGuard.RingSumState)

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.addSumProgram :

TapeMultiProgram AddSumState

Transition function for the add sum stage of the input guard length routine.

Equations

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

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.addSumStart :

AddSumState

Initial control state of the add sum stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.addSumStart = Sum.inl Complexity.DepthThreeLowerBound.TapeCopyAdd.start

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.addSumDone :

AddSumState

Terminal control state of the add sum stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.addSumDone = Sum.inr Complexity.DepthThreeLowerBound.TapeInputGuard.ringSumDone

Instances For

source

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputGuard.SumState :

Type

Control states for the sum stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.SumState = (Complexity.DepthThreeLowerBound.TapeCopy.State ⊕ Complexity.DepthThreeLowerBound.TapeInputGuard.AddSumState)

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.sumProgram :

TapeMultiProgram SumState

Transition function for the sum stage of the input guard length routine.

Equations

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

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.sumStart :

SumState

Initial control state of the sum stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.sumStart = Sum.inl Complexity.DepthThreeLowerBound.TapeCopy.State.start

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.sumDone :

SumState

Terminal control state of the sum stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.sumDone = Sum.inr Complexity.DepthThreeLowerBound.TapeInputGuard.addSumDone

Instances For

source

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.runs_sum (σ : TapeStore) (d r : ℕ) (h2 : σ 2 = List.replicate d true) (h3 : σ 3 = List.replicate r true) (h5 : σ 5 = []) (h8 : σ 8 = []) :

RunsIn sumProgram.step (TapeMultiProgram.cfg sumStart (storeTapes σ)) (TapeMultiProgram.cfg sumDone (storeTapes (Function.update σ 8 (List.replicate (d + d + r + r) true)))) (12 * d + 20 * r + 31)

source

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputGuard.TailState :

Type

Control states for the tail stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.TailState = (Complexity.DepthThreeLowerBound.TapeUnary.DecState ⊕ Complexity.DepthThreeLowerBound.TapeInputGuard.ProductState)

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.tailProgram :

TapeMultiProgram TailState

Transition function for the tail stage of the input guard length routine.

Equations

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

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.tailStart :

TailState

Initial control state of the tail stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.tailStart = Sum.inl Complexity.DepthThreeLowerBound.TapeUnary.DecState.start

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.tailDone :

TailState

Terminal control state of the tail stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.tailDone = Sum.inr Complexity.DepthThreeLowerBound.TapeInputGuard.productDone

Instances For

source

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputGuard.LengthState :

Type

Control states for the length stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.LengthState = (Complexity.DepthThreeLowerBound.TapeInputGuard.SumState ⊕ Complexity.DepthThreeLowerBound.TapeInputGuard.TailState)

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.lengthProgram :

TapeMultiProgram LengthState

Transition function for the length stage of the input guard length routine.

Equations

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

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.lengthStart :

LengthState

Initial control state of the length stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.lengthStart = Sum.inl Complexity.DepthThreeLowerBound.TapeInputGuard.sumStart

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.lengthDone :

LengthState

Terminal control state of the length stage of the input guard length routine.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.lengthDone = Sum.inr Complexity.DepthThreeLowerBound.TapeInputGuard.tailDone

Instances For

source

def Complexity.DepthThreeLowerBound.TapeInputGuard.lengthCost (d r t : ℕ) :

ℕ

Transition budget for the input guard length routine at its length stage.

Equations

Complexity.DepthThreeLowerBound.TapeInputGuard.lengthCost d r t = 12 * d + 20 * r + 16 * t + 10 * (t * r) + 45

Instances For

source

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.runs_length (σ : TapeStore) (d r t : ℕ) (h2 : σ 2 = List.replicate d true) (h3 : σ 3 = List.replicate r true) (h4 : σ 4 = List.replicate t true) (h5 : σ 5 = []) (h6 : σ 6 = []) (h8 : σ 8 = []) :

RunsIn lengthProgram.step (TapeMultiProgram.cfg lengthStart (storeTapes σ)) (TapeMultiProgram.cfg lengthDone (storeTapes (outputStore σ d r t))) (lengthCost d r t)

source

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.lengthProgram_done (h : TapeHeads) :

lengthProgram lengthDone h = none

Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeInputGuardLength

Unrestricted depth-three lower bound: tape input guard length #