Rational hitting lists: model

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

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

inductive Complexity.RationalHitting.Formula (n : ℕ) : Type

A noncommutative rational formula over n variables and rational constants.

• var {n : ℕ} : Fin n → Formula n

  An input variable.

• const {n : ℕ} : ℚ → Formula n

  A rational scalar.

• add {n : ℕ} : Formula n → Formula n → Formula n

  Addition of two subformulas.

• mul {n : ℕ} : Formula n → Formula n → Formula n

  Ordered multiplication of two subformulas.

• inv {n : ℕ} : Formula n → Formula n

  Inversion, defined only when the evaluated operand is a unit.

@[instance_reducible]

instance Complexity.RationalHitting.instDecidableEqFormula {n✝ : ℕ} : DecidableEq (Formula n✝)

Equations

• Complexity.RationalHitting.instDecidableEqFormula = Complexity.RationalHitting.instDecidableEqFormula.decEq

def Complexity.RationalHitting.instDecidableEqFormula.decEq {n✝ : ℕ} (x✝ x✝¹ : Formula n✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RationalHitting.instDecidableEqFormula.decEq (Complexity.RationalHitting.Formula.var a) (Complexity.RationalHitting.Formula.var b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq (Complexity.RationalHitting.Formula.var a) (Complexity.RationalHitting.Formula.const a_1) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq (Complexity.RationalHitting.Formula.var a) (a_1.add a_2) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq (Complexity.RationalHitting.Formula.var a) (a_1.mul a_2) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq (Complexity.RationalHitting.Formula.var a) a_1.inv = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq (Complexity.RationalHitting.Formula.const a) (Complexity.RationalHitting.Formula.var a_1) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq (Complexity.RationalHitting.Formula.const a) (Complexity.RationalHitting.Formula.const b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq (Complexity.RationalHitting.Formula.const a) (a_1.add a_2) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq (Complexity.RationalHitting.Formula.const a) (a_1.mul a_2) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq (Complexity.RationalHitting.Formula.const a) a_1.inv = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq (a.add a_1) (Complexity.RationalHitting.Formula.var a_2) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq (a.add a_1) (Complexity.RationalHitting.Formula.const a_2) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq (a.add a_1) (a_2.mul a_3) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq (a.add a_1) a_2.inv = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq (a.mul a_1) (Complexity.RationalHitting.Formula.var a_2) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq (a.mul a_1) (Complexity.RationalHitting.Formula.const a_2) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq (a.mul a_1) (a_2.add a_3) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq (a.mul a_1) a_2.inv = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq a.inv (Complexity.RationalHitting.Formula.var a_1) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq a.inv (Complexity.RationalHitting.Formula.const a_1) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq a.inv (a_1.add a_2) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqFormula.decEq a.inv (a_1.mul a_2) = isFalse ⋯

def Complexity.RationalHitting.Formula.size {n : ℕ} : Formula n → ℕ

Number of syntax-tree nodes, counting variables, constants, and operations.

Equations

• (Complexity.RationalHitting.Formula.var a).size = 1
• (Complexity.RationalHitting.Formula.const a).size = 1
• (f.add g).size = f.size + g.size + 1
• (f.mul g).size = f.size + g.size + 1
• f.inv.size = f.size + 1

inductive Complexity.RationalHitting.Formula.Eval {n : ℕ} {R : Type u} [Ring R] (c : ℚ →+* R) (X : Fin n → R) : Formula n → R → Prop

Evaluation in any rational algebra; a unary inverse requires an actual two-sided inverse of the evaluated operand, not a totalized inverse.

• var {n : ℕ} {R : Type u} [Ring R] {c : ℚ →+* R} {X : Fin n → R} (i : Fin n) : Eval c X (Formula.var i) (X i)

  A variable evaluates to its assigned value.

• const {n : ℕ} {R : Type u} [Ring R] {c : ℚ →+* R} {X : Fin n → R} (a : ℚ) : Eval c X (Formula.const a) (c a)

  A constant evaluates through the specified scalar homomorphism.

• add {n : ℕ} {R : Type u} [Ring R] {c : ℚ →+* R} {X : Fin n → R} {f g : Formula n} {a b : R} : Eval c X f a → Eval c X g b → Eval c X (f.add g) (a + b)

  Defined summands give a defined sum.

• mul {n : ℕ} {R : Type u} [Ring R] {c : ℚ →+* R} {X : Fin n → R} {f g : Formula n} {a b : R} : Eval c X f a → Eval c X g b → Eval c X (f.mul g) (a * b)

  Defined factors give a defined ordered product.

• inv {n : ℕ} {R : Type u} [Ring R] {c : ℚ →+* R} {X : Fin n → R} {f : Formula n} {a b : R} : Eval c X f a → a * b = 1 → b * a = 1 → Eval c X f.inv b

  Both inverse identities are required at an inverse node.

@[reducible, inline]

abbrev Complexity.RationalHitting.Mat (d : ℕ) : Type

Square rational matrices of the specified dimension.

Equations

• Complexity.RationalHitting.Mat d = Matrix (Fin d) (Fin d) ℚ

@[reducible, inline]

abbrev Complexity.RationalHitting.Tuple (n d : ℕ) : Type

A matrix substitution for every input variable.

Equations

• Complexity.RationalHitting.Tuple n d = (Fin n → Complexity.RationalHitting.Mat d)

def Complexity.RationalHitting.Evaluates {n d : ℕ} (f : Formula n) (X : Tuple n d) (v : Mat d) : Prop

Defined evaluation on a rational matrix tuple.

Equations

• Complexity.RationalHitting.Evaluates f X v = Complexity.RationalHitting.Formula.Eval (algebraMap ℚ (Complexity.RationalHitting.Mat d)) X f v

def Complexity.RationalHitting.Admissible {n : ℕ} (f : Formula n) : Prop

Some positive-dimensional rational matrix substitution is in the formula's domain.

Equations

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

def Complexity.RationalHitting.Nonzero {n : ℕ} (f : Formula n) : Prop

Some positive-dimensional rational matrix substitution has a defined nonzero value.

Equations

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

structure Complexity.RationalHitting.Output (n : ℕ) : Type

All output tuples have one common positive dimension.

• dimension : ℕ

  Common dimension of all matrix tuples.

• dimension_pos : 0 < self.dimension

  Exclude the trivial zero-dimensional matrix ring.

• tuples : List (Tuple n self.dimension)

  The finite list of matrix substitutions, in output order.

def Complexity.RationalHitting.encodeNat (a : ℕ) : List Bool

Little-endian unsigned binary, prefixed by a unary bit-length and a zero terminator. This is a self-delimiting binary encoding, including zero.

Equations

• Complexity.RationalHitting.encodeNat a = List.replicate (List.map (fun (b : ℕ) => b != 0) (Nat.digits 2 a)).length true ++ [false] ++ List.map (fun (b : ℕ) => b != 0) (Nat.digits 2 a)

def Complexity.RationalHitting.encodeRat (a : ℚ) : List Bool

Sign bit, binary numerator magnitude, and positive binary denominator. Rat.num and Rat.den are the canonical reduced numerator and denominator.

Equations

• Complexity.RationalHitting.encodeRat a = [decide (a.num < 0)] ++ Complexity.RationalHitting.encodeNat a.num.natAbs ++ Complexity.RationalHitting.encodeNat a.den

def Complexity.RationalHitting.encodeTuple {n d : ℕ} (X : Tuple n d) : List Bool

Serialize a tuple in variable, row, and column order using reduced rational encodings.

Equations

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

def Complexity.RationalHitting.encodeOutput {n : ℕ} (H : Output n) : List Bool

Encode the common dimension, tuple count, and all rational matrix entries.

Equations

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

@[reducible, inline]

abbrev Complexity.RationalHitting.Alphabet : Type

0 is blank, 1 and 2 are the two literal binary digits, 3 is work space. Fixed finite tape alphabet and finite state space; no advice or oracle.

Equations

• Complexity.RationalHitting.Alphabet = Fin 4

@[reducible, inline]

abbrev Complexity.RationalHitting.Machine (m : ℕ) : Type

A finite-state Mathlib machine on the fixed four-symbol alphabet.

Equations

• Complexity.RationalHitting.Machine m = Turing.TM0.Machine Complexity.RationalHitting.Alphabet (Fin (m + 1))

@[reducible, inline]

abbrev Complexity.RationalHitting.Config (m : ℕ) : Type

Configuration of the corresponding Mathlib machine.

Equations

• Complexity.RationalHitting.Config m = Turing.TM0.Cfg Complexity.RationalHitting.Alphabet (Fin (m + 1))

def Complexity.RationalHitting.tapeBit (b : Bool) : Alphabet

The two nonblank tape symbols representing a literal binary digit.

Equations

• Complexity.RationalHitting.tapeBit b = if b = true then 2 else 1

def Complexity.RationalHitting.unaryInput (n s : ℕ) : List Alphabet

Two unary parameters separated by one distinguished nonblank symbol.

Equations

• Complexity.RationalHitting.unaryInput n s = List.replicate n 2 ++ [1] ++ List.replicate s 2

def Complexity.RationalHitting.run {m : ℕ} (G : Machine m) : ℕ → Config m → Option (Config m)

Exactly t ordinary deterministic TM0 transitions.

Equations

• Complexity.RationalHitting.run G 0 x✝ = some x✝
• Complexity.RationalHitting.run G t.succ x✝ = (Turing.TM0.step G x✝).bind (Complexity.RationalHitting.run G t)

def Complexity.RationalHitting.OutputsWithin {m n : ℕ} (G : Machine m) (s bound : ℕ) (H : Output n) : Prop

Halt within the given transition bound with the complete encoding at and right of the head.

Equations

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

def Complexity.RationalHitting.Hits {n : ℕ} (s : ℕ) (H : Output n) : Prop

Every admissible nonzero formula of bounded size has an invertible value on the list.

Equations

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

def Complexity.RationalHitting.MainStatement : Prop

A fixed polynomial bound on bit time, full binary output length, and common positive dimension.

Equations

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