One-way liveness

OpenAI's relation-product language from An Exponential Two-Way Deterministic State Lower Bound for One-Way Liveness (25 September 2026). Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Automata/Model.lean

A letter is a binary relation on Fin h. A word is Live when the product of its relations is nonempty, equivalently when it has a path through all layers. The alphabet is finite, but its size depends on h.

structure Complexity.FiniteAutomaton.BRel (H : Type u_1) : Type u_1

Binary relations, with multiplication following the order of a path.

• holds : H → H → Prop

  Whether a pair of endpoints belongs to the relation.

theorem Complexity.FiniteAutomaton.BRel.ext {H : Type u_1} {x y : BRel H} (holds : x.holds = y.holds) : x = y

theorem Complexity.FiniteAutomaton.BRel.ext_iff {H : Type u_1} {x y : BRel H} : x = y ↔ x.holds = y.holds

@[instance_reducible]

instance Complexity.FiniteAutomaton.BRel.instOne {H : Type u_1} : One (BRel H)

Equations

• Complexity.FiniteAutomaton.BRel.instOne = { one := { holds := Eq } }

@[instance_reducible]

instance Complexity.FiniteAutomaton.BRel.instMul {H : Type u_1} : Mul (BRel H)

Equations

• Complexity.FiniteAutomaton.BRel.instMul = { mul := fun (a b : Complexity.FiniteAutomaton.BRel H) => { holds := fun (x z : H) => ∃ (y : H), a.holds x y ∧ b.holds y z } }

@[instance_reducible]

instance Complexity.FiniteAutomaton.BRel.instZero {H : Type u_1} : Zero (BRel H)

Equations

• Complexity.FiniteAutomaton.BRel.instZero = { zero := { holds := fun (x x_1 : H) => False } }

@[simp]

theorem Complexity.FiniteAutomaton.BRel.one_holds {H : Type u_1} (x y : H) : holds 1 x y ↔ x = y

@[simp]

theorem Complexity.FiniteAutomaton.BRel.mul_holds {H : Type u_1} (a b : BRel H) (x z : H) : (a * b).holds x z ↔ ∃ (y : H), a.holds x y ∧ b.holds y z

@[simp]

theorem Complexity.FiniteAutomaton.BRel.zero_holds {H : Type u_1} (x y : H) : ¬holds 0 x y

@[instance_reducible]

instance Complexity.FiniteAutomaton.BRel.instMonoid {H : Type u_1} : Monoid (BRel H)

Equations

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

def Complexity.FiniteAutomaton.BRel.restrictedId {H : Type u_1} (F : Set H) : BRel H

The identity relation restricted to a set.

Equations

• Complexity.FiniteAutomaton.BRel.restrictedId F = { holds := fun (x y : H) => x = y ∧ x ∈ F }

def Complexity.FiniteAutomaton.BRel.Live {H : Type u_1} (w : List (BRel H)) : Prop

The product of the relations has at least one pair of related endpoints.

Equations

• Complexity.FiniteAutomaton.BRel.Live w = ∃ (x : H) (y : H), w.prod.holds x y

instance Complexity.FiniteAutomaton.BRel.instFinite {H : Type u_1} [Finite H] : Finite (BRel H)

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.Alphabet (h : ℕ) : Type

The finite alphabet of all binary relations on h points.

Equations

• Complexity.FiniteAutomaton.Alphabet h = Complexity.FiniteAutomaton.BRel (Fin h)

def Complexity.FiniteAutomaton.oneWayLiveness (h : ℕ) : Set (List (Alphabet h))

Words whose relation product is nonempty.

Equations

• Complexity.FiniteAutomaton.oneWayLiveness h = {w : List (Complexity.FiniteAutomaton.Alphabet h) | Complexity.FiniteAutomaton.BRel.Live w}

def Complexity.FiniteAutomaton.livenessNFA (h : ℕ) : NFA (Alphabet h) (Fin h)

The ordinary Mathlib NFA for one-way liveness, with h states and every state both initial and accepting. The endmarker model uses three additional states.

Equations

• Complexity.FiniteAutomaton.livenessNFA h = { step := fun (q : Fin h) (R : Complexity.FiniteAutomaton.Alphabet h) => {r : Fin h | R.holds q r}, start := Set.univ, accept := Set.univ }