Arithmetic leaves for proof-carrying binary routines

This module exposes sound proof-carrying adapters for canonical binary arithmetic, fixed-polynomial evaluation, natural-code emission, and raw-gate emission. Each theorem connects the adapter's pure value effect, exact emitted word, time bound, and all-prefix space bound to its concrete Turing machine.

Main results

• clear_sound, addConst_sound, set_sound, add_sound, and mulAdd_sound cover basic arithmetic leaves.
• evalPolynomial_sound covers fixed natural-polynomial evaluation.
• emitNatCode_sound and emitRawGate_sound cover the two encoding leaves.

theorem Complexity.BinaryRoutine.clear_sound {n : ℕ} (idx : Fin n) : (clear idx).Sound

Clearing one canonical binary value is a sound routine leaf.

theorem Complexity.BinaryRoutine.addConst_sound {n : ℕ} (idx : Fin n) (constant : ℕ) : (addConst idx constant).Sound

Adding a hardwired natural to one canonical value is sound.

theorem Complexity.BinaryRoutine.set_sound {n : ℕ} (idx : Fin n) (value : ℕ) : (set idx value).Sound

Replacing one canonical binary value by a hardwired natural is sound.

theorem Complexity.BinaryRoutine.add_sound {n : ℕ} (srcIdx dstIdx counterIdx : Fin n) : (add srcIdx dstIdx counterIdx).Sound

Preserved-source binary addition is sound on its explicit distinct-index and zero-counter domain.

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

Binary multiply-add is sound on its explicit distinct-index and zero-counter domain.

theorem Complexity.BinaryRoutine.evalPolynomial_sound {n : ℕ} (inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx : Fin n) (p : Polynomial ℕ) : (evalPolynomial inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx p).Sound

Evaluation of a fixed natural polynomial is sound on its explicit distinct-index and zero-scratch domain.

theorem Complexity.BinaryRoutine.emitNatCode_sound {n : ℕ} (counterIdx valueIdx : Fin n) : (emitNatCode counterIdx valueIdx).Sound

Terminated-unary natural-code emission is sound, preserves every pure value, and restores its zero scratch counter.

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

Raw-gate emission is sound, preserves every pure value, and emits exactly the encoded gate assembled from its two referenced values.