Rational hitting lists: procedure control

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

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

def Complexity.RationalHitting.StackLanguage.Procedure.toPort {A B : Type} {ca : A → List Bool} {cb : B → List Bool} {f : A → B} (p : Procedure ca cb f) : Procedure ca cb f

Give a procedure a single external input/output port. The two transfers are real stack programs; scratch registers remain clean.

Equations

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

def Complexity.RationalHitting.StackLanguage.splitPair {K : Type} (a b tmp : K) : Program K

Unpack an encoded pair into the designated registers.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.eval_splitPair {K : Type} [DecidableEq K] {a b tmp : K} (hab : a ≠ b) (hat : a ≠ tmp) (hbt : b ≠ tmp) (x y : List Bool) : Eval (splitPair a b tmp) (single b (codeWord x ++ y)) (both a b x y) (7 * x.length + 10)

theorem Complexity.RationalHitting.StackLanguage.extend_both {K L : Type} [DecidableEq K] [DecidableEq L] (f : K → L) (hf : Function.Injective f) (i j : K) (x y : List Bool) : (Function.extend f (both i j x y) fun (x : L) => []) = both (f i) (f j) x y

def Complexity.RationalHitting.StackLanguage.Procedure.fromBinary {A B C K : Type} [Fintype K] [DecidableEq K] {ca : A → List Bool} {cb : B → List Bool} {cc : C → List Bool} {f : A × B → C} (p : Program K) (i j o : K) (hij : i ≠ j) (bnd : TimeBound) (hp : ∀ (a : A) (b : B), ∃ t ≤ bnd.eval ((ca a).length + (cb b).length + 1), Eval p (both i j (ca a) (cb b)) (single o (cc (f (a, b)))) t) (hs : ∀ (a : A) (b : B), (cc (f (a, b))).length ≤ bnd.eval ((ca a).length + (cb b).length + 1)) : Procedure (pairCode ca cb) cc f

Package an independently proved two-input clean register routine as a serialized procedure. Its polynomial bound is not an operation oracle: the actual Eval proof is required.

Equations

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

def Complexity.RationalHitting.StackLanguage.boolCode (b : Bool) : List Bool

The one-bit encoding of a Boolean value.

Equations

• Complexity.RationalHitting.StackLanguage.boolCode b = [b]

@[simp]

theorem Complexity.RationalHitting.StackLanguage.boolCode_length (b : Bool) : (boolCode b).length = 1

def Complexity.RationalHitting.StackLanguage.Procedure.rename {A B K : Type} [Fintype K] [DecidableEq K] {ca : A → List Bool} {cb : B → List Bool} {f : A → B} (p : Procedure ca cb f) (e : p.Registers → K) (he : Function.Injective e) : Procedure ca cb f

Embed a procedure in a larger finite register type.

Equations

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

def Complexity.RationalHitting.StackLanguage.Procedure.branch {A B : Type} {ca : A → List Bool} {cb : B → List Bool} {f g : A → B} (p : Procedure ca cb f) (q : Procedure ca cb g) : Procedure (pairCode boolCode ca) cb fun (a : Bool × A) => if a.1 = true then f a.2 else g a.2

Deterministic Boolean branching on a serialized pair. Only the selected finite subprogram runs; the tag is physically consumed.

Equations

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

def Complexity.RationalHitting.StackLanguage.unaryCode (n : ℕ) : List Bool

Unary loop count. These symbols are explicitly popped by the loop body.

Equations

• Complexity.RationalHitting.StackLanguage.unaryCode n = List.replicate n true

@[simp]

theorem Complexity.RationalHitting.StackLanguage.unaryCode_length (n : ℕ) : (unaryCode n).length = n

@[simp]

theorem Complexity.RationalHitting.StackLanguage.unaryCode_zero : unaryCode 0 = []

@[simp]

theorem Complexity.RationalHitting.StackLanguage.unaryCode_succ (n : ℕ) : unaryCode (n + 1) = true :: unaryCode n

def Complexity.RationalHitting.StackLanguage.Procedure.iterateProgram {A : Type} {ca : A → List Bool} {f : A → A} (p : Procedure ca ca f) : Program (p.Registers ⊕ Unit)

Repeat a procedure using a separate unary counter register.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Procedure.eval_iterateProgram {A : Type} {ca : A → List Bool} {f : A → A} (p : Procedure ca ca f) (hport : p.output = p.input) (n : ℕ) (a : A) (B : ℕ) (hb : ∀ i ≤ n, (ca (f^[i] a)).length ≤ B) : ∃ t ≤ n * (p.bound.eval (B + 1) + 3) + 1, Eval p.iterateProgram (both (Sum.inl p.input) (Sum.inr ()) (ca a) (unaryCode n)) (single (Sum.inl p.input) (ca (f^[n] a))) t

def Complexity.RationalHitting.StackLanguage.Procedure.iterate {A : Type} {ca : A → List Bool} {f : A → A} (p : Procedure ca ca f) (Q : TimeBound) (hQ : ∀ (n : ℕ) (a : A), ∀ i ≤ n, (ca (f^[i] a)).length ≤ Q.eval ((pairCode unaryCode ca (n, a)).length + 1)) : Procedure (pairCode unaryCode ca) ca fun (a : ℕ × A) => f^[a.1] a.2

Bounded iteration is compiled to a real finite loop. The semantic size invariant is a proof obligation, not a loop oracle or added main hypothesis.

Equations

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