Arithmetic leaves for proof-carrying binary routines -- definitions

These adapters expose the remaining framed binary subroutines through the pure value-vector interface. Static index separation and reusable-zero requirements remain explicit in BinaryRoutine.requires.

def Complexity.BinaryRoutine.clear {n : ℕ} (idx : Fin n) : BinaryRoutine n

Clear one canonical binary work value to zero.

Equations

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

def Complexity.BinaryRoutine.addConst {n : ℕ} (idx : Fin n) (constant : ℕ) : BinaryRoutine n

Add one hardwired natural to a canonical binary value.

Equations

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

def Complexity.BinaryRoutine.set {n : ℕ} (idx : Fin n) (value : ℕ) : BinaryRoutine n

Replace one canonical binary value by a hardwired natural.

Equations

• Complexity.BinaryRoutine.set idx value = (Complexity.BinaryRoutine.clear idx).seq (Complexity.BinaryRoutine.addConst idx value)

def Complexity.BinaryRoutine.add {n : ℕ} (srcIdx dstIdx counterIdx : Fin n) : BinaryRoutine n

Add a preserved source into a destination and restore a private counter.

Equations

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

def Complexity.BinaryRoutine.mulAdd {n : ℕ} (leftIdx rightIdx accIdx mulCounterIdx addCounterIdx : Fin n) : BinaryRoutine n

Add the product of two preserved values into an accumulator and restore both private counters.

Equations

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

noncomputable def Complexity.BinaryRoutine.evalPolynomial {n : ℕ} (inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx : Fin n) (p : Polynomial ℕ) : BinaryRoutine n

Evaluate one fixed natural polynomial from a preserved input into a zero result tape, restoring the alternate accumulator and both counters.

Equations

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

def Complexity.BinaryRoutine.emitNatCode {n : ℕ} (counterIdx valueIdx : Fin n) : BinaryRoutine n

Emit the terminated-unary code of a preserved value, restoring the zero scratch counter and leaving all pure values unchanged.

Equations

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

def Complexity.BinaryRoutine.emitRawGate {n : ℕ} (op : AndOrOp) (negated₀ negated₁ : Bool) (emitCounterIdx input₀Idx input₁Idx : Fin n) : BinaryRoutine n

Emit one raw gate without advancing any pure value. This is the loop body used when the surrounding binary driver itself advances the wire frontier.

Equations

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