Structured RAM pair validator — proof internals

The benchmark supplies only its typed scanner specification. State encoding, execution, correctness, and resource proofs are all in the generic scanner layer.

theorem Complexity.RAM.Structured.PairValidate.program_measured_internal (bits : List Bool) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec program (inputStore bits) final (stepCount bits.length) cost space ∧ cost ≤ timeBound bits.length ∧ space ≤ spaceBound bits.length ∧ final lengthReg = Input.bitValue (TM.pairValidateAccept (List.foldl TM.pairValidateStep TM.PairValidateState.next bits))